no goals
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U : R
hU : U ∈ unitary R
⊢ star (star U) * star U = 1
rw [star_star, mul_star_self_of_mem hU]
no goals
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U : R
hU : U ∈ unitary R
⊢ star U * star (star U) = 1
rw [star_star, star_mul_self_of_mem hU]