case h
α : Type ?u.11501
s t : Set α
a : α
β : Type u_1
inst✝ : InvolutiveStar β
x y : β
⊢ y ∈ {x}⋆ ↔ y ∈ {x⋆}
α : Type ?u.11501
s t : Set α
a : α
β : Type u_1
inst✝ : InvolutiveStar β
x : β
⊢ {x}⋆ = {x⋆}
ext1 y
no goals
case h
α : Type ?u.11501
s t : Set α
a : α
β : Type u_1
inst✝ : InvolutiveStar β
x y : β
⊢ y ∈ {x}⋆ ↔ y ∈ {x⋆}
rw [mem_star, mem_singleton_iff, mem_singleton_iff, star_eq_iff_star_eq, eq_comm]