-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem isPrimitiveClassified_of_coprime_of_zero_left (hc : Int.gcd x y = 1) (hx : x = 0) :
    h.IsPrimitiveClassified

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x = 0
⊢ h.IsPrimitiveClassified

Tactic:
subst x

Result:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.gcd 0 y = 1
⊢ h.IsPrimitiveClassified

Proof state:
case h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -↑y.natAbs
⊢ (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)

Tactic:
decide

Result:
no goals

Proof state:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.gcd 0 y = 1
⊢ h.IsPrimitiveClassified

Tactic:
change Nat.gcd 0 (Int.natAbs y) = 1 at hc

Result:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Nat.gcd 0 y.natAbs = 1
⊢ h.IsPrimitiveClassified

Proof state:
case h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = ↑y.natAbs
⊢ (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)

Tactic:
decide

Result:
no goals

Proof state:
case h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -↑y.natAbs
⊢ (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)

Tactic:
rw [hy, hc, Int.gcd_zero_left]

Result:
case h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -↑y.natAbs
⊢ (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)

Proof state:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
⊢ h.IsPrimitiveClassified

Tactic:
rcases Int.natAbs_eq y with hy | hy

Result:
case inl
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = ↑y.natAbs
⊢ h.IsPrimitiveClassified

case inr
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -↑y.natAbs
⊢ h.IsPrimitiveClassified

Proof state:
case inl
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = ↑y.natAbs
⊢ h.IsPrimitiveClassified

Tactic:
use 1, 0

Result:
case h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = ↑y.natAbs
⊢ (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)

Proof state:
case h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = ↑y.natAbs
⊢ (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)

Tactic:
rw [hy, hc, Int.gcd_zero_right]

Result:
case h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = ↑y.natAbs
⊢ (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)

Proof state:
case inr
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -↑y.natAbs
⊢ h.IsPrimitiveClassified

Tactic:
use 0, 1

Result:
case h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -↑y.natAbs
⊢ (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)

Proof state:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Nat.gcd 0 y.natAbs = 1
⊢ h.IsPrimitiveClassified

Tactic:
rw [Nat.gcd_zero_left (Int.natAbs y)] at hc

Result:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
⊢ h.IsPrimitiveClassified