case pos
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hz : 0 < z
⊢ IsPrimitiveClassified h

case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hz : ¬0 < z
⊢ IsPrimitiveClassified h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
⊢ IsPrimitiveClassified h
by_cases hz : 0 < z
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hz : ¬0 < z
h' : PythagoreanTriple x y (-z)
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hz : ¬0 < z
⊢ IsPrimitiveClassified h
have h' : PythagoreanTriple x y (-z) := by simpa [PythagoreanTriple, neg_mul_neg] using h.eq
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hz : ¬0 < z
h' : PythagoreanTriple x y (-z)
⊢ 0 < -z
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hz : ¬0 < z
h' : PythagoreanTriple x y (-z)
⊢ IsPrimitiveClassified h
apply h'.isPrimitiveClassified_of_coprime_of_pos hc
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hz : ¬0 < z
h' : PythagoreanTriple x y (-z)
⊢ 0 ≤ -z
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hz : ¬0 < z
h' : PythagoreanTriple x y (-z)
⊢ 0 < -z
apply lt_of_le_of_ne _ (h'.ne_zero_of_coprime hc).symm
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hz : ¬0 < z
h' : PythagoreanTriple x y (-z)
⊢ 0 ≤ -z
exact le_neg.mp (not_lt.mp hz)
no goals
case pos
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hz : 0 < z
⊢ IsPrimitiveClassified h
exact h.isPrimitiveClassified_of_coprime_of_pos hc hz
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hz : ¬0 < z
⊢ PythagoreanTriple x y (-z)
simpa [PythagoreanTriple, neg_mul_neg] using h.eq