case zero
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
⊢ Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } Nat.zero) ≤ lowerCentralSeries G Nat.zero

case succ
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
⊢ Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } (Nat.succ d)) ≤ lowerCentralSeries G (Nat.succ d)
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
n : ℕ
⊢ Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } n) ≤ lowerCentralSeries G n
induction' n with d hd
no goals
case zero
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
⊢ Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } Nat.zero) ≤ lowerCentralSeries G Nat.zero
simp
case succ
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
⊢ closure
      (↑(Subgroup.subtype H) ''
        {x | ∃ p, p ∈ lowerCentralSeries { x // x ∈ H } d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x}) ≤
    closure {x | ∃ p, p ∈ lowerCentralSeries G d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x}
case succ
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
⊢ Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } (Nat.succ d)) ≤ lowerCentralSeries G (Nat.succ d)
rw [lowerCentralSeries_succ, lowerCentralSeries_succ, MonoidHom.map_closure]
case succ.h'
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
⊢ ↑(Subgroup.subtype H) '' {x | ∃ p, p ∈ lowerCentralSeries { x // x ∈ H } d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x} ⊆
    {x | ∃ p, p ∈ lowerCentralSeries G d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x}
case succ
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
⊢ closure
      (↑(Subgroup.subtype H) ''
        {x | ∃ p, p ∈ lowerCentralSeries { x // x ∈ H } d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x}) ≤
    closure {x | ∃ p, p ∈ lowerCentralSeries G d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x}
apply Subgroup.closure_mono
case succ.h'.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
x3 : { x // x ∈ H }
hx3 : x3 ∈ lowerCentralSeries { x // x ∈ H } d
x4 : { x // x ∈ H }
_hx4 : x4 ∈ ⊤
⊢ ↑(Subgroup.subtype H) (x3 * x4 * x3⁻¹ * x4⁻¹) ∈
    {x | ∃ p, p ∈ lowerCentralSeries G d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x}
case succ.h'
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
⊢ ↑(Subgroup.subtype H) '' {x | ∃ p, p ∈ lowerCentralSeries { x // x ∈ H } d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x} ⊆
    {x | ∃ p, p ∈ lowerCentralSeries G d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x}
rintro x1 ⟨x2, ⟨x3, hx3, x4, _hx4, rfl⟩, rfl⟩
no goals
case succ.h'.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
x3 : { x // x ∈ H }
hx3 : x3 ∈ lowerCentralSeries { x // x ∈ H } d
x4 : { x // x ∈ H }
_hx4 : x4 ∈ ⊤
⊢ ↑(Subgroup.subtype H) (x3 * x4 * x3⁻¹ * x4⁻¹) ∈
    {x | ∃ p, p ∈ lowerCentralSeries G d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x}
exact ⟨x3, hd (mem_map.mpr ⟨x3, hx3, rfl⟩), x4, by simp⟩
no goals
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
x3 : { x // x ∈ H }
hx3 : x3 ∈ lowerCentralSeries { x // x ∈ H } d
x4 : { x // x ∈ H }
_hx4 : x4 ∈ ⊤
⊢ ↑x4 ∈ ⊤ ∧ ↑x3 * ↑x4 * (↑x3)⁻¹ * (↑x4)⁻¹ = ↑(Subgroup.subtype H) (x3 * x4 * x3⁻¹ * x4⁻¹)
simp