case refine_1
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), upperCentralSeries G n = ⊤ → ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤

case refine_2
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsAscendingCentralSeries H ∧ H n = ⊤) → upperCentralSeries G n = ⊤
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) = nilpotencyClass G
refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
case refine_1
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤
case refine_1
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), upperCentralSeries G n = ⊤ → ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤
intro n hn
no goals
case refine_1
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤
exact ⟨upperCentralSeries G, upperCentralSeries_isAscendingCentralSeries G, hn⟩
case refine_2.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ upperCentralSeries G n = ⊤
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsAscendingCentralSeries H ∧ H n = ⊤) → upperCentralSeries G n = ⊤
rintro n ⟨H, ⟨hH, hn⟩⟩
case refine_2.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n
case refine_2.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ upperCentralSeries G n = ⊤
rw [← top_le_iff, ← hn]
no goals
case refine_2.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n
exact ascending_central_series_le_upper H hH n