[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B ∈ {U | star U * U = 1 ∧ U * star U = 1}
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ star (U * B) * (U * B) = 1
[PROOFSTEP]
calc
  star (U * B) * (U * B) = star B * star U * U * B := by simp only [mul_assoc, star_mul]
  _ = star B * (star U * U) * B := by rw [← mul_assoc]
  _ = 1 := by rw [hA₁, mul_one, hB₁]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ star (U * B) * (U * B) = star B * star U * U * B
[PROOFSTEP]
simp only [mul_assoc, star_mul]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ star B * star U * U * B = star B * (star U * U) * B
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ star B * (star U * U) * B = 1
[PROOFSTEP]
rw [hA₁, mul_one, hB₁]
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * star (U * B) = 1
[PROOFSTEP]
calc
  U * B * star (U * B) = U * B * (star B * star U) := by rw [star_mul]
  _ = U * (B * star B) * star U := by simp_rw [← mul_assoc]
  _ = 1 := by rw [hB₂, mul_one, hA₂]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * star (U * B) = U * B * (star B * star U)
[PROOFSTEP]
rw [star_mul]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * (star B * star U) = U * (B * star B) * star U
[PROOFSTEP]
simp_rw [← mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * (B * star B) * star U = 1
[PROOFSTEP]
rw [hB₂, mul_one, hA₂]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
⊢ 1 ∈
    { carrier := {U | star U * U = 1 ∧ U * star U = 1},
        mul_mem' :=
          (_ :
            ∀ (U B : R),
              U ∈ {U | star U * U = 1 ∧ U * star U = 1} →
                B ∈ {U | star U * U = 1 ∧ U * star U = 1} → U * B ∈ {U | star U * U = 1 ∧ U * star U = 1}) }.carrier
[PROOFSTEP]
simp only [mul_one, and_self_iff, Set.mem_setOf_eq, star_one]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U : R
hU : U ∈ unitary R
⊢ star (star U) * star U = 1
[PROOFSTEP]
rw [star_star, mul_star_self_of_mem hU]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U : R
hU : U ∈ unitary R
⊢ star U * star (star U) = 1
[PROOFSTEP]
rw [star_star, star_mul_self_of_mem hU]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
⊢ Function.Involutive star
[PROOFSTEP]
intro x
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
x : { x // x ∈ unitary R }
⊢ star (star x) = x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
x : { x // x ∈ unitary R }
⊢ ↑(star (star x)) = ↑x
[PROOFSTEP]
rw [coe_star, coe_star, star_star]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
⊢ ∀ (r s : { x // x ∈ unitary R }), star (r * s) = star s * star r
[PROOFSTEP]
intro x y
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
x y : { x // x ∈ unitary R }
⊢ star (x * y) = star y * star x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
x y : { x // x ∈ unitary R }
⊢ ↑(star (x * y)) = ↑(star y * star x)
[PROOFSTEP]
rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]
[GOAL]
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarSemigroup R
U₁ U₂ : { x // x ∈ unitary R }
⊢ ↑(U₁ / U₂) = ↑U₁ / ↑U₂
[PROOFSTEP]
simp only [div_eq_mul_inv, coe_inv, Submonoid.coe_mul]
[GOAL]
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarSemigroup R
U : { x // x ∈ unitary R }
z : ℤ
⊢ ↑(U ^ z) = ↑U ^ z
[PROOFSTEP]
induction z
[GOAL]
case ofNat
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarSemigroup R
U : { x // x ∈ unitary R }
a✝ : ℕ
⊢ ↑(U ^ Int.ofNat a✝) = ↑U ^ Int.ofNat a✝
[PROOFSTEP]
simp [SubmonoidClass.coe_pow]
[GOAL]
case negSucc
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarSemigroup R
U : { x // x ∈ unitary R }
a✝ : ℕ
⊢ ↑(U ^ Int.negSucc a✝) = ↑U ^ Int.negSucc a✝
[PROOFSTEP]
simp [coe_inv]
[GOAL]
R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
U : { x // x ∈ unitary R }
⊢ -↑U ∈ unitary R
[PROOFSTEP]
simp [mem_iff, star_neg, neg_mul_neg]
