English
For any f : Sym2 α → Sym2 β → Prop, if f holds for all Sym2.mk a1 a2 and Sym2.mk b1 b2, then f i j for any i,j.
Русский
Для любого f : Sym2 α → Sym2 β → Prop, если выполняется для всех пар (a1,a2) и (b1,b2), тогда f i j для любых i,j.
LaTeX
$$$$ \forall f : Sym2\alpha \to Sym2\beta \to Prop, (\forall a_1 a_2 b_1 b_2, f(\mathrm{Sym2.mk}\{fst := a_1, snd := a_2\}) (\mathrm{Sym2.mk}\{fst := b_1, snd := b_2\})) \to f\,i\,j. $$$$
Lean4
@[elab_as_elim]
protected theorem inductionOn₂ {f : Sym2 α → Sym2 β → Prop} (i : Sym2 α) (j : Sym2 β)
(hf : ∀ a₁ a₂ b₁ b₂, f s(a₁, a₂) s(b₁, b₂)) : f i j :=
Quot.induction_on₂ i j <| by
intro ⟨a₁, a₂⟩ ⟨b₁, b₂⟩
exact hf _ _ _ _
