-- Mathlib/GroupTheory/Nilpotent.lean
theorem least_descending_central_series_length_eq_nilpotencyClass :
    Nat.find ((nilpotent_iff_finite_descending_central_series G).mp hG) =
    Group.nilpotencyClass G

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

Tactic:
exact hH.1

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ Nat.find ⋯ = Nat.find ⋯

Tactic:
refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)

Result:
case refine_1
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsAscendingCentralSeries H ∧ H n = ⊤) → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥

case refine_2
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤

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

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

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

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

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

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

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

Tactic:
dsimp only

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

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

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

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

Proof state:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ Nat.find ⋯ = nilpotencyClass G

Tactic:
rw [← least_ascending_central_series_length_eq_nilpotencyClass]

Result:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ Nat.find ⋯ = Nat.find ⋯

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

Tactic:
rw [tsub_self]

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

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

Tactic:
dsimp only

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

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

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

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

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

Tactic:
rw [tsub_self]

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

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

Tactic:
exact hH.1

Result:
no goals