English
If pair x y = pair x' y', then x = x' and y = y'.
Русский
Если пары x,y и x',y' равны, то x = x' и y = y'.
LaTeX
$$$\\forall x,y,x',y',\\ pair x y = pair x' y' \\Rightarrow x = x' \\land y = y'$$$
Lean4
theorem pair_injective : Function.Injective2 pair :=
by
intro x x' y y' H
simp_rw [ZFSet.ext_iff, pair, mem_pair] at H
obtain rfl : x = x' := And.left <| by simpa [or_and_left] using (H { x }).1 (Or.inl rfl)
have he : y = x → y = y' := by
rintro rfl
simpa [eq_comm] using H { y, y' }
have hx := H { x, y }
simp_rw [pair_eq_singleton_iff, true_and, or_true, true_iff] at hx
refine ⟨rfl, hx.elim he fun hy ↦ Or.elim ?_ he id⟩
simpa using ZFSet.ext_iff.1 hy y
