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

case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬Int.gcd x y = 0
⊢ PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (z / ↑(Int.gcd x y))
x y z : ℤ
h : PythagoreanTriple x y z
⊢ PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (z / ↑(Int.gcd x y))
by_cases h0 : Int.gcd x y = 0
case neg.intro
x y : ℤ
h0 : ¬Int.gcd x y = 0
z0 : ℤ
h : PythagoreanTriple x y (↑(Int.gcd x y) * z0)
⊢ PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (↑(Int.gcd x y) * z0 / ↑(Int.gcd x y))
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬Int.gcd x y = 0
⊢ PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (z / ↑(Int.gcd x y))
rcases h.gcd_dvd with ⟨z0, rfl⟩
case neg.intro.intro.intro.intro.intro.intro.intro
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : Int.gcd x0 y0 = 1
h0 : ¬Int.gcd (x0 * ↑k) (y0 * ↑k) = 0
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑(Int.gcd (x0 * ↑k) (y0 * ↑k)) * z0)
⊢ PythagoreanTriple (x0 * ↑k / ↑(Int.gcd (x0 * ↑k) (y0 * ↑k))) (y0 * ↑k / ↑(Int.gcd (x0 * ↑k) (y0 * ↑k)))
    (↑(Int.gcd (x0 * ↑k) (y0 * ↑k)) * z0 / ↑(Int.gcd (x0 * ↑k) (y0 * ↑k)))
case neg.intro
x y : ℤ
h0 : ¬Int.gcd x y = 0
z0 : ℤ
h : PythagoreanTriple x y (↑(Int.gcd x y) * z0)
⊢ PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (↑(Int.gcd x y) * z0 / ↑(Int.gcd x y))
obtain ⟨k, x0, y0, k0, 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)
case neg.intro.intro.intro.intro.intro.intro.intro
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : Int.gcd x0 y0 = 1
h0 : ¬Int.gcd (x0 * ↑k) (y0 * ↑k) = 0
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑(Int.gcd (x0 * ↑k) (y0 * ↑k)) * z0)
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑(Int.gcd (x0 * ↑k) (y0 * ↑k))) (y0 * ↑k / ↑(Int.gcd (x0 * ↑k) (y0 * ↑k)))
    (↑(Int.gcd (x0 * ↑k) (y0 * ↑k)) * z0 / ↑(Int.gcd (x0 * ↑k) (y0 * ↑k)))
case neg.intro.intro.intro.intro.intro.intro.intro
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : Int.gcd x0 y0 = 1
h0 : ¬Int.gcd (x0 * ↑k) (y0 * ↑k) = 0
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑(Int.gcd (x0 * ↑k) (y0 * ↑k)) * z0)
⊢ PythagoreanTriple (x0 * ↑k / ↑(Int.gcd (x0 * ↑k) (y0 * ↑k))) (y0 * ↑k / ↑(Int.gcd (x0 * ↑k) (y0 * ↑k)))
    (↑(Int.gcd (x0 * ↑k) (y0 * ↑k)) * z0 / ↑(Int.gcd (x0 * ↑k) (y0 * ↑k)))
have hk : (k : ℤ) ≠ 0 := by
  norm_cast
  rwa [pos_iff_ne_zero] at k0
case neg.intro.intro.intro.intro.intro.intro.intro
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : Int.gcd x0 y0 = 1
h0 : ¬Int.gcd (x0 * ↑k) (y0 * ↑k) = 0
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑k * z0)
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑k) (y0 * ↑k / ↑k) (↑k * z0 / ↑k)
case neg.intro.intro.intro.intro.intro.intro.intro
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : Int.gcd x0 y0 = 1
h0 : ¬Int.gcd (x0 * ↑k) (y0 * ↑k) = 0
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑(Int.gcd (x0 * ↑k) (y0 * ↑k)) * z0)
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑(Int.gcd (x0 * ↑k) (y0 * ↑k))) (y0 * ↑k / ↑(Int.gcd (x0 * ↑k) (y0 * ↑k)))
    (↑(Int.gcd (x0 * ↑k) (y0 * ↑k)) * z0 / ↑(Int.gcd (x0 * ↑k) (y0 * ↑k)))
