English
A version of two-argument induction on quotients with implicit s₁,s₂ arguments.
Русский
Версия двуместной индукции по кватам с неявными s₁, s₂ аргументами.
LaTeX
$$$(\\forall q_1:\\, \\operatorname{Quotient}(s_1))(\\forall q_2:\\, \\operatorname{Quotient}(s_2), p q_1 q_2)$$$
Lean4
/-- A version of `Quotient.inductionOn₂` taking `{s₁ : Setoid α} {s₂ : Setoid β}` as implicit
arguments instead of instance arguments. -/
@[elab_as_elim]
protected theorem inductionOn₂' {p : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂)
(h : ∀ a₁ a₂, p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) : p q₁ q₂ :=
Quotient.inductionOn₂ q₁ q₂ h
