English
There is a choice-free induction principle for quotients indexed by a list: to prove a property for all quotients on a list, it suffices to prove it for a canonical constructor built from representatives.
Русский
Существует индуктивность без выбора для фактор-объектов, индексируемых списком: чтобы доказать свойство для всех факторов на списке, достаточно доказать его для канонического конструктора из представлений.
LaTeX
$$$\\forall l, \\forall C, (\\forall a, C (\\llbracket a \\cdot \\cdot \\rrbracket)) \\Rightarrow \\forall q, C(q)$$$
Lean4
/-- Choice-free induction principle for quotients indexed by a `List`. -/
@[elab_as_elim]
theorem list_ind {l : List ι} {C : (∀ i ∈ l, Quotient (S i)) → Prop} (f : ∀ a : ∀ i ∈ l, α i, C (⟦a · ·⟧))
(q : ∀ i ∈ l, Quotient (S i)) : C q :=
match l with
| [] => cast (congr_arg _ (funext₂ nofun)) (f nofun)
| i :: l => by
rw [← List.Pi.cons_eta q]
induction List.Pi.head q using Quotient.ind with
| _ a
refine @list_ind _ (fun q ↦ C (List.Pi.cons _ _ ⟦a⟧ q)) ?_ (List.Pi.tail q)
intro as
rw [List.Pi.cons_map a as (fun i ↦ Quotient.mk (S i))]
exact f _
