case basic
G : Type u_1
H : Type ?u.144028
A : Type ?u.144031
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x : G
hx : x ∈ conjugatesOfSet s
⊢ g * x * g⁻¹ ∈ normalClosure s

case one
G : Type u_1
H : Type ?u.144028
A : Type ?u.144031
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g : G
⊢ g * 1 * g⁻¹ ∈ normalClosure s

case inv
G : Type u_1
H : Type ?u.144028
A : Type ?u.144031
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x : G
hx : InClosure (conjugatesOfSet s) x
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ g * x⁻¹ * g⁻¹ ∈ normalClosure s

case mul
G : Type u_1
H : Type ?u.144028
A : Type ?u.144031
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x y : G
hx : InClosure (conjugatesOfSet s) x
hy : InClosure (conjugatesOfSet s) y
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * (x * y) * g⁻¹ ∈ normalClosure s
G : Type u_1
H : Type ?u.144028
A : Type ?u.144031
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n : G
h : n ∈ normalClosure s
g : G
⊢ g * n * g⁻¹ ∈ normalClosure s
induction' h with x hx x hx ihx x y hx hy ihx ihy
no goals
case basic
G : Type u_1
H : Type ?u.144028
A : Type ?u.144031
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x : G
hx : x ∈ conjugatesOfSet s
⊢ g * x * g⁻¹ ∈ normalClosure s
exact conjugatesOfSet_subset_normalClosure (conj_mem_conjugatesOfSet hx)
no goals
case one
G : Type u_1
H : Type ?u.144028
A : Type ?u.144031
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g : G
⊢ g * 1 * g⁻¹ ∈ normalClosure s
simpa using (normalClosure.isSubgroup s).one_mem
case inv
G : Type u_1
H : Type ?u.144028
A : Type ?u.144031
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x : G
hx : InClosure (conjugatesOfSet s) x
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ (g * x * g⁻¹)⁻¹ ∈ normalClosure s
case inv
G : Type u_1
H : Type ?u.144028
A : Type ?u.144031
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x : G
hx : InClosure (conjugatesOfSet s) x
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ g * x⁻¹ * g⁻¹ ∈ normalClosure s
rw [← conj_inv]
no goals
case inv
G : Type u_1
H : Type ?u.144028
A : Type ?u.144031
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x : G
hx : InClosure (conjugatesOfSet s) x
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ (g * x * g⁻¹)⁻¹ ∈ normalClosure s
exact (normalClosure.isSubgroup _).inv_mem ihx
case mul
G : Type u_1
H : Type ?u.144028
A : Type ?u.144031
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x y : G
hx : InClosure (conjugatesOfSet s) x
hy : InClosure (conjugatesOfSet s) y
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * x * g⁻¹ * (g * y * g⁻¹) ∈ normalClosure s
case mul
G : Type u_1
H : Type ?u.144028
A : Type ?u.144031
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x y : G
hx : InClosure (conjugatesOfSet s) x
hy : InClosure (conjugatesOfSet s) y
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * (x * y) * g⁻¹ ∈ normalClosure s
rw [← conj_mul]
no goals
case mul
G : Type u_1
H : Type ?u.144028
A : Type ?u.144031
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x y : G
hx : InClosure (conjugatesOfSet s) x
hy : InClosure (conjugatesOfSet s) y
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * x * g⁻¹ * (g * y * g⁻¹) ∈ normalClosure s
exact (normalClosure.isSubgroup _).toIsSubmonoid.mul_mem ihx ihy