English
If x, y, z form a Pythagorean triple, then gcd(x, y) divides z.
Русский
Если x, y, z — Пифагорова тройка, то НОД(x, y) делит z.
LaTeX
$$$\gcd(x,y) \mid z$$$
Lean4
theorem gcd_dvd : (Int.gcd x y : ℤ) ∣ z := by
by_cases h0 : Int.gcd x y = 0
· have hx : x = 0 := by
apply Int.natAbs_eq_zero.mp
apply Nat.eq_zero_of_gcd_eq_zero_left h0
have hy : y = 0 := by
apply Int.natAbs_eq_zero.mp
apply Nat.eq_zero_of_gcd_eq_zero_right h0
have hz : z = 0 := by simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero, or_self_iff] using h
simp only [hz, dvd_zero]
obtain ⟨k, x0, y0, _, h2, rfl, rfl⟩ : ∃ (k : ℕ) (x0 y0 : _), 0 < k ∧ Int.gcd x0 y0 = 1 ∧ x = x0 * k ∧ y = y0 * k :=
Int.exists_gcd_one' (Nat.pos_of_ne_zero h0)
rw [Int.gcd_mul_right, h2, Int.natAbs_natCast, one_mul]
rw [← Int.pow_dvd_pow_iff two_ne_zero, sq z, ← h.eq]
rw [(by ring : x0 * k * (x0 * k) + y0 * k * (y0 * k) = (k : ℤ) ^ 2 * (x0 * x0 + y0 * y0))]
exact dvd_mul_right _ _
