-- Mathlib/GroupTheory/Nilpotent.lean
theorem lowerCentralSeries.map {H : Type*} [Group H] (f : G →* H) (n : ℕ) :
    Subgroup.map f (lowerCentralSeries G n) ≤ lowerCentralSeries H n

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
n : ℕ
⊢ Subgroup.map f (lowerCentralSeries G n) ≤ lowerCentralSeries H n

Tactic:
induction' n with d hd

Result:
case zero
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
⊢ Subgroup.map f (lowerCentralSeries G 0) ≤ lowerCentralSeries H 0

case succ
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
⊢ Subgroup.map f (lowerCentralSeries G (d + 1)) ≤ lowerCentralSeries H (d + 1)

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
y : G
x✝ : y ∈ closure {g | ∃ g₁ ∈ lowerCentralSeries G d, ∃ g₂ ∈ ⊤, ⁅g₁, g₂⁆ = g}
hy : f y ∈ lowerCentralSeries H (d + 1)
⊢ f y⁻¹ ∈ lowerCentralSeries H (d + 1)

Tactic:
rw [f.map_inv]

Result:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
y : G
x✝ : y ∈ closure {g | ∃ g₁ ∈ lowerCentralSeries G d, ∃ g₂ ∈ ⊤, ⁅g₁, g₂⁆ = g}
hy : f y ∈ lowerCentralSeries H (d + 1)
⊢ (f y)⁻¹ ∈ lowerCentralSeries H (d + 1)

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
y : G
x✝ : y ∈ closure {g | ∃ g₁ ∈ lowerCentralSeries G d, ∃ g₂ ∈ ⊤, ⁅g₁, g₂⁆ = g}
hy : f y ∈ lowerCentralSeries H (d + 1)
⊢ (f y)⁻¹ ∈ lowerCentralSeries H (d + 1)

Tactic:
exact Subgroup.inv_mem _ hy

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
y z : G
x✝¹ : y ∈ closure {g | ∃ g₁ ∈ lowerCentralSeries G d, ∃ g₂ ∈ ⊤, ⁅g₁, g₂⁆ = g}
x✝ : z ∈ closure {g | ∃ g₁ ∈ lowerCentralSeries G d, ∃ g₂ ∈ ⊤, ⁅g₁, g₂⁆ = g}
hy : f y ∈ lowerCentralSeries H (d + 1)
hz : f z ∈ lowerCentralSeries H (d + 1)
⊢ f (y * z) ∈ lowerCentralSeries H (d + 1)

Tactic:
simp [MonoidHom.map_mul, Subgroup.mul_mem _ hy hz]

Result:
no goals

Proof state:
case zero
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
⊢ Subgroup.map f (lowerCentralSeries G 0) ≤ lowerCentralSeries H 0

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
y : G
hy : y ∈ lowerCentralSeries G d
z : G
K : Subgroup H
hK : {g | ∃ g₁ ∈ lowerCentralSeries H d, ∃ g₂ ∈ ⊤, ⁅g₁, g₂⁆ = g} ⊆ ↑K
⊢ ∃ g₂ ∈ ⊤, ⁅f y, g₂⁆ = f ⁅y, z⁆

Tactic:
simp [commutatorElement_def]

Result:
no goals

Proof state:
case succ.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
⊢ f x ∈ lowerCentralSeries H (d + 1)

Tactic:
refine closure_induction (hx := hx) ?_ (by simp [f.map_one, Subgroup.one_mem _])
  (fun y z _ _ hy hz => by simp [MonoidHom.map_mul, Subgroup.mul_mem _ hy hz]) (fun y _ hy => by
    rw [f.map_inv]; exact Subgroup.inv_mem _ hy)

Result:
case succ.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
⊢ ∀ x ∈ {g | ∃ g₁ ∈ lowerCentralSeries G d, ∃ g₂ ∈ ⊤, ⁅g₁, g₂⁆ = g}, f x ∈ lowerCentralSeries H (d + 1)

Proof state:
case succ.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
y : G
hy : y ∈ lowerCentralSeries G d
z : G
⊢ ∀ (K : Subgroup H), {g | ∃ g₁ ∈ lowerCentralSeries H d, ∃ g₂ ∈ ⊤, ⁅g₁, g₂⁆ = g} ⊆ ↑K → f ⁅y, z⁆ ∈ K

Tactic:
exact fun K hK => hK ⟨f y, hd (mem_map_of_mem f hy), by simp [commutatorElement_def]⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
⊢ f 1 ∈ lowerCentralSeries H (d + 1)

Tactic:
simp [f.map_one, Subgroup.one_mem _]

Result:
no goals

Proof state:
case succ.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
y : G
hy : y ∈ lowerCentralSeries G d
z : G
⊢ f ⁅y, z⁆ ∈ lowerCentralSeries H (d + 1)

Tactic:
apply mem_closure.mpr

Result:
case succ.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
y : G
hy : y ∈ lowerCentralSeries G d
z : G
⊢ ∀ (K : Subgroup H), {g | ∃ g₁ ∈ lowerCentralSeries H d, ∃ g₂ ∈ ⊤, ⁅g₁, g₂⁆ = g} ⊆ ↑K → f ⁅y, z⁆ ∈ K

Proof state:
case succ.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
⊢ ∀ x ∈ {g | ∃ g₁ ∈ lowerCentralSeries G d, ∃ g₂ ∈ ⊤, ⁅g₁, g₂⁆ = g}, f x ∈ lowerCentralSeries H (d + 1)

Tactic:
rintro a ⟨y, hy, z, ⟨-, rfl⟩⟩

Result:
case succ.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
y : G
hy : y ∈ lowerCentralSeries G d
z : G
⊢ f ⁅y, z⁆ ∈ lowerCentralSeries H (d + 1)

Proof state:
case succ
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
⊢ Subgroup.map f (lowerCentralSeries G (d + 1)) ≤ lowerCentralSeries H (d + 1)

Tactic:
rintro a ⟨x, hx : x ∈ lowerCentralSeries G d.succ, rfl⟩

Result:
case succ.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G d.succ
⊢ f x ∈ lowerCentralSeries H (d + 1)