-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem gcd_dvd : (Int.gcd x y : ℤ) ∣ z

Proof state:
case neg.intro.intro.intro.intro.intro.intro
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑k ^ 2 ∣ x0 * ↑k * (x0 * ↑k) + y0 * ↑k * (y0 * ↑k)

Tactic:
rw [(by ring : x0 * k * (x0 * k) + y0 * k * (y0 * k) = (k : ℤ) ^ 2 * (x0 * x0 + y0 * y0))]

Result:
case neg.intro.intro.intro.intro.intro.intro
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑k ^ 2 ∣ ↑k ^ 2 * (x0 * x0 + y0 * y0)

Proof state:
case neg.intro.intro.intro.intro.intro.intro
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑((x0 * ↑k).gcd (y0 * ↑k)) ∣ z

Tactic:
rw [Int.gcd_mul_right, h2, Int.natAbs_ofNat, one_mul]

Result:
case neg.intro.intro.intro.intro.intro.intro
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑k ∣ z

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ y = 0

Tactic:
apply Int.natAbs_eq_zero.mp

Result:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ y.natAbs = 0

Proof state:
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ x0 * ↑k * (x0 * ↑k) + y0 * ↑k * (y0 * ↑k) = ↑k ^ 2 * (x0 * x0 + y0 * y0)

Tactic:
ring

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
⊢ ↑(x.gcd y) ∣ z

Tactic:
by_cases h0 : Int.gcd x y = 0

Result:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ ↑(x.gcd y) ∣ z

case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ ↑(x.gcd y) ∣ z

Proof state:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ ↑(x.gcd y) ∣ z

Tactic:
have hy : y = 0 := by
  apply Int.natAbs_eq_zero.mp
  apply Nat.eq_zero_of_gcd_eq_zero_right h0

Result:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ ↑(x.gcd y) ∣ z

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ y.natAbs = 0

Tactic:
apply Nat.eq_zero_of_gcd_eq_zero_right h0

Result:
no goals

Proof state:
case neg.intro.intro.intro.intro.intro.intro
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑k ∣ z

Tactic:
rw [← Int.pow_dvd_pow_iff two_ne_zero, sq z, ← h.eq]

Result:
case neg.intro.intro.intro.intro.intro.intro
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑k ^ 2 ∣ x0 * ↑k * (x0 * ↑k) + y0 * ↑k * (y0 * ↑k)

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ x.natAbs = 0

Tactic:
apply Nat.eq_zero_of_gcd_eq_zero_left h0

Result:
no goals

Proof state:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ ↑(x.gcd y) ∣ z

Tactic:
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)

Result:
case neg.intro.intro.intro.intro.intro.intro
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑((x0 * ↑k).gcd (y0 * ↑k)) ∣ z

Proof state:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
hz : z = 0
⊢ ↑(x.gcd y) ∣ z

Tactic:
simp only [hz, dvd_zero]

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ x = 0

Tactic:
apply Int.natAbs_eq_zero.mp

Result:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ x.natAbs = 0

Proof state:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ ↑(x.gcd y) ∣ z

Tactic:
have hz : z = 0 := by
  simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
    or_self_iff] using h

Result:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
hz : z = 0
⊢ ↑(x.gcd y) ∣ z

Proof state:
case neg.intro.intro.intro.intro.intro.intro
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑k ^ 2 ∣ ↑k ^ 2 * (x0 * x0 + y0 * y0)

Tactic:
exact dvd_mul_right _ _

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ z = 0

Tactic:
simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
  or_self_iff] using h

Result:
no goals

Proof state:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ ↑(x.gcd y) ∣ z

Tactic:
have hx : x = 0 := by
  apply Int.natAbs_eq_zero.mp
  apply Nat.eq_zero_of_gcd_eq_zero_left h0

Result:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ ↑(x.gcd y) ∣ z