Lean 4: strong induction over a class of groups via `P : (H : Type u) → [Group H] → Prop`

To prove something for every finite group in a subgroup-closed class (nilpotent, supersolvable, ...) by induction on |G|, make the class a parameter (P : (H : Type u) → [Group H] → Prop) with hsub : ∀ (H : Type u) [Group H], P H → ∀ K : Subgroup H, P K. Then state ∀ n, ∀ (G : Type u) [Group G] [Finite G], P G → Nat.card G = n → ... and use induction n using Nat.strong_induction_on. P K elaborates with K's group instance automatically. Instantiate with (fun H _ ↦ Group.IsNilpotent H) and (fun H _ _ K ↦ inferInstance). The proper subgroup step is Subgroup.card_lt_of_lt (lt_top_iff_ne_top.2 hI) after rw [← Subgroup.card_top (G := G)]. Keep the universe of G fixed (Type u); the representation space can live in any universe v.