no goals
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
⊢ k * x * (k * x) + k * y * (k * y) = k ^ 2 * (x * x + y * y)
ring
no goals
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
⊢ k ^ 2 * (x * x + y * y) = k ^ 2 * (z * z)
rw [h.eq]
no goals
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
⊢ k ^ 2 * (z * z) = k * z * (k * z)
ring