case h
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Group α
inst✝ : StarSemigroup α
s : Set α
x✝ : α
⊢ x✝ ∈ s⁻¹⋆ ↔ x✝ ∈ s⋆⁻¹
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Group α
inst✝ : StarSemigroup α
s : Set α
⊢ s⁻¹⋆ = s⋆⁻¹
ext
no goals
case h
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Group α
inst✝ : StarSemigroup α
s : Set α
x✝ : α
⊢ x✝ ∈ s⁻¹⋆ ↔ x✝ ∈ s⋆⁻¹
simp only [mem_star, mem_inv, star_inv]