[Merged by Bors] - chore: classify slow / slower porting notes

Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

@@ -104,7 +104,7 @@ private theorem colimitModule.one_smul (x : (M F)) : (1 : R) • x = x := by
   simp
   rfl
 
--- Porting note: writing directly the `Module` instance makes things very slow.
+-- Porting note (#11083): writing directly the `Module` instance makes things very slow.
 instance colimitMulAction : MulAction R (M F) where
   one_smul x := by
     refine' Quot.inductionOn x _; clear x; intro x; cases' x with j x

Mathlib/Algebra/DirectSum/Ring.lean

@@ -234,7 +234,7 @@ private nonrec theorem one_mul (x : ⨁ i, A i) : 1 * x = x := by
   exact of_eq_of_gradedMonoid_eq (one_mul <| GradedMonoid.mk i xi)
 #noalign direct_sum.one_mul
 
--- Porting note: `suffices` is very slow here.
+-- Porting note (#11083): `suffices` is very slow here.
 private nonrec theorem mul_one (x : ⨁ i, A i) : x * 1 = x := by
   suffices (mulHom A).flip One.one = AddMonoidHom.id (⨁ i, A i) from DFunLike.congr_fun this x
   apply addHom_ext; intro i xi

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -94,7 +94,7 @@ theorem normUnit_one : normUnit (1 : α) = 1 :=
   normUnit_coe_units 1
 #align norm_unit_one normUnit_one
 
--- Porting note: quite slow. Improve performance?
+-- Porting note (#11083): quite slow. Improve performance?
 /-- Chooses an element of each associate class, by multiplying by `normUnit` -/
 def normalize : α →*₀ α where
   toFun x := x * normUnit x
@@ -157,7 +157,7 @@ theorem normalize_eq_one {x : α} : normalize x = 1 ↔ IsUnit x :=
   ⟨fun hx => isUnit_iff_exists_inv.2 ⟨_, hx⟩, fun ⟨u, hu⟩ => hu ▸ normalize_coe_units u⟩
 #align normalize_eq_one normalize_eq_one
 
--- Porting note: quite slow. Improve performance?
+-- Porting note (#11083): quite slow. Improve performance?
 @[simp]
 theorem normUnit_mul_normUnit (a : α) : normUnit (a * normUnit a) = 1 := by
   nontriviality α using Subsingleton.elim a 0
@@ -1206,7 +1206,7 @@ noncomputable def gcdMonoidOfLCM [DecidableEq α] (lcm : α → α → α)
       apply ac }
 #align gcd_monoid_of_lcm gcdMonoidOfLCM
 
--- Porting note: very slow; improve performance?
+-- Porting note (#11083): very slow; improve performance?
 /-- Define `NormalizedGCDMonoid` on a structure just from the `lcm` and its properties. -/
 noncomputable def normalizedGCDMonoidOfLCM [NormalizationMonoid α] [DecidableEq α] (lcm : α → α → α)
     (dvd_lcm_left : ∀ a b, a ∣ lcm a b) (dvd_lcm_right : ∀ a b, b ∣ lcm a b)
@@ -1351,7 +1351,7 @@ namespace CommGroupWithZero
 
 variable (G₀ : Type*) [CommGroupWithZero G₀] [DecidableEq G₀]
 
--- Porting note: very slow; improve performance?
+-- Porting note (#11083): very slow; improve performance?
 -- see Note [lower instance priority]
 instance (priority := 100) : NormalizedGCDMonoid G₀ where
   normUnit x := if h : x = 0 then 1 else (Units.mk0 x h)⁻¹

Mathlib/Algebra/Lie/Weights/Cartan.lean

@@ -124,7 +124,7 @@ def rootSpaceWeightSpaceProductAux {χ₁ χ₂ χ₃ : H → R} (hχ : χ₁ +
       SetLike.mk_smul_mk]
 #align lie_algebra.root_space_weight_space_product_aux LieAlgebra.rootSpaceWeightSpaceProductAux
 
--- Porting note: this def is _really_ slow
+-- Porting note (#11083): this def is _really_ slow
 -- See https://github.com/leanprover-community/mathlib4/issues/5028
 /-- Given a nilpotent Lie subalgebra `H ⊆ L` together with `χ₁ χ₂ : H → R`, there is a natural
 `R`-bilinear product of root vectors and weight vectors, compatible with the actions of `H`. -/

Mathlib/Analysis/NormedSpace/lpSpace.lean

@@ -479,7 +479,7 @@ theorem eq_zero_iff_coeFn_eq_zero {f : lp E p} : f = 0 ↔ ⇑f = 0 := by
   rw [lp.ext_iff, coeFn_zero]
 #align lp.eq_zero_iff_coe_fn_eq_zero lp.eq_zero_iff_coeFn_eq_zero
 
--- porting note: this was very slow, so I squeezed the `simp` calls
+-- porting note (#11083): this was very slow, so I squeezed the `simp` calls
 @[simp]
 theorem norm_neg ⦃f : lp E p⦄ : ‖-f‖ = ‖f‖ := by
   rcases p.trichotomy with (rfl | rfl | hp)
@@ -504,7 +504,7 @@ instance normedAddCommGroup [hp : Fact (1 ≤ p)] : NormedAddCommGroup (lp E p)
         · cases isEmpty_or_nonempty α
           · -- porting note (#10745): was `simp [lp.eq_zero' f]`
             rw [lp.eq_zero' f]
-            simp only [zero_add, norm_zero, le_refl] -- porting note: just `simp` was slow
+            simp only [zero_add, norm_zero, le_refl] -- porting note (#11083): just `simp` was slow
           refine' (lp.isLUB_norm (f + g)).2 _
           rintro x ⟨i, rfl⟩
           refine' le_trans _ (add_mem_upperBounds_add

Mathlib/Combinatorics/Hindman.lean

@@ -71,7 +71,7 @@ def Ultrafilter.semigroup {M} [Semigroup M] : Semigroup (Ultrafilter M) :=
   { Ultrafilter.mul with
     mul_assoc := fun U V W =>
       Ultrafilter.coe_inj.mp <|
-        -- porting note: `simp` was slow to typecheck, replaced by `simp_rw`
+        -- porting note (#11083): `simp` was slow to typecheck, replaced by `simp_rw`
         Filter.ext' fun p => by simp_rw [Ultrafilter.eventually_mul, mul_assoc] }
 #align ultrafilter.semigroup Ultrafilter.semigroup
 #align ultrafilter.add_semigroup Ultrafilter.addSemigroup

Mathlib/Data/Multiset/Powerset.lean

@@ -78,7 +78,7 @@ theorem powersetAux_perm {l₁ l₂ : List α} (p : l₁ ~ l₂) : powersetAux l
     (powerset_aux'_perm p).trans powersetAux_perm_powersetAux'.symm
 #align multiset.powerset_aux_perm Multiset.powersetAux_perm
 
---Porting note: slightly slower implementation due to `map ofList`
+--Porting note (#11083): slightly slower implementation due to `map ofList`
 /-- The power set of a multiset. -/
 def powerset (s : Multiset α) : Multiset (Multiset α) :=
   Quot.liftOn s

Mathlib/Data/Quot.lean

@@ -117,7 +117,7 @@ theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f
 
 /-- Descends a function `f : α → β → γ` to quotients of `α` and `β`. -/
 -- porting note: removed `@[elab_as_elim]`, gave "unexpected resulting type γ"
--- porting note: removed `@[reducible]` because it caused extremely slow `simp`
+-- porting note (#11083): removed `@[reducible]` because it caused extremely slow `simp`
 protected def lift₂ (f : α → β → γ) (hr : ∀ a b₁ b₂, s b₁ b₂ → f a b₁ = f a b₂)
     (hs : ∀ a₁ a₂ b, r a₁ a₂ → f a₁ b = f a₂ b) (q₁ : Quot r) (q₂ : Quot s) : γ :=
   Quot.lift (fun a ↦ Quot.lift (f a) (hr a))
@@ -132,8 +132,8 @@ theorem lift₂_mk (f : α → β → γ) (hr : ∀ a b₁ b₂, s b₁ b₂ →
 #align quot.lift₂_mk Quot.lift₂_mk
 
 /-- Descends a function `f : α → β → γ` to quotients of `α` and `β` and applies it. -/
--- porting note: removed `@[elab_as_elim]`, gave "unexpected resulting type γ"
--- porting note: removed `@[reducible]` because it caused extremely slow `simp`
+-- porting note (#11083): removed `@[elab_as_elim]`, gave "unexpected resulting type γ"
+-- porting note (#11083): removed `@[reducible]` because it caused extremely slow `simp`
 protected def liftOn₂ (p : Quot r) (q : Quot s) (f : α → β → γ)
     (hr : ∀ a b₁ b₂, s b₁ b₂ → f a b₁ = f a b₂) (hs : ∀ a₁ a₂ b, r a₁ a₂ → f a₁ b = f a₂ b) : γ :=
   Quot.lift₂ f hr hs p q
@@ -164,7 +164,7 @@ theorem map₂_mk (f : α → β → γ) (hr : ∀ a b₁ b₂, s b₁ b₂ →
 #align quot.map₂_mk Quot.map₂_mk
 
 /-- A binary version of `Quot.recOnSubsingleton`. -/
--- porting note: removed `@[reducible]` because it caused extremely slow `simp`
+-- porting note (#11083): removed `@[reducible]` because it caused extremely slow `simp`
 @[elab_as_elim]
 protected def recOnSubsingleton₂ {φ : Quot r → Quot s → Sort*}
     [h : ∀ a b, Subsingleton (φ ⟦a⟧ ⟦b⟧)] (q₁ : Quot r)
@@ -499,7 +499,7 @@ protected theorem lift_mk (f : α → β) (c) (a : α) : lift f c (mk a) = f a :
 
 /-- Lift a constant function on `q : Trunc α`. -/
 -- porting note: removed `@[elab_as_elim]` because it gave "unexpected eliminator resulting type"
--- porting note: removed `@[reducible]` because it caused extremely slow `simp`
+-- porting note (#11083): removed `@[reducible]` because it caused extremely slow `simp`
 protected def liftOn (q : Trunc α) (f : α → β) (c : ∀ a b : α, f a = f b) : β :=
   lift f c q
 #align trunc.lift_on Trunc.liftOn
@@ -555,7 +555,7 @@ instance : LawfulMonad Trunc where
 variable {C : Trunc α → Sort*}
 
 /-- Recursion/induction principle for `Trunc`. -/
--- porting note: removed `@[reducible]` because it caused extremely slow `simp`
+-- porting note (#11083): removed `@[reducible]` because it caused extremely slow `simp`
 @[elab_as_elim]
 protected def rec (f : ∀ a, C (mk a))
     (h : ∀ a b : α, (Eq.ndrec (f a) (Trunc.eq (mk a) (mk b)) : C (mk b)) = f b)
@@ -564,15 +564,15 @@ protected def rec (f : ∀ a, C (mk a))
 #align trunc.rec Trunc.rec
 
 /-- A version of `Trunc.rec` taking `q : Trunc α` as the first argument. -/
--- porting note: removed `@[reducible]` because it caused extremely slow `simp`
+-- porting note (#11083): removed `@[reducible]` because it caused extremely slow `simp`
 @[elab_as_elim]
 protected def recOn (q : Trunc α) (f : ∀ a, C (mk a))
     (h : ∀ a b : α, (Eq.ndrec (f a) (Trunc.eq (mk a) (mk b)) : C (mk b)) = f b) : C q :=
   Trunc.rec f h q
 #align trunc.rec_on Trunc.recOn
 
 /-- A version of `Trunc.recOn` assuming the codomain is a `Subsingleton`. -/
--- porting note: removed `@[reducible]` because it caused extremely slow `simp`
+-- porting note (#11083)s: removed `@[reducible]` because it caused extremely slow `simp`
 @[elab_as_elim]
 protected def recOnSubsingleton [∀ a, Subsingleton (C (mk a))] (q : Trunc α) (f : ∀ a, C (mk a)) :
     C q :=
@@ -624,7 +624,7 @@ theorem surjective_Quotient_mk'' : Function.Surjective (Quotient.mk'' : α → Q
 /-- A version of `Quotient.liftOn` taking `{s : Setoid α}` as an implicit argument instead of an
 instance argument. -/
 -- porting note: removed `@[elab_as_elim]` because it gave "unexpected eliminator resulting type"
--- porting note: removed `@[reducible]` because it caused extremely slow `simp`
+-- porting note (#11083): removed `@[reducible]` because it caused extremely slow `simp`
 protected def liftOn' (q : Quotient s₁) (f : α → φ) (h : ∀ a b, @Setoid.r α s₁ a b → f a = f b) :
     φ :=
   Quotient.liftOn q f h
@@ -643,7 +643,7 @@ protected theorem liftOn'_mk'' (f : α → φ) (h) (x : α) :
 /-- A version of `Quotient.liftOn₂` taking `{s₁ : Setoid α} {s₂ : Setoid β}` as implicit arguments
 instead of instance arguments. -/
 -- porting note: removed `@[elab_as_elim]` because it gave "unexpected eliminator resulting type"
--- porting note: removed `@[reducible]` because it caused extremely slow `simp`
+-- porting note (#11083): removed `@[reducible]` because it caused extremely slow `simp`
 protected def liftOn₂' (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → γ)
     (h : ∀ a₁ a₂ b₁ b₂, @Setoid.r α s₁ a₁ b₁ → @Setoid.r β s₂ a₂ b₂ → f a₁ a₂ = f b₁ b₂) : γ :=
   Quotient.liftOn₂ q₁ q₂ f h
@@ -709,7 +709,7 @@ protected def recOnSubsingleton' {φ : Quotient s₁ → Sort*} [∀ a, Subsingl
 
 /-- A version of `Quotient.recOnSubsingleton₂` taking `{s₁ : Setoid α} {s₂ : Setoid α}`
 as implicit arguments instead of instance arguments. -/
--- porting note: removed `@[reducible]` because it caused extremely slow `simp`
+-- porting note (#11083): removed `@[reducible]` because it caused extremely slow `simp`
 @[elab_as_elim]
 protected def recOnSubsingleton₂' {φ : Quotient s₁ → Quotient s₂ → Sort*}
     [∀ a b, Subsingleton (φ ⟦a⟧ ⟦b⟧)]

Mathlib/FieldTheory/Minpoly/Field.lean

@@ -167,7 +167,7 @@ noncomputable def Fintype.subtypeProd {E : Type*} {X : Set E} (hX : X.Finite) {L
 variable (F E K : Type*) [Field F] [Ring E] [CommRing K] [IsDomain K] [Algebra F E] [Algebra F K]
   [FiniteDimensional F E]
 
--- Porting note: removed `noncomputable!` since it seems not to be slow in lean 4,
+-- Porting note (#11083): removed `noncomputable!` since it seems not to be slow in lean 4,
 -- though it isn't very computable in practice (since neither `finrank` nor `finBasis` are).
 /-- Function from Hom_K(E,L) to pi type Π (x : basis), roots of min poly of x -/
 def rootsOfMinPolyPiType (φ : E →ₐ[F] K)

Mathlib/Geometry/Manifold/VectorBundle/Hom.lean

@@ -40,7 +40,7 @@ variable {𝕜 B F₁ F₂ M : Type*} {E₁ : B → Type*} {E₂ : B → Type*}
 
 local notation "LE₁E₂" => TotalSpace (F₁ →L[𝕜] F₂) (Bundle.ContinuousLinearMap (RingHom.id 𝕜) E₁ E₂)
 
--- Porting note: moved slow parts to separate lemmas
+-- Porting note (#11083): moved slow parts to separate lemmas
 theorem smoothOn_continuousLinearMapCoordChange
     [SmoothVectorBundle F₁ E₁ IB] [SmoothVectorBundle F₂ E₂ IB] [MemTrivializationAtlas e₁]
     [MemTrivializationAtlas e₁'] [MemTrivializationAtlas e₂] [MemTrivializationAtlas e₂'] :

Mathlib/Geometry/RingedSpace/OpenImmersion.lean

@@ -919,7 +919,7 @@ instance sigma_ι_isOpenImmersion [HasStrictTerminalObjects C] :
     suffices IsIso <| (colimit.ι (F ⋙ SheafedSpace.forgetToPresheafedSpace) i ≫
         (preservesColimitIso SheafedSpace.forgetToPresheafedSpace F).inv).c.app <|
       op (H.isOpenMap.functor.obj U) by
-      -- Porting note: just `convert` is very slow, so helps it a bit
+      -- Porting note (#11083): just `convert` is very slow, so helps it a bit
       convert this using 2 <;> congr
     rw [PresheafedSpace.comp_c_app,
       ← PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π]

Mathlib/GroupTheory/GroupAction/ConjAct.lean

@@ -162,7 +162,7 @@ theorem units_smul_def (g : ConjAct Mˣ) (h : M) : g • h = ofConjAct g * h * 
   rfl
 #align conj_act.units_smul_def ConjAct.units_smul_def
 
--- porting note: very slow without `simp only` and need to separate `units_smul_def`
+-- porting note (#11083): very slow without `simp only` and need to separate `units_smul_def`
 -- so that things trigger appropriately
 instance unitsMulDistribMulAction : MulDistribMulAction (ConjAct Mˣ) M where
   one_smul := by simp only [units_smul_def, ofConjAct_one, Units.val_one, one_mul, inv_one,
@@ -194,7 +194,7 @@ section Semiring
 
 variable [Semiring R]
 
--- porting note: very slow without `simp only` and need to separate `units_smul_def`
+-- porting note (#11083): very slow without `simp only` and need to separate `units_smul_def`
 -- so that things trigger appropriately
 instance unitsMulSemiringAction : MulSemiringAction (ConjAct Rˣ) R :=
   { ConjAct.unitsMulDistribMulAction with
@@ -223,7 +223,7 @@ theorem toConjAct_zero : toConjAct (0 : G₀) = 0 :=
   rfl
 #align conj_act.to_conj_act_zero ConjAct.toConjAct_zero
 
--- porting note: very slow without `simp only` and need to separate `smul_def`
+-- porting note (#11083): very slow without `simp only` and need to separate `smul_def`
 -- so that things trigger appropriately
 instance mulAction₀ : MulAction (ConjAct G₀) G₀ where
   one_smul := by
@@ -251,7 +251,7 @@ section DivisionRing
 
 variable [DivisionRing K]
 
--- porting note: very slow without `simp only` and need to separate `smul_def`
+-- porting note (#11083): very slow without `simp only` and need to separate `smul_def`
 -- so that things trigger appropriately
 instance distribMulAction₀ : DistribMulAction (ConjAct K) K :=
   { ConjAct.mulAction₀ with
@@ -269,7 +269,7 @@ variable [Group G]
 
 -- todo: this file is not in good order; I will refactor this after the PR
 
--- porting note: very slow without `simp only` and need to separate `smul_def`
+-- porting note (#11083): very slow without `simp only` and need to separate `smul_def`
 -- so that things trigger appropriately
 instance : MulDistribMulAction (ConjAct G) G where
   smul_mul := by

Mathlib/LinearAlgebra/QuotientPi.lean

@@ -79,7 +79,7 @@ theorem quotientPiLift_mk (p : ∀ i, Submodule R (Ms i)) (f : ∀ i, Ms i →
   rfl
 #align submodule.quotient_pi_lift_mk Submodule.quotientPiLift_mk
 
--- Porting note: split up the definition to avoid timeouts. Still slow.
+-- Porting note (#11083): split up the definition to avoid timeouts. Still slow.
 namespace quotientPi_aux
 
 variable [Fintype ι] [DecidableEq ι] (p : ∀ i, Submodule R (Ms i))

Mathlib/NumberTheory/Bertrand.lean

@@ -66,7 +66,7 @@ theorem real_main_inequality {x : ℝ} (x_large : (512 : ℝ) ≤ x) :
   rw [← div_le_one (rpow_pos_of_pos four_pos x), ← div_div_eq_mul_div, ← rpow_sub four_pos, ←
     mul_div 2 x, mul_div_left_comm, ← mul_one_sub, (by norm_num1 : (1 : ℝ) - 2 / 3 = 1 / 3),
     mul_one_div, ← log_nonpos_iff (hf' x h5), ← hf x h5]
-  -- porting note: the proof was rewritten, because it was too slow
+  -- porting note (#11083): the proof was rewritten, because it was too slow
   have h : ConcaveOn ℝ (Set.Ioi 0.5) f := by
     apply ConcaveOn.sub
     apply ConcaveOn.add

Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean

@@ -291,7 +291,7 @@ theorem FiniteField.two_pow_card {F : Type*} [Fintype F] [Field F] (hF : ringCha
   -- Porting note: The type is actually `PrimitiveAddChar (ZMod (8 : ℕ+)) F`, but this seems faster.
   let ψ₈ : PrimitiveAddChar (ZMod 8) F :=
     primitiveZModChar 8 F (by convert hp2 3 using 1; norm_cast)
-  -- Porting note: unifying this is very slow, so only do it once.
+  -- Porting note (#11083): unifying this is very slow, so only do it once.
   let ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
   let τ : FF := ψ₈char 1
   have τ_spec : τ ^ 4 = -1 := by

Mathlib/Order/CompleteBooleanAlgebra.lean

@@ -373,7 +373,7 @@ section CompleteDistribLattice
 
 variable [CompleteDistribLattice α] {a b : α} {s t : Set α}
 
--- Porting note: this is mysteriously slow. Minimised in
+-- Porting note (#11083): this is mysteriously slow. Minimised in
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Performance.20issue.20with.20.60CompleteBooleanAlgebra.60
 -- but not yet resolved.
 instance OrderDual.completeDistribLattice (α) [CompleteDistribLattice α] :

Mathlib/RingTheory/WittVector/StructurePolynomial.lean

@@ -251,7 +251,7 @@ theorem C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum (Φ : MvPolynomial idx
   rw [bind₁, aeval_wittPolynomial, map_sum, map_sum, Finset.sum_congr rfl]
   intro k hk
   rw [Finset.mem_range, Nat.lt_succ_iff] at hk
-  -- Porting note: was much slower
+  -- Porting note (#11083): was much slower
   -- simp only [← sub_eq_zero, ← RingHom.map_sub, ← C_dvd_iff_zmod, C_eq_coe_nat, ← mul_sub, ←
   --   Nat.cast_pow]
   rw [← sub_eq_zero, ← RingHom.map_sub, ← C_dvd_iff_zmod, C_eq_coe_nat, ← Nat.cast_pow,

Mathlib/Topology/Homotopy/HomotopyGroup.lean

@@ -289,7 +289,7 @@ def homotopyTo (i : N) {p q : Ω^ N X x} (H : p.1.HomotopyRel q.1 (Cube.boundary
       (cCompInsert i).comp H.toContinuousMap.curry).uncurry
 #align gen_loop.homotopy_to GenLoop.homotopyTo
 
--- porting note: `@[simps]` no longer too slow in Lean 4 but does not generate this lemma.
+-- porting note (#11083): `@[simps]` no longer too slow in Lean 4 but does not generate this lemma.
 theorem homotopyTo_apply (i : N) {p q : Ω^ N X x} (H : p.1.HomotopyRel q.1 <| Cube.boundary N)
     (t : I × I) (tₙ : I^{ j // j ≠ i }) :
     homotopyTo i H t tₙ = H (t.fst, Cube.insertAt i (t.snd, tₙ)) :=
@@ -320,7 +320,7 @@ theorem homotopicTo (i : N) {p q : Ω^ N X x} :
           (ContinuousMap.comp ⟨Subtype.val, by continuity⟩ H.toContinuousMap).curry).uncurry.comp <|
     (ContinuousMap.id I).prodMap (Cube.splitAt i).toContinuousMap
 #align gen_loop.homotopy_from GenLoop.homotopyFrom
--- porting note: @[simps!] no longer too slow in Lean 4.
+-- porting note (#11083): @[simps!] no longer too slow in Lean 4.
 #align gen_loop.homotopy_from_apply GenLoop.homotopyFrom_apply
 
 theorem homotopicFrom (i : N) {p q : Ω^ N X x} :

Mathlib/Topology/Metrizable/Uniformity.lean

@@ -180,7 +180,7 @@ theorem le_two_mul_dist_ofPreNNDist (d : X → X → ℝ≥0) (dist_self : ∀ x
 
 end PseudoMetricSpace
 
--- Porting note: this is slower than in Lean3 for some reason...
+-- Porting note (#11083): this is slower than in Lean3 for some reason...
 /-- If `X` is a uniform space with countably generated uniformity filter, there exists a
 `PseudoMetricSpace` structure compatible with the `UniformSpace` structure. Use
 `UniformSpace.pseudoMetricSpace` or `UniformSpace.metricSpace` instead. -/