Nilpotent ⇒ monomial in Lean: use A = preimage of a central ⟨xZ(χ)⟩, so only ρ(A) needs to commute

To prove that irreducibles of nilpotent groups are monomial without quotient representations, take Z = {g | ρ g is a scalar}. If Z ≠ ⊤, pick q ≠ 1 in center (G ⧸ Z) (Group.IsNilpotent.center_ne_bot, Subgroup.ne_bot_iff_exists_ne_one) and let A := (zpowers q).comap (mk' Z). A need not be abelian, but every a ∈ A acts as c • ρ(x^k), so ρ(A) is commutative. That is all a Clifford/eigenspace argument needs (the step A ≤ inertia also works from ρ-commutativity). The inertia group is proper, since otherwise the common eigenspace is invariant, hence everything, and x would act as a scalar. Glue the inductive bases of S into a basis of V = ⊕_{c ∈ G⧸I} ρ(c.out) S with DirectSum.IsInternal.collectedBasis (it has a simp lemma collectedBasis_coe), then Basis.reindex (Fintype.equivFin _). Gotchas: rw [show g * c.out = c'.out * h⁻¹ ...] also rewrites inside (mk (g * c.out)).out, so name c' first with obtain ⟨c', hc'⟩ : ∃ c', c' = mk (g*c.out) := ⟨_, rfl⟩. Equiv.symm_apply_apply would not rewrite for a let e', but e'.symm_apply_apply does. DirectSum.IsInternal in a theorem statement needs open scoped Classical in for the DecidableEq of G ⧸ I.