chore: golf separable_iff_squarefree (#10236)

In fact this theorem admits a proof without using any lemmas introduced in #10170.

For this I had to remove some redundant [GCDMonoid R] assumptions in RingTheory/PrincipalIdealDomain.lean.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/FieldTheory/Perfect.lean

@@ -6,7 +6,6 @@ Authors: Oliver Nash
 import Mathlib.FieldTheory.Separable
 import Mathlib.FieldTheory.SplittingField.Construction
 import Mathlib.Algebra.CharP.Reduced
-import Mathlib.Algebra.Squarefree.UniqueFactorizationDomain
 
 /-!
 
@@ -232,21 +231,12 @@ instance toPerfectRing (p : ℕ) [ExpChar K p] : PerfectRing K p := by
   exact minpoly.degree_pos ha
 
 theorem separable_iff_squarefree {g : K[X]} : g.Separable ↔ Squarefree g := by
-  refine ⟨Separable.squarefree, ?_⟩
-  induction' g using UniqueFactorizationMonoid.induction_on_coprime with p hp p n hp p q _ ihp ihq
-  · simp
-  · obtain ⟨x, hx, rfl⟩ := isUnit_iff.mp hp
-    exact fun _ ↦ (separable_C x).mpr hx
-  · intro hpn
-    rcases hpn.eq_zero_or_one_of_pow_of_not_isUnit hp.not_unit with rfl | rfl; · simp
-    exact (pow_one p).symm ▸ PerfectField.separable_of_irreducible hp.irreducible
-  · intro hpq'
-    obtain ⟨h, hp, hq⟩ := squarefree_mul_iff.mp hpq'
-    apply (ihp hp).mul (ihq hq)
-    classical
-    apply EuclideanDomain.isCoprime_of_dvd
-    · rintro ⟨rfl, rfl⟩; simp at hp
-    · exact fun d hd _ hdp hdq ↦ mem_nonunits_iff.mpr hd <| h d hdp hdq
+  refine ⟨Separable.squarefree, fun sqf ↦ isCoprime_of_irreducible_dvd (sqf.ne_zero ·.1) ?_⟩
+  rintro p (h : Irreducible p) ⟨q, rfl⟩ (dvd : p ∣ derivative (p * q))
+  replace dvd : p ∣ q := by
+    rw [derivative_mul, dvd_add_left (dvd_mul_right p _)] at dvd
+    exact (separable_of_irreducible h).dvd_of_dvd_mul_left dvd
+  exact (h.1 : ¬ IsUnit p) (sqf _ <| mul_dvd_mul_left _ dvd)
 
 end PerfectField
 

Mathlib/RingTheory/PrincipalIdealDomain.lean

@@ -354,7 +354,10 @@ section
 
 open Ideal
 
-variable [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [GCDMonoid R]
+variable [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
+
+section GCD
+variable [GCDMonoid R]
 
 theorem span_gcd (x y : R) : span ({gcd x y} : Set R) = span ({x, y} : Set R) := by
   obtain ⟨d, hd⟩ := IsPrincipalIdealRing.principal (span ({x, y} : Set R))
@@ -391,9 +394,12 @@ theorem gcd_isUnit_iff (x y : R) : IsUnit (gcd x y) ↔ IsCoprime x y := by
   rw [IsCoprime, ← Ideal.mem_span_pair, ← span_gcd, ← span_singleton_eq_top, eq_top_iff_one]
 #align gcd_is_unit_iff gcd_isUnit_iff
 
+end GCD
+
 -- this should be proved for UFDs surely?
 theorem isCoprime_of_dvd (x y : R) (nonzero : ¬(x = 0 ∧ y = 0))
     (H : ∀ z ∈ nonunits R, z ≠ 0 → z ∣ x → ¬z ∣ y) : IsCoprime x y := by
+  letI := UniqueFactorizationMonoid.toGCDMonoid R
   rw [← gcd_isUnit_iff]
   by_contra h
   refine' H _ h _ (gcd_dvd_left _ _) (gcd_dvd_right _ _)
@@ -423,7 +429,8 @@ theorem isCoprime_of_irreducible_dvd {x y : R} (nonzero : ¬(x = 0 ∧ y = 0))
 
 theorem isCoprime_of_prime_dvd {x y : R} (nonzero : ¬(x = 0 ∧ y = 0))
     (H : ∀ z : R, Prime z → z ∣ x → ¬z ∣ y) : IsCoprime x y :=
-  isCoprime_of_irreducible_dvd nonzero fun z zi => H z <| GCDMonoid.prime_of_irreducible zi
+  isCoprime_of_irreducible_dvd nonzero fun z zi ↦
+    H z (PrincipalIdealRing.irreducible_iff_prime.1 zi)
 #align is_coprime_of_prime_dvd isCoprime_of_prime_dvd
 
 theorem Irreducible.coprime_iff_not_dvd {p n : R} (pp : Irreducible p) :
@@ -462,6 +469,7 @@ theorem Irreducible.coprime_or_dvd {p : R} (hp : Irreducible p) (i : R) : IsCopr
 
 theorem exists_associated_pow_of_mul_eq_pow' {a b c : R} (hab : IsCoprime a b) {k : ℕ}
     (h : a * b = c ^ k) : ∃ d : R, Associated (d ^ k) a :=
+  letI := UniqueFactorizationMonoid.toGCDMonoid R
   exists_associated_pow_of_mul_eq_pow ((gcd_isUnit_iff _ _).mpr hab) h
 #align exists_associated_pow_of_mul_eq_pow' exists_associated_pow_of_mul_eq_pow'