[GOAL]
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
⊢ a⋆ ∈ s⋆ ↔ a ∈ s
[PROOFSTEP]
simp only [mem_star, star_star]
[GOAL]
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
⊢ star '' s = s⋆
[PROOFSTEP]
simp only [← star_preimage]
[GOAL]
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
⊢ star '' s = star ⁻¹' s
[PROOFSTEP]
rw [image_eq_preimage_of_inverse]
[GOAL]
case h₁
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
⊢ Function.LeftInverse star star
[PROOFSTEP]
intro
[GOAL]
case h₂
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
⊢ Function.RightInverse star star
[PROOFSTEP]
intro
[GOAL]
case h₁
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
x✝ : α
⊢ x✝⋆⋆ = x✝
[PROOFSTEP]
simp only [star_star]
[GOAL]
case h₂
α : Type u_1
s t : Set α
a : α
inst✝ : InvolutiveStar α
x✝ : α
⊢ x✝⋆⋆ = x✝
[PROOFSTEP]
simp only [star_star]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
inst✝ : InvolutiveStar α
s : Set α
⊢ s⋆⋆ = s
[PROOFSTEP]
simp only [← star_preimage, preimage_preimage, star_star, preimage_id']
[GOAL]
α : Type u_1
s✝ t✝ : Set α
a : α
inst✝ : InvolutiveStar α
s t : Set α
⊢ s⋆ ⊆ t ↔ s ⊆ t⋆
[PROOFSTEP]
rw [← star_subset_star, star_star]
[GOAL]
α : Type u_1
s t : Set α
a : α
β : Type u_2
inst✝ : InvolutiveStar β
x : β
⊢ {x}⋆ = {x⋆}
[PROOFSTEP]
ext1 y
[GOAL]
case h
α : Type u_1
s t : Set α
a : α
β : Type u_2
inst✝ : InvolutiveStar β
x y : β
⊢ y ∈ {x}⋆ ↔ y ∈ {x⋆}
[PROOFSTEP]
rw [mem_star, mem_singleton_iff, mem_singleton_iff, star_eq_iff_star_eq, eq_comm]
[GOAL]
α : Type u_1
s✝ t✝ : Set α
a : α
inst✝¹ : Monoid α
inst✝ : StarSemigroup α
s t : Set α
⊢ (s * t)⋆ = t⋆ * s⋆
[PROOFSTEP]
simp_rw [← image_star, ← image2_mul, image_image2, image2_image_left, image2_image_right, star_mul, image2_swap _ s t]
[GOAL]
α : Type u_1
s✝ t✝ : Set α
a : α
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
s t : Set α
⊢ (s + t)⋆ = s⋆ + t⋆
[PROOFSTEP]
simp_rw [← image_star, ← image2_add, image_image2, image2_image_left, image2_image_right, star_add]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Star α
inst✝ : TrivialStar α
s : Set α
⊢ s⋆ = s
[PROOFSTEP]
rw [← star_preimage]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Star α
inst✝ : TrivialStar α
s : Set α
⊢ star ⁻¹' s = s
[PROOFSTEP]
ext1
[GOAL]
case h
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Star α
inst✝ : TrivialStar α
s : Set α
x✝ : α
⊢ x✝ ∈ star ⁻¹' s ↔ x✝ ∈ s
[PROOFSTEP]
simp [star_trivial]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Group α
inst✝ : StarSemigroup α
s : Set α
⊢ s⁻¹⋆ = s⋆⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Group α
inst✝ : StarSemigroup α
s : Set α
x✝ : α
⊢ x✝ ∈ s⁻¹⋆ ↔ x✝ ∈ s⋆⁻¹
[PROOFSTEP]
simp only [mem_star, mem_inv, star_inv]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : DivisionSemiring α
inst✝ : StarRing α
s : Set α
⊢ s⁻¹⋆ = s⋆⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : DivisionSemiring α
inst✝ : StarRing α
s : Set α
x✝ : α
⊢ x✝ ∈ s⁻¹⋆ ↔ x✝ ∈ s⋆⁻¹
[PROOFSTEP]
simp only [mem_star, mem_inv, star_inv']
[GOAL]
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
⊢ star ↑s = ↑s
[PROOFSTEP]
ext x
[GOAL]
case h
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
x : α
⊢ x ∈ star ↑s ↔ x ∈ ↑s
[PROOFSTEP]
simp only [Set.mem_star, SetLike.mem_coe]
[GOAL]
case h
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
x : α
⊢ star x ∈ s ↔ x ∈ s
[PROOFSTEP]
exact ⟨by simpa only [star_star] using star_mem (s := s) (r := star x), star_mem⟩
[GOAL]
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
x : α
⊢ star x ∈ s → x ∈ s
[PROOFSTEP]
simpa only [star_star] using star_mem (s := s) (r := star x)
