English
Applying unpair to the result of pairing a and b gives back the original pair: unpair(pair a b) = (a,b).
Русский
Применение unpair к пары a и b восстанавливает исходную пару: unpair(pair a b) = (a,b).
LaTeX
$$$ \forall a,b \in \mathbb{N}, \; \operatorname{unpair}(\operatorname{pair}(a,b)) = (a,b). $$$
Lean4
@[simp]
theorem unpair_pair (a b : ℕ) : unpair (pair a b) = (a, b) :=
by
dsimp only [pair]; split_ifs with h
· show unpair (b * b + a) = (a, b)
have be : sqrt (b * b + a) = b := sqrt_add_eq _ (le_trans (le_of_lt h) (Nat.le_add_left _ _))
simp [unpair, be, Nat.add_sub_cancel_left, h]
· show unpair (a * a + a + b) = (a, b)
have ae : sqrt (a * a + (a + b)) = a := by
rw [sqrt_add_eq]
exact Nat.add_le_add_left (le_of_not_gt h) _
simp [unpair, ae, Nat.add_assoc, Nat.add_sub_cancel_left]
