case inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hzpos : 0 < z
h1 : x % 2 = 0 ∧ y % 2 = 1
⊢ IsPrimitiveClassified h

case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ IsPrimitiveClassified h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hzpos : 0 < z
⊢ IsPrimitiveClassified h
cases' h.even_odd_of_coprime hc with h1 h2
case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd y x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ IsPrimitiveClassified h
case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ IsPrimitiveClassified h
rw [Int.gcd_comm] at hc
case inr.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd y x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
m n : ℤ
H :
  (y = m ^ 2 - n ^ 2 ∧ x = 2 * m * n ∨ y = 2 * m * n ∧ x = m ^ 2 - n ^ 2) ∧
    Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ IsPrimitiveClassified h
case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd y x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ IsPrimitiveClassified h
obtain ⟨m, n, H⟩ := h.symm.isPrimitiveClassified_of_coprime_of_odd_of_pos hc h2.left hzpos
case inr.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd y x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
m n : ℤ
H :
  (y = m ^ 2 - n ^ 2 ∧ x = 2 * m * n ∨ y = 2 * m * n ∧ x = m ^ 2 - n ^ 2) ∧
    Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
    Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
case inr.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd y x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
m n : ℤ
H :
  (y = m ^ 2 - n ^ 2 ∧ x = 2 * m * n ∨ y = 2 * m * n ∧ x = m ^ 2 - n ^ 2) ∧
    Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ IsPrimitiveClassified h
use m, n
no goals
case inr.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd y x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
m n : ℤ
H :
  (y = m ^ 2 - n ^ 2 ∧ x = 2 * m * n ∨ y = 2 * m * n ∧ x = m ^ 2 - n ^ 2) ∧
    Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
    Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
tauto
no goals
case inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hzpos : 0 < z
h1 : x % 2 = 0 ∧ y % 2 = 1
⊢ IsPrimitiveClassified h
exact h.isPrimitiveClassified_of_coprime_of_odd_of_pos hc h1.right hzpos