α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
⊢ star '' s = star ⁻¹' s
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
⊢ star '' s = s⋆
simp only [← star_preimage]
no goals
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
⊢ star '' s = star ⁻¹' s
rw [image_eq_preimage_of_inverse] <;> intro <;> simp only [star_star]