feat(SetTheory/Cardinal): strong induction on Nat.card for finite types

Mathlib/GroupTheory/Nilpotent.lean

@@ -1207,23 +1207,15 @@ variable {G : Type*} [hG : Group G]
 /-- A p-group is nilpotent -/
 theorem IsPGroup.isNilpotent [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : IsPGroup p G) :
     IsNilpotent G := by
-  cases nonempty_fintype G
-  classical
-    revert hG
-    apply @Fintype.induction_subsingleton_or_nontrivial _ G _
-    · intro _ _ _ _
-      infer_instance
-    · intro G _ _ ih _ h
-      have hcq : Fintype.card (G ⧸ center G) < Fintype.card G := by
-        simp only [← Nat.card_eq_fintype_card]
-        rw [card_eq_card_quotient_mul_card_subgroup (center G)]
-        simp only [Nat.card_eq_fintype_card]
-        apply lt_mul_of_one_lt_right
-        · exact Fintype.card_pos_iff.mpr One.instNonempty
-        · simp only [← Nat.card_eq_fintype_card]
-          exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)
-      have hnq : IsNilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G))
-      exact of_quotient_center_nilpotent hnq
+  induction G using Finite.induction_subsingleton_or_nontrivial generalizing hG with
+  | hbase => infer_instance
+  | hstep G ih =>
+    have hcq : Nat.card (G ⧸ center G) < Nat.card G := by
+      rw [card_eq_card_quotient_mul_card_subgroup (center G)]
+      apply lt_mul_of_one_lt_right Nat.card_pos
+      exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)
+    have hnq : IsNilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G))
+    exact of_quotient_center_nilpotent hnq
 
 variable [Finite G]
 

Mathlib/SetTheory/Cardinal/NatCard.lean

@@ -146,6 +146,24 @@ theorem card_subtype_lt [Finite α] {p : α → Prop} {x : α} (hx : ¬p x) :
   have := Fintype.ofFinite α
   simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx
 
+/-- A custom induction principle for finite types, by strong induction on `Nat.card`:
+the base case is a subsingleton type, and the induction step is for nontrivial types,
+where one can assume the hypothesis for all types of smaller cardinality. -/
+@[elab_as_elim]
+theorem induction_subsingleton_or_nontrivial {P : Type* → Prop} (α) [Finite α]
+    (hbase : ∀ (α) [Finite α] [Subsingleton α], P α)
+    (hstep : ∀ (α) [Finite α] [Nontrivial α],
+      (∀ (β) [Finite β], Nat.card β < Nat.card α → P β) → P α) :
+    P α := by
+  obtain ⟨n, hn⟩ : ∃ n, Nat.card α = n := ⟨Nat.card α, rfl⟩
+  induction n using Nat.strong_induction_on generalizing α with | _ n ih
+  rcases subsingleton_or_nontrivial α with hsing | hnontriv
+  · apply hbase
+  · apply hstep
+    intro β _ hlt
+    rw [hn] at hlt
+    exact ih (Nat.card β) hlt _ rfl
+
 end Finite
 
 namespace ENat