English
There is a custom induction principle for fintypes: base case for subsingleton, induction step for nontrivial types using a strong induction on card α.
Русский
Существует кастомная индукция для конечных типов: базовый случай для подмножеств, переход к не-тривиальным типам через сильную индукцию по кардинальности α.
LaTeX
$$$P(α) \text{ holds by } Fintype.card\;\text{strong_induction_on}$$$
Lean4
/-- A custom induction principle for fintypes. The base case is a subsingleton type,
and the induction step is for non-trivial types, and one can assume the hypothesis for
smaller types (via `Fintype.card`).
The major premise is `Fintype α`, so to use this with the `induction` tactic you have to give a name
to that instance and use that name.
-/
@[elab_as_elim]
theorem induction_subsingleton_or_nontrivial {P : ∀ (α) [Fintype α], Prop} (α : Type*) [Fintype α]
(hbase : ∀ (α) [Fintype α] [Subsingleton α], P α)
(hstep : ∀ (α) [Fintype α] [Nontrivial α], (∀ (β) [Fintype β], Fintype.card β < Fintype.card α → P β) → P α) :
P α := by
obtain ⟨n, hn⟩ : ∃ n, Fintype.card α = n := ⟨Fintype.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 (Fintype.card β) hlt _ rfl
