chore: deal with porting notes about 'protected' (#18368)

Co-authored-by: Johan Commelin <[email protected]>

Mathlib/Algebra/Algebra/Equiv.lean

@@ -130,7 +130,6 @@ theorem mk_coe (e : A₁ ≃ₐ[R] A₂) (e' h₁ h₂ h₃ h₄ h₅) :
 theorem toEquiv_eq_coe : e.toEquiv = e :=
   rfl
 
--- Porting note: `protected` used to be an attribute below
 @[simp]
 protected theorem coe_coe {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) :
     ⇑(f : A₁ ≃ₐ[R] A₂) = f :=

Mathlib/Algebra/GroupWithZero/Divisibility.lean

@@ -139,9 +139,6 @@ theorem dvd_antisymm : a ∣ b → b ∣ a → a = b := by
   rw [mul_assoc, eq_comm, mul_right_eq_self₀, mul_eq_one] at hcd
   obtain ⟨rfl, -⟩ | rfl := hcd <;> simp
 
--- Porting note: `attribute [protected]` is currently unsupported
--- attribute [protected] Nat.dvd_antisymm --This lemma is in core, so we protect it here
-
 theorem dvd_antisymm' : a ∣ b → b ∣ a → b = a :=
   flip dvd_antisymm
 

Mathlib/Algebra/ModEq.lean

@@ -174,16 +174,13 @@ protected theorem sub_iff_right :
     a₂ ≡ b₂ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p]) := fun ⟨m, hm⟩ =>
   (Equiv.subRight m).symm.exists_congr_left.trans <| by simp [sub_sub_sub_comm, hm, sub_smul, ModEq]
 
-alias ⟨add_left_cancel, add⟩ := ModEq.add_iff_left
+protected alias ⟨add_left_cancel, add⟩ := ModEq.add_iff_left
 
-alias ⟨add_right_cancel, _⟩ := ModEq.add_iff_right
+protected alias ⟨add_right_cancel, _⟩ := ModEq.add_iff_right
 
-alias ⟨sub_left_cancel, sub⟩ := ModEq.sub_iff_left
+protected alias ⟨sub_left_cancel, sub⟩ := ModEq.sub_iff_left
 
-alias ⟨sub_right_cancel, _⟩ := ModEq.sub_iff_right
-
--- Porting note: doesn't work
--- attribute [protected] add_left_cancel add_right_cancel add sub_left_cancel sub_right_cancel sub
+protected alias ⟨sub_right_cancel, _⟩ := ModEq.sub_iff_right
 
 protected theorem add_left (c : α) (h : a ≡ b [PMOD p]) : c + a ≡ c + b [PMOD p] :=
   modEq_rfl.add h

Mathlib/Algebra/Ring/Int.lean

@@ -176,13 +176,8 @@ lemma even_mul_pred_self (n : ℤ) : Even (n * (n - 1)) := by
 lemma natAbs_odd : Odd n.natAbs ↔ Odd n := by
   rw [← not_even_iff_odd, ← Nat.not_even_iff_odd, natAbs_even]
 
-alias ⟨_, _root_.Even.natAbs⟩ := natAbs_even
-
-alias ⟨_, _root_.Odd.natAbs⟩ := natAbs_odd
-
--- Porting note: "protected"-attribute not implemented yet.
--- mathlib3 had:
--- `attribute [protected] Even.natAbs Odd.natAbs`
+protected alias ⟨_, _root_.Even.natAbs⟩ := natAbs_even
+protected alias ⟨_, _root_.Odd.natAbs⟩ := natAbs_odd
 
 lemma four_dvd_add_or_sub_of_odd {a b : ℤ} (ha : Odd a) (hb : Odd b) :
     4 ∣ a + b ∨ 4 ∣ a - b := by

Mathlib/Analysis/Normed/Field/Lemmas.lean