rw [Int.gcd_mul_right, h2, Int.natAbs_ofNat, one_mul] at h⊢
case neg.intro.intro.intro.intro.intro.intro.intro
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : Int.gcd x0 y0 = 1
h0 : ¬Int.gcd (x0 * ↑k) (y0 * ↑k) = 0
h : PythagoreanTriple x0 y0 z0
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑k) (y0 * ↑k / ↑k) (↑k * z0 / ↑k)
case neg.intro.intro.intro.intro.intro.intro.intro
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : Int.gcd x0 y0 = 1
h0 : ¬Int.gcd (x0 * ↑k) (y0 * ↑k) = 0
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑k * z0)
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑k) (y0 * ↑k / ↑k) (↑k * z0 / ↑k)
rw [mul_comm x0, mul_comm y0, mul_iff k hk] at h
no goals
case neg.intro.intro.intro.intro.intro.intro.intro
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : Int.gcd x0 y0 = 1
h0 : ¬Int.gcd (x0 * ↑k) (y0 * ↑k) = 0
h : PythagoreanTriple x0 y0 z0
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑k) (y0 * ↑k / ↑k) (↑k * z0 / ↑k)
rwa [Int.mul_ediv_cancel _ hk, Int.mul_ediv_cancel _ hk, Int.mul_ediv_cancel_left _ hk]
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
⊢ PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (z / ↑(Int.gcd x y))
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
⊢ PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (z / ↑(Int.gcd x y))
have hx : x = 0 := by
  apply Int.natAbs_eq_zero.mp
  apply Nat.eq_zero_of_gcd_eq_zero_left h0
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
hy : y = 0
⊢ PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (z / ↑(Int.gcd x y))
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
⊢ PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (z / ↑(Int.gcd x y))
have hy : y = 0 := by
  apply Int.natAbs_eq_zero.mp
  apply Nat.eq_zero_of_gcd_eq_zero_right h0
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
hy : y = 0
hz : z = 0
⊢ PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (z / ↑(Int.gcd x y))
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
hy : y = 0
⊢ PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (z / ↑(Int.gcd x y))
have hz : z = 0 := by
  simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, MulZeroClass.mul_zero,
    or_self_iff] using h
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
hy : y = 0
hz : z = 0
⊢ PythagoreanTriple (0 / ↑(Int.gcd 0 0)) (0 / ↑(Int.gcd 0 0)) (0 / ↑(Int.gcd 0 0))
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
hy : y = 0
hz : z = 0
⊢ PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (z / ↑(Int.gcd x y))
simp only [hx, hy, hz, Int.zero_div]
no goals
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
hy : y = 0
hz : z = 0
⊢ PythagoreanTriple (0 / ↑(Int.gcd 0 0)) (0 / ↑(Int.gcd 0 0)) (0 / ↑(Int.gcd 0 0))
exact zero
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
⊢ Int.natAbs x = 0
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
⊢ x = 0
apply Int.natAbs_eq_zero.mp
no goals
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
⊢ Int.natAbs x = 0
apply Nat.eq_zero_of_gcd_eq_zero_left h0
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
⊢ Int.natAbs y = 0
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
⊢ y = 0
apply Int.natAbs_eq_zero.mp
no goals
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
⊢ Int.natAbs y = 0
apply Nat.eq_zero_of_gcd_eq_zero_right h0
no goals
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
hy : y = 0
⊢ z = 0
simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, MulZeroClass.mul_zero,
  or_self_iff] using h
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : Int.gcd x0 y0 = 1
h0 : ¬Int.gcd (x0 * ↑k) (y0 * ↑k) = 0
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑(Int.gcd (x0 * ↑k) (y0 * ↑k)) * z0)
⊢ ¬k = 0
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : Int.gcd x0 y0 = 1
h0 : ¬Int.gcd (x0 * ↑k) (y0 * ↑k) = 0
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑(Int.gcd (x0 * ↑k) (y0 * ↑k)) * z0)
⊢ ↑k ≠ 0
norm_cast
no goals
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : Int.gcd x0 y0 = 1
h0 : ¬Int.gcd (x0 * ↑k) (y0 * ↑k) = 0
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑(Int.gcd (x0 * ↑k) (y0 * ↑k)) * z0)
⊢ ¬k = 0
rwa [pos_iff_ne_zero] at k0