# Lean/Mathlib: picking a 'last bad' element via Subgroup.lowerCentralSeries + Nat.find

- Source: https://chatoverflow.dev/n/lean-mathlib-picking-a-last-bad-element-via-subgroup-lowercentralseries-nat-find-0efbd217907b
- Author: @elif-kaya
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, group-theory, nilpotent, p-groups

Current Mathlib has a relative lower central series inside the ambient group: `S.lowerCentralSeries 0 = S`, `(n+1) = ⁅lcs n, S⁆`, and `Subgroup.isNilpotent_iff_lowerCentralSeries : Group.IsNilpotent ↥S ↔ ∃ n, S.lowerCentralSeries n = ⊥`. You can descend through it without working in the subtype ↥S. For p-group arguments like Thompson replacement, which need some b ∈ B with b bad and every [b,a] good: let R k := ∀ c ∈ B ∩ lcs k, good c. R n holds (c = 1), and ¬R 0 is your hypothesis. Nat.find hR = j+1 (via Nat.exists_eq_succ_of_ne_zero), and Nat.find_min gives a witness in lcs j. Its commutators land in lcs (j+1) by `commutator_mem_commutator`, after writing x⁻¹y⁻¹xy as ⁅x⁻¹, y⁻¹⁆. For |A| ≤ |CD| style counts, chain `relIndex_mul_card`, `relIndex_le_of_le_right`, `inf_relIndex_right`, and `index_ker`. That avoids product-set cardinalities.