-- Mathlib/GroupTheory/Nilpotent.lean
theorem nilpotent_iff_finite_descending_central_series :
    IsNilpotent G ↔ ∃ n : ℕ, ∃ H : ℕ → Subgroup G, IsDescendingCentralSeries H ∧ H n = ⊥

Proof state:
case mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H (n - n) = ⊥

Tactic:
rw [tsub_self]

Result:
case mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H 0 = ⊥

Proof state:
case mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ (fun m => H (n - m)) n = ⊥

Tactic:
dsimp only

Result:
case mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H (n - n) = ⊥

Proof state:
G : Type u_1
inst✝ : Group G
⊢ IsNilpotent G ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
rw [nilpotent_iff_finite_ascending_central_series]

Result:
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Proof state:
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
constructor

Result:
case mp
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) → ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

Proof state:
case mp
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) → ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
rintro ⟨n, H, hH, hn⟩

Result:
case mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Proof state:
case mpr.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤

Tactic:
exact hH.1

Result:
no goals

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
rintro ⟨n, H, hH, hn⟩

Result:
case mpr.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

Proof state:
case mpr.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H (n - n) = ⊤

Tactic:
rw [tsub_self]

Result:
case mpr.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤

Proof state:
case mpr.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
refine ⟨n, fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩

Result:
case mpr.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ (fun m => H (n - m)) n = ⊤

Proof state:
case mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H 0 = ⊥

Tactic:
exact hH.1

Result:
no goals

Proof state:
case mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
refine ⟨n, fun m => H (n - m), is_descending_rev_series_of_is_ascending G hn hH, ?_⟩

Result:
case mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ (fun m => H (n - m)) n = ⊥

Proof state:
case mpr.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ (fun m => H (n - m)) n = ⊤

Tactic:
dsimp only

Result:
case mpr.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H (n - n) = ⊤