English
Choice-free induction principle for quotients indexed by a finite type: one can reduce reasoning to a base case on a representative of each coordinate.
Русский
Бесчётная индукция по фактор-объектам, индексируемым конечным типом: можно сводить рассуждение к базовому случаю на представителе каждой координаты.
LaTeX
$$$\\forall C \\forall f, (\\forall a, C(\\llbracket a \\rrbracket)) \\Rightarrow C(q)$$$
Lean4
/-- Choice-free induction principle for quotients indexed by a finite type.
See `Quotient.induction_on_pi` for the general version assuming `Classical.choice`. -/
@[elab_as_elim]
theorem ind_fintype_pi {C : (∀ i, Quotient (S i)) → Prop} (f : ∀ a : ∀ i, α i, C (⟦a ·⟧)) (q : ∀ i, Quotient (S i)) :
C q :=
by
have {m : Multiset ι} (C : (∀ i ∈ m, Quotient (S i)) → Prop) :
∀ (_ : ∀ a : ∀ i ∈ m, α i, C (⟦a · ·⟧)) (q : ∀ i ∈ m, Quotient (S i)), C q :=
by
induction m using Quotient.ind
exact list_ind
exact this (fun q ↦ C (q · (Finset.mem_univ _))) (fun _ ↦ f _) (fun i _ ↦ q i)