@@ -157,8 +157,7 @@ instance (priority := 100) NonUnitalSeminormedRing.toContinuousMul [NonUnitalSem
           intro e
           calc
             ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
-              rw [_root_.mul_sub, _root_.sub_mul, sub_add_sub_cancel]
-            -- Porting note: `ENNReal.{mul_sub, sub_mul}` should be protected
+              rw [mul_sub, sub_mul, sub_add_sub_cancel]
             _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
               norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
         refine squeeze_zero (fun e => norm_nonneg _) this ?_
@@ -297,9 +296,8 @@ instance (priority := 100) NormedDivisionRing.to_hasContinuousInv₀ : HasContin
     have e0 : e ≠ 0 := norm_pos_iff.1 (ε0.trans he)
     calc
       ‖e⁻¹ - r⁻¹‖ = ‖r‖⁻¹ * ‖r - e‖ * ‖e‖⁻¹ := by
-        rw [← norm_inv, ← norm_inv, ← norm_mul, ← norm_mul, _root_.mul_sub, _root_.sub_mul,
+        rw [← norm_inv, ← norm_inv, ← norm_mul, ← norm_mul, mul_sub, sub_mul,
           mul_assoc _ e, inv_mul_cancel₀ r0, mul_inv_cancel₀ e0, one_mul, mul_one]
-      -- Porting note: `ENNReal.{mul_sub, sub_mul}` should be `protected`
       _ = ‖r - e‖ / ‖r‖ / ‖e‖ := by field_simp [mul_comm]
       _ ≤ ‖r - e‖ / ‖r‖ / ε := by gcongr
   refine squeeze_zero' (Eventually.of_forall fun _ => norm_nonneg _) this ?_

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -1084,9 +1084,8 @@ theorem mul_mem_ball_mul_iff {c : E} : a * c ∈ ball (b * c) r ↔ a ∈ ball b
 @[to_additive]
 theorem smul_closedBall'' : a • closedBall b r = closedBall (a • b) r := by
   ext
-  simp [mem_closedBall, Set.mem_smul_set, dist_eq_norm_div, _root_.div_eq_inv_mul, ←
+  simp [mem_closedBall, Set.mem_smul_set, dist_eq_norm_div, div_eq_inv_mul, ←
     eq_inv_mul_iff_mul_eq, mul_assoc]
-  -- Porting note: `ENNReal.div_eq_inv_mul` should be `protected`?
 
 @[to_additive]
 theorem smul_ball'' : a • ball b r = ball (a • b) r := by

Mathlib/Analysis/Normed/Group/Bounded.lean

@@ -161,8 +161,6 @@ lemma HasCompactMulSupport.exists_pos_le_norm [One E] (hf : HasCompactMulSupport
   obtain ⟨K, ⟨hK1, hK2⟩⟩ := exists_compact_iff_hasCompactMulSupport.mpr hf
   obtain ⟨S, hS, hS'⟩ := hK1.isBounded.exists_pos_norm_le
   refine ⟨S + 1, by positivity, fun x hx => hK2 x ((mt <| hS' x) ?_)⟩
-  -- Porting note: `ENNReal.add_lt_add` should be `protected`?
-  -- [context: we used `_root_.add_lt_add` in a previous version of this proof]
   contrapose! hx
   exact lt_add_of_le_of_pos hx zero_lt_one
 

Mathlib/Analysis/Normed/Group/Uniform.lean

@@ -325,8 +325,7 @@ theorem mul_lipschitzWith (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g
   refine AntilipschitzWith.of_le_mul_dist fun x y => ?_
   rw [NNReal.coe_inv, ← _root_.div_eq_inv_mul]
   rw [le_div_iff₀ (NNReal.coe_pos.2 <| tsub_pos_iff_lt.2 hK)]
-  rw [mul_comm, NNReal.coe_sub hK.le, _root_.sub_mul]
-  -- Porting note: `ENNReal.sub_mul` should be `protected`?
+  rw [mul_comm, NNReal.coe_sub hK.le, sub_mul]
   calc
     ↑Kf⁻¹ * dist x y - Kg * dist x y ≤ dist (f x) (f y) - dist (g x) (g y) :=
       sub_le_sub (hf.mul_le_dist x y) (hg.dist_le_mul x y)

Mathlib/Analysis/Oscillation.lean

@@ -107,7 +107,7 @@ theorem uniform_oscillationWithin (comp : IsCompact K) (hK : ∀ x ∈ K, oscill
       ⟨ENNReal.ofReal ((a - r) / 2), by simp [ar], ?_⟩
     refine fun y hy ↦ ⟨a - (a - r) / 2, by linarith,
       le_trans (diam_mono (image_mono fun z hz ↦ ?_)) ha⟩
-    refine ⟨lt_of_le_of_lt (edist_triangle z y x) (lt_of_lt_of_eq (add_lt_add hz.1 hy) ?_),
+    refine ⟨lt_of_le_of_lt (edist_triangle z y x) (lt_of_lt_of_eq (ENNReal.add_lt_add hz.1 hy) ?_),
       hz.2⟩
     rw [← ofReal_add (by linarith) (by linarith), sub_add_cancel]
   have S_cover : K ⊆ ⋃ r > 0, S r := by

Mathlib/CategoryTheory/Category/Pointed.lean

@@ -25,17 +25,14 @@ universe u
 /-- The category of pointed types. -/
 structure Pointed : Type (u + 1) where
   /-- the underlying type -/
-  X : Type u
+  protected X : Type u
   /-- the distinguished element -/
   point : X
 
 namespace Pointed
 
 instance : CoeSort Pointed Type* :=
-  ⟨X⟩
-
--- Porting note: protected attribute does not work
---attribute [protected] Pointed.X
+  ⟨Pointed.X⟩
 
 /-- Turns a point into a pointed type. -/
 def of {X : Type*} (point : X) : Pointed :=

Mathlib/Data/ENNReal/Operations.lean

@@ -250,7 +250,7 @@ theorem coe_finset_prod {s : Finset α} {f : α → ℝ≥0} : ↑(∏ a ∈ s,
 end OperationsAndInfty
 
 -- Porting note (#11215): TODO: generalize to `WithTop`
-@[gcongr] theorem add_lt_add (ac : a < c) (bd : b < d) : a + b < c + d := by
+@[gcongr] protected theorem add_lt_add (ac : a < c) (bd : b < d) : a + b < c + d := by
   lift a to ℝ≥0 using ac.ne_top
   lift b to ℝ≥0 using bd.ne_top
   cases c; · simp
@@ -414,14 +414,14 @@ theorem sub_right_inj {a b c : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≤ a) (hc :
   (cancel_of_ne ha).tsub_right_inj (cancel_of_ne <| ne_top_of_le_ne_top ha hb)
     (cancel_of_ne <| ne_top_of_le_ne_top ha hc) hb hc
 
-theorem sub_mul (h : 0 < b → b < a → c ≠ ∞) : (a - b) * c = a * c - b * c := by
+protected theorem sub_mul (h : 0 < b → b < a → c ≠ ∞) : (a - b) * c = a * c - b * c := by
   rcases le_or_lt a b with hab | hab; · simp [hab, mul_right_mono hab, tsub_eq_zero_of_le]
   rcases eq_or_lt_of_le (zero_le b) with (rfl | hb); · simp
   exact (cancel_of_ne <| mul_ne_top hab.ne_top (h hb hab)).tsub_mul
 
-theorem mul_sub (h : 0 < c → c < b → a ≠ ∞) : a * (b - c) = a * b - a * c := by
+protected theorem mul_sub (h : 0 < c → c < b → a ≠ ∞) : a * (b - c) = a * b - a * c := by
   simp only [mul_comm a]
-  exact sub_mul h
+  exact ENNReal.sub_mul h
 
 theorem sub_le_sub_iff_left (h : c ≤ a) (h' : a ≠ ∞) :
     (a - b ≤ a - c) ↔ c ≤ b :=

Mathlib/Data/List/Nodup.lean

@@ -213,10 +213,7 @@ theorem nodup_attach {l : List α} : Nodup (attach l) ↔ Nodup l :=
   ⟨fun h => attach_map_subtype_val l ▸ h.map fun _ _ => Subtype.eq, fun h =>
     Nodup.of_map Subtype.val ((attach_map_subtype_val l).symm ▸ h)⟩
 
-alias ⟨Nodup.of_attach, Nodup.attach⟩ := nodup_attach
-
--- Porting note: commented out
---attribute [protected] nodup.attach
+protected alias ⟨Nodup.of_attach, Nodup.attach⟩ := nodup_attach
 
 theorem Nodup.pmap {p : α → Prop} {f : ∀ a, p a → β} {l : List α} {H}
     (hf : ∀ a ha b hb, f a ha = f b hb → a = b) (h : Nodup l) : Nodup (pmap f l H) := by

Mathlib/Data/List/Pairwise.lean

@@ -69,9 +69,6 @@ theorem pairwise_of_reflexive_of_forall_ne {l : List α} {r : α → α → Prop
 
 /-! ### Pairwise filtering -/
 
-alias ⟨_, Pairwise.pwFilter⟩ := pwFilter_eq_self
-
--- Porting note: commented out
--- attribute [protected] List.Pairwise.pwFilter
+protected alias ⟨_, Pairwise.pwFilter⟩ := pwFilter_eq_self
 
 end List

Mathlib/Data/List/Perm/Subperm.lean

@@ -46,10 +46,7 @@ lemma subperm_iff : l₁ <+~ l₂ ↔ ∃ l, l ~ l₂ ∧ l₁ <+ l := by
 
 lemma subperm_cons_self : l <+~ a :: l := ⟨l, Perm.refl _, sublist_cons_self _ _⟩
 
-alias ⟨subperm.of_cons, subperm.cons⟩ := subperm_cons
-
--- Porting note: commented out
---attribute [protected] subperm.cons
+protected alias ⟨subperm.of_cons, subperm.cons⟩ := subperm_cons
 
 theorem cons_subperm_of_mem {a : α} {l₁ l₂ : List α} (d₁ : Nodup l₁) (h₁ : a ∉ l₁) (h₂ : a ∈ l₂)
     (s : l₁ <+~ l₂) : a :: l₁ <+~ l₂ := by

Mathlib/Data/List/Sublists.lean

@@ -327,12 +327,9 @@ theorem nodup_sublists {l : List α} : Nodup (sublists l) ↔ Nodup l :=
 theorem nodup_sublists' {l : List α} : Nodup (sublists' l) ↔ Nodup l := by
   rw [sublists'_eq_sublists, nodup_map_iff reverse_injective, nodup_sublists, nodup_reverse]
 
-alias ⟨nodup.of_sublists, nodup.sublists⟩ := nodup_sublists
+protected alias ⟨Nodup.of_sublists, Nodup.sublists⟩ := nodup_sublists
 
-alias ⟨nodup.of_sublists', nodup.sublists'⟩ := nodup_sublists'
-
--- Porting note: commented out
---attribute [protected] nodup.sublists nodup.sublists'
+protected alias ⟨Nodup.of_sublists', _⟩ := nodup_sublists'
 
 theorem nodup_sublistsLen (n : ℕ) {l : List α} (h : Nodup l) : (sublistsLen n l).Nodup := by
   have : Pairwise (· ≠ ·) l.sublists' := Pairwise.imp

Mathlib/Data/Nat/Prime/Basic.lean

@@ -135,10 +135,8 @@ theorem Prime.not_dvd_mul {p m n : ℕ} (pp : Prime p) (Hm : ¬p ∣ m) (Hn : ¬
 
 @[simp] lemma coprime_two_right : n.Coprime 2 ↔ Odd n := coprime_comm.trans coprime_two_left
 
-alias ⟨Coprime.odd_of_left, _root_.Odd.coprime_two_left⟩ := coprime_two_left
-alias ⟨Coprime.odd_of_right, _root_.Odd.coprime_two_right⟩ := coprime_two_right
-
--- Porting note: attributes `protected`, `nolint dup_namespace` removed
+protected alias ⟨Coprime.odd_of_left, _root_.Odd.coprime_two_left⟩ := coprime_two_left
+protected alias ⟨Coprime.odd_of_right, _root_.Odd.coprime_two_right⟩ := coprime_two_right
 
 theorem Prime.dvd_of_dvd_pow {p m n : ℕ} (pp : Prime p) (h : p ∣ m ^ n) : p ∣ m :=
   pp.prime.dvd_of_dvd_pow h

Mathlib/Data/Real/EReal.lean

@@ -1493,7 +1493,7 @@ lemma inv_neg_of_neg_ne_bot {a : EReal} (h : a < 0) (h' : a ≠ ⊥) : a⁻¹ <
 
 /-! ### Division -/
 
-lemma div_eq_inv_mul (a b : EReal) : a / b = b⁻¹ * a := EReal.mul_comm a b⁻¹
+protected lemma div_eq_inv_mul (a b : EReal) : a / b = b⁻¹ * a := EReal.mul_comm a b⁻¹
 
 lemma coe_div (a b : ℝ) : (a / b : ℝ) = (a : EReal) / (b : EReal) := rfl
 

Mathlib/Data/Set/Finite.lean

@@ -197,12 +197,9 @@ protected theorem toFinset_subset_toFinset : hs.toFinset ⊆ ht.toFinset ↔ s 
 protected theorem toFinset_ssubset_toFinset : hs.toFinset ⊂ ht.toFinset ↔ s ⊂ t := by
   simp only [← Finset.coe_ssubset, Finite.coe_toFinset]
 
-alias ⟨_, toFinset_mono⟩ := Finite.toFinset_subset_toFinset
+protected alias ⟨_, toFinset_mono⟩ := Finite.toFinset_subset_toFinset
 
-alias ⟨_, toFinset_strictMono⟩ := Finite.toFinset_ssubset_toFinset
-
--- Porting note: attribute [protected] doesn't work
--- attribute [protected] toFinset_mono toFinset_strictMono
+protected alias ⟨_, toFinset_strictMono⟩ := Finite.toFinset_ssubset_toFinset
 
 -- Porting note: `simp` can simplify LHS but then it simplifies something
 -- in the generated `Fintype {x | p x}` instance and fails to apply `Set.toFinset_setOf`
@@ -1213,10 +1210,7 @@ theorem infinite_range_iff {f : α → β} (hi : Injective f) :
     (range f).Infinite ↔ Infinite α := by
   rw [← image_univ, infinite_image_iff hi.injOn, infinite_univ_iff]
 
-alias ⟨_, Infinite.image⟩ := infinite_image_iff
-
--- Porting note: attribute [protected] doesn't work
--- attribute [protected] infinite.image
+protected alias ⟨_, Infinite.image⟩ := infinite_image_iff
 
 section Image2
 

Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean

@@ -63,7 +63,6 @@ instance evenOdd.gradedMonoid : SetLike.GradedMonoid (evenOdd Q) where
 
 /-- A version of `CliffordAlgebra.ι` that maps directly into the graded structure. This is
 primarily an auxiliary construction used to provide `CliffordAlgebra.gradedAlgebra`. -/
--- Porting note: added `protected`
 protected def GradedAlgebra.ι : M →ₗ[R] ⨁ i : ZMod 2, evenOdd Q i :=
   DirectSum.lof R (ZMod 2) (fun i => ↥(evenOdd Q i)) 1 ∘ₗ (ι Q).codRestrict _ (ι_mem_evenOdd_one Q)
 

Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean

@@ -24,7 +24,6 @@ open scoped DirectSum
 
 /-- A version of `ExteriorAlgebra.ι` that maps directly into the graded structure. This is
 primarily an auxiliary construction used to provide `ExteriorAlgebra.gradedAlgebra`. -/
--- Porting note: protected
 protected def GradedAlgebra.ι :
     M →ₗ[R] ⨁ i : ℕ, ⋀[R]^i M :=
   DirectSum.lof R ℕ (fun i => ⋀[R]^i M) 1 ∘ₗ

Mathlib/LinearAlgebra/Ray.lean

@@ -217,7 +217,6 @@ theorem equiv_iff_sameRay {v₁ v₂ : RayVector R M} : v₁ ≈ v₂ ↔ SameRa
 
 variable (R)
 
--- Porting note: Removed `protected` here, not in namespace
 /-- The ray given by a nonzero vector. -/
 def rayOfNeZero (v : M) (h : v ≠ 0) : Module.Ray R M :=
   ⟦⟨v, h⟩⟧

Mathlib/ModelTheory/Semantics.lean

@@ -466,10 +466,8 @@ theorem realize_all_liftAt_one_self {n : ℕ} {φ : L.BoundedFormula α n} {v :
 
 end BoundedFormula
 
-
--- Porting note: no `protected` attribute in Lean4
+-- Porting note: in Lean 3 we used these unprotected above, and then protected them here.
 -- attribute [protected] bounded_formula.falsum bounded_formula.equal bounded_formula.rel
-
 -- attribute [protected] bounded_formula.imp bounded_formula.all
 
 namespace LHom
@@ -492,11 +490,6 @@ theorem realize_onBoundedFormula [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpan
 
 end LHom
 
--- Porting note: no `protected` attribute in Lean4
--- attribute [protected] bounded_formula.falsum bounded_formula.equal bounded_formula.rel
-
--- attribute [protected] bounded_formula.imp bounded_formula.all
-
 namespace Formula
 
 /-- A formula can be evaluated as true or false by giving values to each free variable. -/

Mathlib/NumberTheory/FunctionField.lean

@@ -54,7 +54,6 @@ Note that `F` can be a function field over multiple, non-isomorphic, `Fq`.
 abbrev FunctionField [Algebra (RatFunc Fq) F] : Prop :=
   FiniteDimensional (RatFunc Fq) F
 
--- Porting note: Removed `protected`
 /-- `F` is a function field over `Fq` iff it is a finite extension of `Fq(t)`. -/
 theorem functionField_iff (Fqt : Type*) [Field Fqt] [Algebra Fq[X] Fqt]
     [IsFractionRing Fq[X] Fqt] [Algebra (RatFunc Fq) F] [Algebra Fqt F] [Algebra Fq[X] F]

Mathlib/Order/Directed.lean

@@ -58,11 +58,7 @@ alias ⟨DirectedOn.directed_val, _⟩ := directedOn_iff_directed
 theorem directedOn_range {f : ι → α} : Directed r f ↔ DirectedOn r (Set.range f) := by
   simp_rw [Directed, DirectedOn, Set.forall_mem_range, Set.exists_range_iff]
 
--- Porting note: This alias was misplaced in `order/compactly_generated.lean` in mathlib3
-alias ⟨Directed.directedOn_range, _⟩ := directedOn_range
-
--- Porting note: `attribute [protected]` doesn't work
--- attribute [protected] Directed.directedOn_range
+protected alias ⟨Directed.directedOn_range, _⟩ := directedOn_range
 
 theorem directedOn_image {s : Set β} {f : β → α} :
     DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s := by

Mathlib/Order/Filter/Germ/Basic.lean

@@ -79,7 +79,6 @@ def productSetoid (l : Filter α) (ε : α → Type*) : Setoid ((a : _) → ε a
 
 /-- The filter product `(a : α) → ε a` at a filter `l`. This is a dependent version of
   `Filter.Germ`. -/
--- Porting note: removed @[protected]
 def Product (l : Filter α) (ε : α → Type*) : Type _ :=
   Quotient (productSetoid l ε)
 

Mathlib/Order/Irreducible.lean

@@ -261,11 +261,8 @@ theorem infPrime_iff_infIrred : InfPrime a ↔ InfIrred a :=
   ⟨InfPrime.infIrred,
     And.imp_right fun h b c => by simp_rw [← sup_eq_left, sup_inf_left]; exact @h _ _⟩
 
-alias ⟨_, SupIrred.supPrime⟩ := supPrime_iff_supIrred
-
-alias ⟨_, InfIrred.infPrime⟩ := infPrime_iff_infIrred
-
--- Porting note: was attribute [protected] SupIrred.supPrime InfIrred.infPrime
+protected alias ⟨_, SupIrred.supPrime⟩ := supPrime_iff_supIrred
+protected alias ⟨_, InfIrred.infPrime⟩ := infPrime_iff_infIrred
 
 end DistribLattice
 

Mathlib/Order/Partition/Finpartition.lean

@@ -64,16 +64,13 @@ structure Finpartition [Lattice α] [OrderBot α] (a : α) where
   /-- The elements of the finite partition of `a` -/
   parts : Finset α
   /-- The partition is supremum-independent -/
-  supIndep : parts.SupIndep id
+  protected supIndep : parts.SupIndep id
   /-- The supremum of the partition is `a` -/
   sup_parts : parts.sup id = a
   /-- No element of the partition is bottom -/
   not_bot_mem : ⊥ ∉ parts
   deriving DecidableEq
 
--- Porting note: attribute [protected] doesn't work
--- attribute [protected] Finpartition.supIndep
-
 namespace Finpartition
 
 section Lattice

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -593,7 +593,6 @@ protected theorem IsInducing.topologicalGroup {F : Type*} [Group H] [Topological
 @[deprecated (since := "2024-10-28")] alias Inducing.topologicalGroup := IsInducing.topologicalGroup
 
 @[to_additive]
--- Porting note: removed `protected` (needs to be in namespace)
 theorem topologicalGroup_induced {F : Type*} [Group H] [FunLike F H G] [MonoidHomClass F H G]
     (f : F) :
     @TopologicalGroup H (induced f ‹_›) _ :=

Mathlib/Topology/Instances/ENNReal.lean

@@ -1096,7 +1096,7 @@ theorem edist_ne_top_of_mem_ball {a : β} {r : ℝ≥0∞} (x y : ball a r) : ed
   ne_of_lt <|
     calc
       edist x y ≤ edist a x + edist a y := edist_triangle_left x.1 y.1 a
-      _ < r + r := by rw [edist_comm a x, edist_comm a y]; exact add_lt_add x.2 y.2
+      _ < r + r := by rw [edist_comm a x, edist_comm a y]; exact ENNReal.add_lt_add x.2 y.2
       _ ≤ ∞ := le_top
 
 /-- Each ball in an extended metric space gives us a metric space, as the edist

Mathlib/Topology/MetricSpace/Dilation.lean

@@ -267,8 +267,8 @@ protected def id (α) [PseudoEMetricSpace α] : α →ᵈ α where
 instance : Inhabited (α →ᵈ α) :=
   ⟨Dilation.id α⟩
 
-@[simp] -- Porting note: Removed `@[protected]`
-theorem coe_id : ⇑(Dilation.id α) = id :=
+@[simp]
+protected theorem coe_id : ⇑(Dilation.id α) = id :=
   rfl
 
 theorem ratio_id : ratio (Dilation.id α) = 1 := by