-- Mathlib/GroupTheory/Nilpotent.lean
theorem lowerCentralSeries_map_subtype_le (H : Subgroup G) (n : ℕ) :
    (lowerCentralSeries H n).map H.subtype ≤ lowerCentralSeries G n

Proof state:
case zero
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Subgroup.map H.subtype (lowerCentralSeries (↥H) 0) ≤ lowerCentralSeries G 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
G : Type u_1
inst✝ : Group G
H : Subgroup G
d : ℕ
hd : Subgroup.map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
⊢ closure (⇑H.subtype '' {x | ∃ p ∈ lowerCentralSeries (↥H) d, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}) ≤
    closure {x | ∃ p ∈ lowerCentralSeries G d, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}

Tactic:
apply Subgroup.closure_mono

Result:
case succ.h'
G : Type u_1
inst✝ : Group G
H : Subgroup G
d : ℕ
hd : Subgroup.map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
⊢ ⇑H.subtype '' {x | ∃ p ∈ lowerCentralSeries (↥H) d, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x} ⊆
    {x | ∃ p ∈ lowerCentralSeries G d, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}

Proof state:
case succ
G : Type u_1
inst✝ : Group G
H : Subgroup G
d : ℕ
hd : Subgroup.map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
⊢ Subgroup.map H.subtype (lowerCentralSeries (↥H) (d + 1)) ≤ lowerCentralSeries G (d + 1)

Tactic:
rw [lowerCentralSeries_succ, lowerCentralSeries_succ, MonoidHom.map_closure]

Result:
case succ
G : Type u_1
inst✝ : Group G
H : Subgroup G
d : ℕ
hd : Subgroup.map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
⊢ closure (⇑H.subtype '' {x | ∃ p ∈ lowerCentralSeries (↥H) d, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}) ≤
    closure {x | ∃ p ∈ lowerCentralSeries G d, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
d : ℕ
hd : Subgroup.map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
x3 : ↥H
hx3 : x3 ∈ lowerCentralSeries (↥H) d
x4 : ↥H
_hx4 : x4 ∈ ⊤
⊢ ↑x4 ∈ ⊤ ∧ ↑x3 * ↑x4 * (↑x3)⁻¹ * (↑x4)⁻¹ = H.subtype (x3 * x4 * x3⁻¹ * x4⁻¹)

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
⊢ Subgroup.map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n

Tactic:
induction' n with d hd

Result:
case zero
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Subgroup.map H.subtype (lowerCentralSeries (↥H) 0) ≤ lowerCentralSeries G 0

case succ
G : Type u_1
inst✝ : Group G
H : Subgroup G
d : ℕ
hd : Subgroup.map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
⊢ Subgroup.map H.subtype (lowerCentralSeries (↥H) (d + 1)) ≤ lowerCentralSeries G (d + 1)

Proof state:
case succ.h'.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
d : ℕ
hd : Subgroup.map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
x3 : ↥H
hx3 : x3 ∈ lowerCentralSeries (↥H) d
x4 : ↥H
_hx4 : x4 ∈ ⊤
⊢ H.subtype (x3 * x4 * x3⁻¹ * x4⁻¹) ∈ {x | ∃ p ∈ lowerCentralSeries G d, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}

Tactic:
exact ⟨x3, hd (mem_map.mpr ⟨x3, hx3, rfl⟩), x4, by simp⟩

Result:
no goals

Proof state:
case succ.h'
G : Type u_1
inst✝ : Group G
H : Subgroup G
d : ℕ
hd : Subgroup.map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
⊢ ⇑H.subtype '' {x | ∃ p ∈ lowerCentralSeries (↥H) d, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x} ⊆
    {x | ∃ p ∈ lowerCentralSeries G d, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}

Tactic:
rintro x1 ⟨x2, ⟨x3, hx3, x4, _hx4, rfl⟩, rfl⟩

Result:
case succ.h'.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
d : ℕ
hd : Subgroup.map H.subtype (lowerCentralSeries (↥H) d) ≤ lowerCentralSeries G d
x3 : ↥H
hx3 : x3 ∈ lowerCentralSeries (↥H) d
x4 : ↥H
_hx4 : x4 ∈ ⊤
⊢ H.subtype (x3 * x4 * x3⁻¹ * x4⁻¹) ∈ {x | ∃ p ∈ lowerCentralSeries G d, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}