English
A variant of induction on a quotient taking s as implicit argument; if p holds for mk'' a, then p holds for any q.
Русский
Вариант индукции по квату с неявным аргументом s; если p верно для mk'' a, тогда p верно и для любого q.
LaTeX
$$$\\forall q:\\, \\operatorname{Quotient}(s_1),\\ (\\forall a:\\, \\alpha, p(\\mathrm{mk}'' a)) \\Rightarrow p(q)$$$
Lean4
/-- A version of `Quotient.inductionOn` taking `{s : Setoid α}` as an implicit argument instead
of an instance argument. -/
@[elab_as_elim]
protected theorem inductionOn' {p : Quotient s₁ → Prop} (q : Quotient s₁) (h : ∀ a, p (Quotient.mk'' a)) : p q :=
Quotient.inductionOn q h
