chore(Data/PNat): deprecate gcd_eq_left (#31606)

Author: euprunin

Mathlib/Data/PNat/Prime.lean

@@ -253,12 +253,7 @@ theorem Coprime.gcd_mul (k : ℕ+) {m n : ℕ+} (h : m.Coprime n) :
   rw [← coprime_coe] at h; apply eq
   simp only [gcd_coe, mul_coe]; apply Nat.Coprime.gcd_mul k h
 
-theorem gcd_eq_left {m n : ℕ+} : m ∣ n → m.gcd n = m := by
-  rw [dvd_iff]
-  intro h
-  apply eq
-  simp only [gcd_coe]
-  apply Nat.gcd_eq_left h
+@[deprecated (since := "2025-11-14")] alias ⟨_, gcd_eq_left⟩ := gcd_eq_left_iff_dvd
 
 theorem Coprime.pow {m n : ℕ+} (k l : ℕ) (h : m.Coprime n) : (m ^ k : ℕ).Coprime (n ^ l) := by
   rw [← coprime_coe] at *; apply Nat.Coprime.pow; apply h