RFC/chore(Algebra/GCDMonoid): should we un-@[simp] normalize_apply? (#18006)

The lemma `normalize_apply` feels to me like it exposes the implementation detail that `normalize` is defined in terms of `normUnit`. I think the `normalize` function itself is much more familiar so it doesn't really seem like a simplification to insert `normUnit` instead. Indeed there are quite a few `simp [-normalize_apply]` in Mathlib.

Moreover, there were some `simp` lemmas about `normalize` that had to be given higher priority since e.g. `normalize (a * b) = normalize a * normalize b` but `normUnit (a * b)` does not necessarily equal `normUnit a * normUnit b`.

A few downstream fixes are needed where a `@[simp]` lemma is proved for `normUnit` and not for `normalize`, otherwise everything goes very smoothly.

Author: Vierkantor

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -116,21 +116,16 @@ theorem normalize_associated_iff {x y : α} : Associated (normalize x) y ↔ Ass
 theorem Associates.mk_normalize (x : α) : Associates.mk (normalize x) = Associates.mk x :=
   Associates.mk_eq_mk_iff_associated.2 (normalize_associated _)
 
-@[simp]
 theorem normalize_apply (x : α) : normalize x = x * normUnit x :=
   rfl
 
--- Porting note (#10618): `simp` can prove this
--- @[simp]
 theorem normalize_zero : normalize (0 : α) = 0 :=
   normalize.map_zero
 
--- Porting note (#10618): `simp` can prove this
--- @[simp]
 theorem normalize_one : normalize (1 : α) = 1 :=
   normalize.map_one
 
-theorem normalize_coe_units (u : αˣ) : normalize (u : α) = 1 := by simp
+theorem normalize_coe_units (u : αˣ) : normalize (u : α) = 1 := by simp [normalize_apply]
 
 theorem normalize_eq_zero {x : α} : normalize x = 0 ↔ x = 0 :=
   ⟨fun hx => (associated_zero_iff_eq_zero x).1 <| hx ▸ associated_normalize _, by
@@ -147,7 +142,8 @@ theorem normUnit_mul_normUnit (a : α) : normUnit (a * normUnit a) = 1 := by
   · rw [normUnit_zero, zero_mul, normUnit_zero]
   · rw [normUnit_mul h (Units.ne_zero _), normUnit_coe_units, mul_inv_eq_one]
 
-theorem normalize_idem (x : α) : normalize (normalize x) = normalize x := by simp
+@[simp]
+theorem normalize_idem (x : α) : normalize (normalize x) = normalize x := by simp [normalize_apply]
 
 theorem normalize_eq_normalize {a b : α} (hab : a ∣ b) (hba : b ∣ a) :
     normalize a = normalize b := by
@@ -173,11 +169,11 @@ theorem Associated.eq_of_normalized
     a = b :=
   dvd_antisymm_of_normalize_eq ha hb h.dvd h.dvd'
 
---can be proven by simp
+@[simp]
 theorem dvd_normalize_iff {a b : α} : a ∣ normalize b ↔ a ∣ b :=
   Units.dvd_mul_right
 
---can be proven by simp
+@[simp]
 theorem normalize_dvd_iff {a b : α} : normalize a ∣ b ↔ a ∣ b :=
   Units.mul_right_dvd
 
@@ -216,8 +212,7 @@ theorem out_dvd_iff (a : α) (b : Associates α) : b.out ∣ a ↔ b ≤ Associa
 theorem out_top : (⊤ : Associates α).out = 0 :=
   normalize_zero
 
--- Porting note: lower priority to avoid linter complaints about simp-normal form
-@[simp 1100]
+@[simp]
 theorem normalize_out (a : Associates α) : normalize a.out = a.out :=
   Quotient.inductionOn a normalize_idem
 
@@ -287,8 +282,7 @@ theorem gcd_isUnit_iff_isRelPrime [GCDMonoid α] {a b : α} :
     IsUnit (gcd a b) ↔ IsRelPrime a b :=
   ⟨fun h _ ha hb ↦ isUnit_of_dvd_unit (dvd_gcd ha hb) h, (· (gcd_dvd_left a b) (gcd_dvd_right a b))⟩
 
--- Porting note: lower priority to avoid linter complaints about simp-normal form
-@[simp 1100]
+@[simp]
 theorem normalize_gcd [NormalizedGCDMonoid α] : ∀ a b : α, normalize (gcd a b) = gcd a b :=
   NormalizedGCDMonoid.normalize_gcd
 
@@ -399,7 +393,7 @@ theorem gcd_mul_left [NormalizedGCDMonoid α] (a b c : α) :
     gcd (a * b) (a * c) = normalize a * gcd b c :=
   (by_cases (by rintro rfl; simp only [zero_mul, gcd_zero_left, normalize_zero]))
     fun ha : a ≠ 0 =>
-    suffices gcd (a * b) (a * c) = normalize (a * gcd b c) by simpa [- normalize_apply]
+    suffices gcd (a * b) (a * c) = normalize (a * gcd b c) by simpa
     let ⟨d, eq⟩ := dvd_gcd (dvd_mul_right a b) (dvd_mul_right a c)
     gcd_eq_normalize
       (eq.symm ▸ mul_dvd_mul_left a
@@ -689,8 +683,7 @@ theorem lcm_eq_zero_iff [GCDMonoid α] (a b : α) : lcm a b = 0 ↔ a = 0 ∨ b
       rwa [← mul_eq_zero, ← associated_zero_iff_eq_zero])
     (by rintro (rfl | rfl) <;> [apply lcm_zero_left; apply lcm_zero_right])
 
--- Porting note: lower priority to avoid linter complaints about simp-normal form
-@[simp 1100]
+@[simp]
 theorem normalize_lcm [NormalizedGCDMonoid α] (a b : α) : normalize (lcm a b) = lcm a b :=
   NormalizedGCDMonoid.normalize_lcm a b
 
@@ -766,7 +759,7 @@ theorem lcm_mul_left [NormalizedGCDMonoid α] (a b c : α) :
     lcm (a * b) (a * c) = normalize a * lcm b c :=
   (by_cases (by rintro rfl; simp only [zero_mul, lcm_zero_left, normalize_zero]))
     fun ha : a ≠ 0 =>
-    suffices lcm (a * b) (a * c) = normalize (a * lcm b c) by simpa [- normalize_apply]
+    suffices lcm (a * b) (a * c) = normalize (a * lcm b c) by simpa
     have : a ∣ lcm (a * b) (a * c) := (dvd_mul_right _ _).trans (dvd_lcm_left _ _)
     let ⟨_, eq⟩ := this
     lcm_eq_normalize
@@ -866,8 +859,7 @@ instance subsingleton_normalizedGCDMonoid_of_unique_units : Subsingleton (Normal
 theorem normUnit_eq_one (x : α) : normUnit x = 1 :=
   rfl
 
--- Porting note (#10618): `simp` can prove this
--- @[simp]
+@[simp]
 theorem normalize_eq (x : α) : normalize x = x :=
   mul_one x
 

Mathlib/Algebra/GCDMonoid/Nat.lean

@@ -79,7 +79,7 @@ theorem normalize_coe_nat (n : ℕ) : normalize (n : ℤ) = n :=
 
 theorem abs_eq_normalize (z : ℤ) : |z| = normalize z := by
   cases le_total 0 z <;>
-  simp [-normalize_apply, abs_of_nonneg, abs_of_nonpos, normalize_of_nonneg, normalize_of_nonpos, *]
+  simp [abs_of_nonneg, abs_of_nonpos, normalize_of_nonneg, normalize_of_nonpos, *]
 
 theorem nonneg_of_normalize_eq_self {z : ℤ} (hz : normalize z = z) : 0 ≤ z := by
   by_cases h : 0 ≤ z
@@ -147,7 +147,7 @@ def associatesIntEquivNat : Associates ℤ ≃ ℕ := by
   refine ⟨(·.out.natAbs), (Associates.mk ·), ?_, fun n ↦ ?_⟩
   · refine Associates.forall_associated.2 fun a ↦ ?_
     refine Associates.mk_eq_mk_iff_associated.2 <| Associated.symm <| ⟨normUnit a, ?_⟩
-    simp [Int.abs_eq_normalize]
+    simp [Int.abs_eq_normalize, normalize_apply]
   · dsimp only [Associates.out_mk]
     rw [← Int.abs_eq_normalize, Int.natAbs_abs, Int.natAbs_ofNat]
 

Mathlib/Algebra/Polynomial/FieldDivision.lean

@@ -195,8 +195,9 @@ instance instNormalizationMonoid : NormalizationMonoid R[X] where
 theorem coe_normUnit {p : R[X]} : (normUnit p : R[X]) = C ↑(normUnit p.leadingCoeff) := by
   simp [normUnit]
 
+@[simp]
 theorem leadingCoeff_normalize (p : R[X]) :
-    leadingCoeff (normalize p) = normalize (leadingCoeff p) := by simp
+    leadingCoeff (normalize p) = normalize (leadingCoeff p) := by simp [normalize_apply]
 
 theorem Monic.normalize_eq_self {p : R[X]} (hp : p.Monic) : normalize p = p := by
   simp only [Polynomial.coe_normUnit, normalize_apply, hp.leadingCoeff, normUnit_one,
@@ -536,7 +537,9 @@ theorem map_dvd_map' [Field k] (f : R →+* k) {x y : R[X]} : x.map f ∣ y.map
       leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
       map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
 
-theorem degree_normalize [DecidableEq R] : degree (normalize p) = degree p := by simp
+@[simp]
+theorem degree_normalize [DecidableEq R] : degree (normalize p) = degree p := by
+  simp [normalize_apply]
 
 theorem prime_of_degree_eq_one (hp1 : degree p = 1) : Prime p := by
   classical

Mathlib/RingTheory/DedekindDomain/Ideal.lean

@@ -1429,7 +1429,7 @@ theorem count_span_normalizedFactors_eq_of_normUnit {r X : R}
     (hr : r ≠ 0) (hX₁ : normUnit X = 1) (hX : Prime X) :
       Multiset.count (Ideal.span {X} : Ideal R) (normalizedFactors (Ideal.span {r})) =
         Multiset.count X (normalizedFactors r) := by
-  simpa [hX₁] using count_span_normalizedFactors_eq hr hX
+  simpa [hX₁, normalize_apply] using count_span_normalizedFactors_eq hr hX
 
 end NormalizationMonoid