y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.gcd 0 y = 1
⊢ IsPrimitiveClassified h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x = 0
⊢ IsPrimitiveClassified h
subst x
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Nat.gcd 0 (Int.natAbs y) = 1
⊢ IsPrimitiveClassified h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.gcd 0 y = 1
⊢ IsPrimitiveClassified h
change Nat.gcd 0 (Int.natAbs y) = 1 at hc
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
⊢ IsPrimitiveClassified h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Nat.gcd 0 (Int.natAbs y) = 1
⊢ IsPrimitiveClassified h
rw [Nat.gcd_zero_left (Int.natAbs y)] at hc
case inl
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
hy : y = ↑(Int.natAbs y)
⊢ IsPrimitiveClassified h

case inr
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
hy : y = -↑(Int.natAbs y)
⊢ IsPrimitiveClassified h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
⊢ IsPrimitiveClassified h
cases' Int.natAbs_eq y with hy hy
case inl
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
hy : y = ↑(Int.natAbs y)
⊢ (0 = 1 ^ 2 - 0 ^ 2 ∧ y = 2 * 1 * 0 ∨ 0 = 2 * 1 * 0 ∧ y = 1 ^ 2 - 0 ^ 2) ∧
    Int.gcd 1 0 = 1 ∧ (1 % 2 = 0 ∧ 0 % 2 = 1 ∨ 1 % 2 = 1 ∧ 0 % 2 = 0)
case inl
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
hy : y = ↑(Int.natAbs y)
⊢ IsPrimitiveClassified h
use 1, 0
case inl
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
hy : y = ↑(Int.natAbs y)
⊢ (0 = 1 ^ 2 - 0 ^ 2 ∧ ↑1 = 2 * 1 * 0 ∨ 0 = 2 * 1 * 0 ∧ ↑1 = 1 ^ 2 - 0 ^ 2) ∧
    Int.natAbs 1 = 1 ∧ (1 % 2 = 0 ∧ 0 % 2 = 1 ∨ 1 % 2 = 1 ∧ 0 % 2 = 0)
case inl
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
hy : y = ↑(Int.natAbs y)
⊢ (0 = 1 ^ 2 - 0 ^ 2 ∧ y = 2 * 1 * 0 ∨ 0 = 2 * 1 * 0 ∧ y = 1 ^ 2 - 0 ^ 2) ∧
    Int.gcd 1 0 = 1 ∧ (1 % 2 = 0 ∧ 0 % 2 = 1 ∨ 1 % 2 = 1 ∧ 0 % 2 = 0)
rw [hy, hc, Int.gcd_zero_right]
no goals
case inl
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
hy : y = ↑(Int.natAbs y)
⊢ (0 = 1 ^ 2 - 0 ^ 2 ∧ ↑1 = 2 * 1 * 0 ∨ 0 = 2 * 1 * 0 ∧ ↑1 = 1 ^ 2 - 0 ^ 2) ∧
    Int.natAbs 1 = 1 ∧ (1 % 2 = 0 ∧ 0 % 2 = 1 ∨ 1 % 2 = 1 ∧ 0 % 2 = 0)
norm_num
case inr
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
hy : y = -↑(Int.natAbs y)
⊢ (0 = 0 ^ 2 - 1 ^ 2 ∧ y = 2 * 0 * 1 ∨ 0 = 2 * 0 * 1 ∧ y = 0 ^ 2 - 1 ^ 2) ∧
    Int.gcd 0 1 = 1 ∧ (0 % 2 = 0 ∧ 1 % 2 = 1 ∨ 0 % 2 = 1 ∧ 1 % 2 = 0)
case inr
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
hy : y = -↑(Int.natAbs y)
⊢ IsPrimitiveClassified h
use 0, 1
case inr
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
hy : y = -↑(Int.natAbs y)
⊢ (0 = 0 ^ 2 - 1 ^ 2 ∧ -↑1 = 2 * 0 * 1 ∨ 0 = 2 * 0 * 1 ∧ -↑1 = 0 ^ 2 - 1 ^ 2) ∧
    Int.natAbs 1 = 1 ∧ (0 % 2 = 0 ∧ 1 % 2 = 1 ∨ 0 % 2 = 1 ∧ 1 % 2 = 0)
case inr
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
hy : y = -↑(Int.natAbs y)
⊢ (0 = 0 ^ 2 - 1 ^ 2 ∧ y = 2 * 0 * 1 ∨ 0 = 2 * 0 * 1 ∧ y = 0 ^ 2 - 1 ^ 2) ∧
    Int.gcd 0 1 = 1 ∧ (0 % 2 = 0 ∧ 1 % 2 = 1 ∨ 0 % 2 = 1 ∧ 1 % 2 = 0)
rw [hy, hc, Int.gcd_zero_left]
no goals
case inr
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.natAbs y = 1
hy : y = -↑(Int.natAbs y)
⊢ (0 = 0 ^ 2 - 1 ^ 2 ∧ -↑1 = 2 * 0 * 1 ∨ 0 = 2 * 0 * 1 ∧ -↑1 = 0 ^ 2 - 1 ^ 2) ∧
    Int.natAbs 1 = 1 ∧ (0 % 2 = 0 ∧ 1 % 2 = 1 ∨ 0 % 2 = 1 ∧ 1 % 2 = 0)
norm_num