chore: remove unnecessary private and backward.privateInPublic (#36430)

This PR removes `private` modifiers and corresponding `set_option backward.privateInPublic` from definitions in three files where they are not really sensible.

These private definitions were being exposed to public proofs via `backward.privateInPublic`, which means the private names (with `_private.` mangling) appear in downstream goal states. When the tactic analysis regression linter tries to re-run replacement tactics on those goals, it encounters "Unknown constant" errors because the private constants aren't accessible from other modules.

Files changed:
- `Mathlib.RingTheory.OreLocalization.Basic`: remove `private` from `add''`, `add''_char`, `add'`, `add`, `nsmul`
- `Mathlib.Analysis.Complex.Norm`: change `private` to `protected` for `norm_nonneg`, `norm_add_le'`, `norm_eq_zero_iff`, `norm_map_zero'`, `norm_neg'` (these names clash with global names from `NormedAddCommGroup`)
- `Mathlib.Analysis.Normed.Module.Multilinear.Basic`: remove `private` from `uniformity_eq_seminorm`

Verified locally: all three files and their downstream dependencies build successfully.

🤖 Prepared with Claude Code

Author: kim-em

Mathlib/Analysis/Complex/Norm.lean

@@ -30,49 +30,43 @@ theorem norm_def (z : ℂ) : ‖z‖ = √(normSq z) := rfl
 theorem norm_mul_self_eq_normSq (z : ℂ) : ‖z‖ * ‖z‖ = normSq z :=
   Real.mul_self_sqrt (normSq_nonneg _)
 
-private theorem norm_nonneg (z : ℂ) : 0 ≤ ‖z‖ :=
+protected theorem norm_nonneg (z : ℂ) : 0 ≤ ‖z‖ :=
   Real.sqrt_nonneg _
 
 @[bound]
 theorem abs_re_le_norm (z : ℂ) : |z.re| ≤ ‖z‖ := by
-  rw [mul_self_le_mul_self_iff (abs_nonneg z.re) (norm_nonneg _), abs_mul_abs_self,
+  rw [mul_self_le_mul_self_iff (abs_nonneg z.re) (Complex.norm_nonneg _), abs_mul_abs_self,
     norm_mul_self_eq_normSq]
   apply re_sq_le_normSq
 
 theorem re_le_norm (z : ℂ) : z.re ≤ ‖z‖ :=
   (abs_le.1 (abs_re_le_norm _)).2
 
-set_option backward.privateInPublic true in
-private theorem norm_add_le' (z w : ℂ) : ‖z + w‖ ≤ ‖z‖ + ‖w‖ :=
-  (mul_self_le_mul_self_iff (norm_nonneg (z + w)) (add_nonneg (norm_nonneg z)
-    (norm_nonneg w))).2 <| by
+protected theorem norm_add_le' (z w : ℂ) : ‖z + w‖ ≤ ‖z‖ + ‖w‖ :=
+  (mul_self_le_mul_self_iff (Complex.norm_nonneg (z + w)) (add_nonneg (Complex.norm_nonneg z)
+    (Complex.norm_nonneg w))).2 <| by
     rw [norm_mul_self_eq_normSq, add_mul_self_eq, norm_mul_self_eq_normSq, norm_mul_self_eq_normSq,
       add_right_comm, normSq_add, mul_assoc, norm_def, norm_def, ← Real.sqrt_mul <| normSq_nonneg z,
       ← normSq_conj w, ← map_mul]
     gcongr
     exact re_le_norm (z * conj w)
 
-set_option backward.privateInPublic true in
-private theorem norm_eq_zero_iff {z : ℂ} : ‖z‖ = 0 ↔ z = 0 :=
+protected theorem norm_eq_zero_iff {z : ℂ} : ‖z‖ = 0 ↔ z = 0 :=
   (Real.sqrt_eq_zero <| normSq_nonneg _).trans normSq_eq_zero
 
-set_option backward.privateInPublic true in
-private theorem norm_map_zero' : ‖(0 : ℂ)‖ = 0 :=
-  norm_eq_zero_iff.mpr rfl
+protected theorem norm_map_zero' : ‖(0 : ℂ)‖ = 0 :=
+  Complex.norm_eq_zero_iff.mpr rfl
 
-set_option backward.privateInPublic true in
-private theorem norm_neg' (z : ℂ) : ‖-z‖ = ‖z‖ := by
+protected theorem norm_neg' (z : ℂ) : ‖-z‖ = ‖z‖ := by
   rw [Complex.norm_def, norm_def, normSq_neg]
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance instNormedAddCommGroup : NormedAddCommGroup ℂ :=
   AddGroupNorm.toNormedAddCommGroup
   { toFun := norm
-    map_zero' := norm_map_zero'
-    add_le' := norm_add_le'
-    neg' := norm_neg'
-    eq_zero_of_map_eq_zero' := fun _ ↦ norm_eq_zero_iff.mp }
+    map_zero' := Complex.norm_map_zero'
+    add_le' := Complex.norm_add_le'
+    neg' := Complex.norm_neg'
+    eq_zero_of_map_eq_zero' := fun _ ↦ Complex.norm_eq_zero_iff.mp }
 
 @[simp 1100]
 protected theorem norm_mul (z w : ℂ) : ‖z * w‖ = ‖z‖ * ‖w‖ := by
@@ -84,7 +78,7 @@ protected theorem norm_div (z w : ℂ) : ‖z / w‖ = ‖z‖ / ‖w‖ := by
 
 instance isAbsoluteValueNorm : IsAbsoluteValue (‖·‖ : ℂ → ℝ) where
   abv_nonneg' := norm_nonneg
-  abv_eq_zero' := norm_eq_zero_iff
+  abv_eq_zero' := Complex.norm_eq_zero_iff
   abv_add' := norm_add_le
   abv_mul' := Complex.norm_mul
 

Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean

@@ -450,8 +450,7 @@ so that it is definitionally equal to the one coming from the topologies on `E`
 protected def seminorm : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G) :=
   .ofSMulLE norm opNorm_zero opNorm_add_le fun c f ↦ f.opNorm_smul_le c
 
-set_option backward.privateInPublic true in
-private lemma uniformity_eq_seminorm :
+lemma uniformity_eq_seminorm :
     𝓤 (ContinuousMultilinearMap 𝕜 E G) = ⨅ r > 0, 𝓟 {f | ‖-f.1 + f.2‖ < r} := by
   have A (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G) :
       ‖-f.1 + f.2‖ = ‖f.1 - f.2‖ := by rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
@@ -484,8 +483,6 @@ private lemma uniformity_eq_seminorm :
       _ ≤ δ * ε ^ Fintype.card ι := by have := (norm_nonneg x).trans hx; gcongr
       _ ≤ r := (mul_comm _ _).trans_le hδ.le
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance instPseudoMetricSpace : PseudoMetricSpace (ContinuousMultilinearMap 𝕜 E G) :=
   .replaceUniformity
     (ContinuousMultilinearMap.seminorm 𝕜 E G).toSeminormedAddCommGroup.toPseudoMetricSpace

Mathlib/RingTheory/OreLocalization/Basic.lean

@@ -78,11 +78,11 @@ section DistribMulAction
 variable {R : Type*} [Monoid R] {S : Submonoid R} [OreSet S] {X : Type*} [AddMonoid X]
 variable [DistribMulAction R X]
 
-set_option backward.privateInPublic true in
-private def add'' (r₁ : X) (s₁ : S) (r₂ : X) (s₂ : S) : X[S⁻¹] :=
+/-- Auxiliary definition for addition on the Ore localization. -/
+def add'' (r₁ : X) (s₁ : S) (r₂ : X) (s₂ : S) : X[S⁻¹] :=
   (oreDenom (s₁ : R) s₂ • r₁ + oreNum (s₁ : R) s₂ • r₂) /ₒ (oreDenom (s₁ : R) s₂ * s₁)
 
-private theorem add''_char (r₁ : X) (s₁ : S) (r₂ : X) (s₂ : S) (rb : R) (sb : R)
+theorem add''_char (r₁ : X) (s₁ : S) (r₂ : X) (s₂ : S) (rb : R) (sb : R)
     (hb : sb * s₁ = rb * s₂) (h : sb * s₁ ∈ S) :
     add'' r₁ s₁ r₂ s₂ = (sb • r₁ + rb • r₂) /ₒ ⟨sb * s₁, h⟩ := by
   simp only [add'']
@@ -103,8 +103,8 @@ private theorem add''_char (r₁ : X) (s₁ : S) (r₂ : X) (s₂ : S) (rb : R)
 
 attribute [local instance] OreLocalization.oreEqv
 
-set_option backward.privateInPublic true in
-private def add' (r₂ : X) (s₂ : S) : X[S⁻¹] → X[S⁻¹] :=
+/-- Auxiliary definition for addition on the Ore localization, with one argument fixed. -/
+def add' (r₂ : X) (s₂ : S) : X[S⁻¹] → X[S⁻¹] :=
   (--plus tilde
       Quotient.lift
       fun r₁s₁ : X × S => add'' r₁s₁.1 r₁s₁.2 r₂ s₂) <| by
@@ -126,10 +126,9 @@ private def add' (r₂ : X) (s₂ : S) : X[S⁻¹] → X[S⁻¹] :=
     simp only [mul_smul, smul_add, one_smul, OneMemClass.coe_one, one_mul, true_and]
     rw [this, hc, mul_assoc]
 
-set_option backward.privateInPublic true in
 /-- The addition on the Ore localization. -/
 @[irreducible]
-private def add : X[S⁻¹] → X[S⁻¹] → X[S⁻¹] := fun x =>
+def add : X[S⁻¹] → X[S⁻¹] → X[S⁻¹] := fun x =>
   Quotient.lift (fun rs : X × S => add' rs.1 rs.2 x)
     (by
       rintro ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨sb, rb, hb, hb'⟩
@@ -148,8 +147,6 @@ private def add : X[S⁻¹] → X[S⁻¹] → X[S⁻¹] := fun x =>
       simp only [one_smul, one_mul, mul_smul, ← hb, Submonoid.smul_def, ← mul_assoc, and_true]
       simp only [smul_smul, hd])
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance : Add X[S⁻¹] :=
   ⟨add⟩
 
@@ -205,12 +202,10 @@ protected theorem add_zero (x : X[S⁻¹]) : x + 0 = x := by
   induction x
   rw [← zero_oreDiv, add_oreDiv]; simp
 
-set_option backward.privateInPublic true in
+/-- Scalar multiplication by natural numbers on the Ore localization. -/
 @[irreducible]
-private def nsmul : ℕ → X[S⁻¹] → X[S⁻¹] := nsmulRec
+def nsmul : ℕ → X[S⁻¹] → X[S⁻¹] := nsmulRec
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance : AddMonoid X[S⁻¹] where
     add_assoc := OreLocalization.add_assoc
     zero_add := OreLocalization.zero_add