refactor(NumberTheory): golf Mathlib/NumberTheory/PythagoreanTriples (#38454)

- simplifies the `Int.gcd x y = 0` branches in `gcd_dvd`, `normalize`, and `classified` using `Int.gcd_eq_zero_iff`
- shortens the zero case in `normalize` to a direct `simpa` from `PythagoreanTriple.zero`

Extracted from #38144

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/NumberTheory/PythagoreanTriples.lean

@@ -143,16 +143,11 @@ theorem even_odd_of_coprime (hc : Int.gcd x y = 1) :
 
 theorem gcd_dvd : (Int.gcd x y : ℤ) ∣ z := by
   by_cases h0 : Int.gcd x y = 0
-  · have hx : x = 0 := by
-      apply Int.natAbs_eq_zero.mp
-      apply Nat.eq_zero_of_gcd_eq_zero_left h0
-    have hy : y = 0 := by
-      apply Int.natAbs_eq_zero.mp
-      apply Nat.eq_zero_of_gcd_eq_zero_right h0
+  · obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
     have hz : z = 0 := by
       simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
         or_self_iff] using h
-    simp only [hz, dvd_zero]
+    simp [h0, hz]
   obtain ⟨k, x0, y0, _, h2, rfl, rfl⟩ :
     ∃ (k : ℕ) (x0 y0 : _), 0 < k ∧ Int.gcd x0 y0 = 1 ∧ x = x0 * k ∧ y = y0 * k :=
     Int.exists_gcd_one' (Nat.pos_of_ne_zero h0)
@@ -163,17 +158,11 @@ theorem gcd_dvd : (Int.gcd x y : ℤ) ∣ z := by
 
 theorem normalize : PythagoreanTriple (x / Int.gcd x y) (y / Int.gcd x y) (z / Int.gcd x y) := by
   by_cases h0 : Int.gcd x y = 0
-  · have hx : x = 0 := by
-      apply Int.natAbs_eq_zero.mp
-      apply Nat.eq_zero_of_gcd_eq_zero_left h0
-    have hy : y = 0 := by
-      apply Int.natAbs_eq_zero.mp
-      apply Nat.eq_zero_of_gcd_eq_zero_right h0
+  · obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
     have hz : z = 0 := by
       simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
         or_self_iff] using h
-    simp only [hx, hy, hz]
-    exact zero
+    simpa [h0, hx, hy, hz] using zero
   rcases h.gcd_dvd with ⟨z0, rfl⟩
   obtain ⟨k, x0, y0, k0, h2, rfl, rfl⟩ :
     ∃ (k : ℕ) (x0 y0 : _), 0 < k ∧ Int.gcd x0 y0 = 1 ∧ x = x0 * k ∧ y = y0 * k :=
@@ -528,12 +517,7 @@ theorem isPrimitiveClassified_of_coprime (hc : Int.gcd x y = 1) : h.IsPrimitiveC
 
 theorem classified : h.IsClassified := by
   by_cases h0 : Int.gcd x y = 0
-  · have hx : x = 0 := by
-      apply Int.natAbs_eq_zero.mp
-      apply Nat.eq_zero_of_gcd_eq_zero_left h0
-    have hy : y = 0 := by
-      apply Int.natAbs_eq_zero.mp
-      apply Nat.eq_zero_of_gcd_eq_zero_right h0
+  · obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
     use 0, 1, 0
     simp [hx, hy]
   apply h.isClassified_of_normalize_isPrimitiveClassified