G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) ↔ ∃ n, lowerCentralSeries G n = ⊥
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Group.IsNilpotent G ↔ ∃ n, lowerCentralSeries G n = ⊥
rw [nilpotent_iff_finite_descending_central_series]
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ n, lowerCentralSeries G n = ⊥

case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ (∃ n, lowerCentralSeries G n = ⊥) → ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) ↔ ∃ n, lowerCentralSeries G n = ⊥
constructor
case mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ ∃ n, lowerCentralSeries G n = ⊥
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ n, lowerCentralSeries G n = ⊥
rintro ⟨n, H, ⟨h0, hs⟩, hn⟩
case mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ lowerCentralSeries G n = ⊥
case mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ ∃ n, lowerCentralSeries G n = ⊥
use n
case mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ lowerCentralSeries G n ≤ H n
case mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ lowerCentralSeries G n = ⊥
rw [eq_bot_iff, ← hn]
no goals
case mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ lowerCentralSeries G n ≤ H n
exact descending_central_series_ge_lower H ⟨h0, hs⟩ n
case mpr.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
hn : lowerCentralSeries G n = ⊥
⊢ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ (∃ n, lowerCentralSeries G n = ⊥) → ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
rintro ⟨n, hn⟩
no goals
case mpr.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
hn : lowerCentralSeries G n = ⊥
⊢ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
exact ⟨n, lowerCentralSeries G, lowerCentralSeries_isDescendingCentralSeries, hn⟩