case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
⊢ IsClassified h

case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬Int.gcd x y = 0
⊢ IsClassified h
x y z : ℤ
h : PythagoreanTriple x y z
⊢ IsClassified h
by_cases h0 : Int.gcd x y = 0
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬Int.gcd x y = 0
⊢ IsPrimitiveClassified (_ : 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
⊢ IsClassified h
apply h.isClassified_of_normalize_isPrimitiveClassified
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬Int.gcd x y = 0
⊢ Int.gcd (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) = 1
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬Int.gcd x y = 0
⊢ IsPrimitiveClassified (_ : PythagoreanTriple (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) (z / ↑(Int.gcd x y)))
apply h.normalize.isPrimitiveClassified_of_coprime
no goals
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬Int.gcd x y = 0
⊢ Int.gcd (x / ↑(Int.gcd x y)) (y / ↑(Int.gcd x y)) = 1
apply Int.gcd_div_gcd_div_gcd (Nat.pos_of_ne_zero h0)
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
⊢ IsClassified h
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
⊢ IsClassified h
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
⊢ IsClassified h
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
⊢ IsClassified h
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
⊢ (x = 0 * (1 ^ 2 - 0 ^ 2) ∧ y = 0 * (2 * 1 * 0) ∨ x = 0 * (2 * 1 * 0) ∧ y = 0 * (1 ^ 2 - 0 ^ 2)) ∧ Int.gcd 1 0 = 1
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
hy : y = 0
⊢ IsClassified h
use 0, 1, 0
no goals
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : Int.gcd x y = 0
hx : x = 0
hy : y = 0
⊢ (x = 0 * (1 ^ 2 - 0 ^ 2) ∧ y = 0 * (2 * 1 * 0) ∨ x = 0 * (2 * 1 * 0) ∧ y = 0 * (1 ^ 2 - 0 ^ 2)) ∧ Int.gcd 1 0 = 1
field_simp [hx, hy]
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