English
If 2m = x^2 + y^2 for integers m,x,y, then m = ((x - y)/2)^2 + ((x + y)/2)^2.
Русский
Если 2m = x^2 + y^2 для целых x,y, то m = ((x - y)/2)^2 + ((x + y)/2)^2.
LaTeX
$$$2m = x^2 + y^2 \quad\Rightarrow\quad m = \left(\frac{x-y}{2}\right)^2 + \left(\frac{x+y}{2}\right)^2$$$
Lean4
theorem sq_add_sq_of_two_mul_sq_add_sq {m x y : ℤ} (h : 2 * m = x ^ 2 + y ^ 2) :
m = ((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2 :=
have : Even (x ^ 2 + y ^ 2) := by simp [← h]
mul_right_injective₀ (show (2 * 2 : ℤ) ≠ 0 by decide) <|
calc
2 * 2 * m = (x - y) ^ 2 + (x + y) ^ 2 := by rw [mul_assoc, h]; ring
_ = (2 * ((x - y) / 2)) ^ 2 + (2 * ((x + y) / 2)) ^ 2 := by
rw [Int.mul_ediv_cancel' _, Int.mul_ediv_cancel' _] <;> simpa [sq, parity_simps, ← even_iff_two_dvd]
_ = 2 * 2 * (((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2) := by nlinarith
