chore: classify todo porting notes (#11216)

Classifies by adding issue number #11215 to porting notes claiming "TODO".

Mathlib/Algebra/Algebra/Basic.lean

@@ -896,7 +896,7 @@ variable (R)
 #align linear_map.coe_restrict_scalars_eq_coe LinearMap.coe_restrictScalars
 #align linear_map.coe_coe_is_scalar_tower LinearMap.coe_restrictScalars
 
--- Porting note: todo: generalize to `CompatibleSMul`
+-- Porting note (#11215): TODO: generalize to `CompatibleSMul`
 /-- `A`-linearly coerce an `R`-linear map from `M` to `A` to a function, given an algebra `A` over
 a commutative semiring `R` and `M` a module over `R`. -/
 def ltoFun (R : Type u) (M : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid M] [Module R M]

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -1146,7 +1146,8 @@ variable (K)
 variable (f : ∀ i, K i →ₐ[R] B) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h))
   (T : Subalgebra R A) (hT : T = iSup K)
 
--- Porting note: TODO: turn `hT` into an assumption `T ≤ iSup K`. That's what `Set.iUnionLift` needs
+-- Porting note (#11215): TODO: turn `hT` into an assumption `T ≤ iSup K`.
+-- That's what `Set.iUnionLift` needs
 -- Porting note: the proofs of `map_{zero,one,add,mul}` got a bit uglier, probably unification trbls
 /-- Define an algebra homomorphism on a directed supremum of subalgebras by defining
 it on each subalgebra, and proving that it agrees on the intersection of subalgebras. -/

Mathlib/Algebra/BigOperators/Order.lean

@@ -176,7 +176,7 @@ theorem prod_le_univ_prod_of_one_le' [Fintype ι] {s : Finset ι} (w : ∀ x, 1
 #align finset.prod_le_univ_prod_of_one_le' Finset.prod_le_univ_prod_of_one_le'
 #align finset.sum_le_univ_sum_of_nonneg Finset.sum_le_univ_sum_of_nonneg
 
--- Porting Note: TODO -- The two next lemmas give the same lemma in additive version
+-- Porting note (#11215): TODO -- The two next lemmas give the same lemma in additive version
 @[to_additive sum_eq_zero_iff_of_nonneg]
 theorem prod_eq_one_iff_of_one_le' :
     (∀ i ∈ s, 1 ≤ f i) → ((∏ i in s, f i) = 1 ↔ ∀ i ∈ s, f i = 1) := by
@@ -471,7 +471,7 @@ This is a variant (beta-reduced) version of the standard lemma `Finset.sum_lt_su
 convenient for the `gcongr` tactic. -/
 add_decl_doc GCongr.sum_lt_sum_of_nonempty
 
--- Porting note: TODO -- calc indentation
+-- Porting note (#11215): TODO -- calc indentation
 @[to_additive sum_lt_sum_of_subset]
 theorem prod_lt_prod_of_subset' (h : s ⊆ t) {i : ι} (ht : i ∈ t) (hs : i ∉ s) (hlt : 1 < f i)
     (hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j) : ∏ j in s, f j < ∏ j in t, f j := by

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -160,7 +160,7 @@ theorem forget₂_map (X Y : ModuleCat R) (f : X ⟶ Y) :
   rfl
 #align Module.forget₂_map ModuleCat.forget₂_map
 
--- Porting note: TODO: `ofHom` and `asHom` are duplicates!
+-- Porting note (#11215): TODO: `ofHom` and `asHom` are duplicates!
 
 /-- Typecheck a `LinearMap` as a morphism in `Module R`. -/
 def ofHom {R : Type u} [Ring R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y]

Mathlib/Algebra/Category/ModuleCat/Subobject.lean

@@ -102,7 +102,8 @@ are equal if they differ by an element of the image.
 The application is for homology:
 two elements in homology are equal if they differ by a boundary.
 -/
--- Porting note: TODO compiler complains that this is marked with `@[ext]`. Should this be changed?
+-- Porting note (#11215): TODO compiler complains that this is marked with `@[ext]`.
+-- Should this be changed?
 -- @[ext] this is no longer an ext lemma under the current interpretation see eg
 -- the conversation beginning at
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/

Mathlib/Algebra/Group/Equiv/Basic.lean

@@ -233,7 +233,7 @@ theorem coe_toEquiv (f : M ≃* N) : ⇑(f : M ≃ N) = f := rfl
 #align mul_equiv.coe_to_equiv MulEquiv.coe_toEquiv
 #align add_equiv.coe_to_equiv AddEquiv.coe_toEquiv
 
--- Porting note: todo: `MulHom.coe_mk` simplifies `↑f.toMulHom` to `f.toMulHom.toFun`,
+-- Porting note (#11215): TODO: `MulHom.coe_mk` simplifies `↑f.toMulHom` to `f.toMulHom.toFun`,
 -- not `f.toEquiv.toFun`; use higher priority as a workaround
 @[to_additive (attr := simp 1100)]
 theorem coe_toMulHom {f : M ≃* N} : (f.toMulHom : M → N) = f := rfl
@@ -608,7 +608,7 @@ noncomputable def ofBijective {M N F} [Mul M] [Mul N] [FunLike F M N] [MulHomCla
 #align mul_equiv.of_bijective_apply MulEquiv.ofBijective_apply
 #align add_equiv.of_bijective_apply AddEquiv.ofBijective_apply
 
--- Porting note: todo: simplify `symm_apply` to `surjInv`?
+-- Porting note (#11215): TODO: simplify `symm_apply` to `surjInv`?
 @[to_additive (attr := simp)]
 theorem ofBijective_apply_symm_apply {n : N} (f : M →* N) (hf : Bijective f) :
     f ((ofBijective f hf).symm n) = n := (ofBijective f hf).apply_symm_apply n

Mathlib/Algebra/Group/Units.lean

@@ -923,7 +923,7 @@ def unit' (h : IsUnit a) : αˣ := ⟨a, a⁻¹, h.mul_inv_cancel, h.inv_mul_can
 #align is_unit.coe_unit' IsUnit.val_unit'
 #align is_add_unit.coe_add_unit' IsAddUnit.val_addUnit'
 
--- Porting note: TODO: `simps val_inv` fails
+-- Porting note (#11215): TODO: `simps val_inv` fails
 @[to_additive] lemma val_inv_unit' (h : IsUnit a) : ↑(h.unit'⁻¹) = a⁻¹ := rfl
 #align is_unit.coe_inv_unit' IsUnit.val_inv_unit'
 #align is_add_unit.coe_neg_add_unit' IsAddUnit.val_neg_addUnit'

Mathlib/Algebra/Homology/LocalCohomology.lean

@@ -74,7 +74,7 @@ def ringModIdeals (I : D ⥤ Ideal R) : D ⥤ ModuleCat.{u} R where
   map_comp f g := by apply Submodule.linearMap_qext; rfl
 #align local_cohomology.ring_mod_ideals localCohomology.ringModIdeals
 
--- Porting note: TODO:  Once this file is ported, move this instance to the right location.
+-- Porting note (#11215): TODO:  Once this file is ported, move this instance to the right location.
 instance moduleCat_enoughProjectives' : EnoughProjectives (ModuleCat.{u} R) :=
   ModuleCat.moduleCat_enoughProjectives.{u}
 set_option linter.uppercaseLean3 false in

Mathlib/Algebra/Module/Equiv.lean

@@ -46,7 +46,7 @@ variable {N₁ : Type*} {N₂ : Type*} {N₃ : Type*} {N₄ : Type*} {ι : Type*
 section
 
 /-- A linear equivalence is an invertible linear map. -/
--- Porting note: TODO @[nolint has_nonempty_instance]
+-- Porting note (#11215): TODO @[nolint has_nonempty_instance]
 structure LinearEquiv {R : Type*} {S : Type*} [Semiring R] [Semiring S] (σ : R →+* S)
   {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type*) (M₂ : Type*)
   [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends LinearMap σ M M₂, M ≃+ M₂
@@ -186,8 +186,8 @@ instance : FunLike (M ≃ₛₗ[σ] M₂) M M₂ where
   coe_injective' := DFunLike.coe_injective
 
 instance : SemilinearEquivClass (M ≃ₛₗ[σ] M₂) σ M M₂ where
-  map_add := (·.map_add') --map_add' Porting note: TODO why did I need to change this?
-  map_smulₛₗ := (·.map_smul') --map_smul' Porting note: TODO why did I need to change this?
+  map_add := (·.map_add') --map_add' Porting note (#11215): TODO why did I need to change this?
+  map_smulₛₗ := (·.map_smul') --map_smul' Porting note (#11215): TODO why did I need to change this?
 
 -- Porting note: moved to a lower line since there is no shortcut `CoeFun` instance any more
 @[simp]

Mathlib/Algebra/Module/Projective.lean

@@ -171,7 +171,7 @@ end Ring
 --This is in a different section because special universe restrictions are required.
 section OfLiftingProperty
 
--- Porting note: todo: generalize to `P : Type v`?
+-- Porting note (#11215): TODO: generalize to `P : Type v`?
 /-- A module which satisfies the universal property is projective. Note that the universe variables
 in `huniv` are somewhat restricted. -/
 theorem Projective.of_lifting_property' {R : Type u} [Semiring R] {P : Type max u v}
@@ -185,7 +185,7 @@ theorem Projective.of_lifting_property' {R : Type u} [Semiring R] {P : Type max
   .of_lifting_property'' (huniv · _)
 #align module.projective_of_lifting_property' Module.Projective.of_lifting_property'
 
--- Porting note: todo: generalize to `P : Type v`?
+-- Porting note (#11215): TODO: generalize to `P : Type v`?
 /-- A variant of `of_lifting_property'` when we're working over a `[Ring R]`,
 which only requires quantifying over modules with an `AddCommGroup` instance. -/
 theorem Projective.of_lifting_property {R : Type u} [Ring R] {P : Type max u v} [AddCommGroup P]

Mathlib/Algebra/Module/ULift.lean

@@ -55,7 +55,7 @@ instance isScalarTower'' [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N]
 instance [SMul R M] [SMul Rᵐᵒᵖ M] [IsCentralScalar R M] : IsCentralScalar R (ULift M) :=
   ⟨fun r m => congr_arg up <| op_smul_eq_smul r m.down⟩
 
--- Porting note: TODO this takes way longer to elaborate than it should
+-- Porting note (#11215): TODO this takes way longer to elaborate than it should
 @[to_additive]
 instance mulAction [Monoid R] [MulAction R M] : MulAction (ULift R) M where
   smul := (· • ·)
@@ -132,7 +132,8 @@ instance smulWithZero' [Zero R] [Zero M] [SMulWithZero R M] : SMulWithZero R (UL
 instance mulActionWithZero [MonoidWithZero R] [Zero M] [MulActionWithZero R M] :
     MulActionWithZero (ULift R) M :=
   { ULift.smulWithZero with
-    -- Porting note: TODO there seems to be a mismatch in whether the carrier is explicit here
+    -- Porting note (#11215): TODO there seems to be a mismatch in whether
+    -- the carrier is explicit here
     one_smul := one_smul _
     mul_smul := mul_smul }
 #align ulift.mul_action_with_zero ULift.mulActionWithZero

Mathlib/Algebra/Order/Hom/Basic.lean

@@ -133,7 +133,8 @@ theorem le_map_add_map_div [Group α] [AddCommSemigroup β] [LE β] [MulLEAddHom
     (a b : α) : f a ≤ f b + f (a / b) := by
   simpa only [add_comm, div_mul_cancel'] using map_mul_le_add f (a / b) b
 #align le_map_add_map_div le_map_add_map_div
--- #align le_map_add_map_sub le_map_add_map_sub -- Porting note: TODO: `to_additive` clashes
+-- #align le_map_add_map_sub le_map_add_map_sub
+-- Porting note (#11215): TODO: `to_additive` clashes
 
 @[to_additive]
 theorem le_map_div_mul_map_div [Group α] [CommSemigroup β] [LE β] [SubmultiplicativeHomClass F α β]
@@ -147,7 +148,8 @@ theorem le_map_div_add_map_div [Group α] [AddCommSemigroup β] [LE β] [MulLEAd
     (f : F) (a b c : α) : f (a / c) ≤ f (a / b) + f (b / c) := by
     simpa only [div_mul_div_cancel'] using map_mul_le_add f (a / b) (b / c)
 #align le_map_div_add_map_div le_map_div_add_map_div
--- #align le_map_sub_add_map_sub le_map_sub_add_map_sub -- Porting note: TODO: `to_additive` clashes
+-- #align le_map_sub_add_map_sub le_map_sub_add_map_sub
+-- Porting note (#11215): TODO: `to_additive` clashes
 
 namespace Mathlib.Meta.Positivity
 

Mathlib/Algebra/Order/Ring/WithTop.lean

@@ -133,7 +133,7 @@ protected def _root_.MonoidWithZeroHom.withTopMap {R S : Type*} [MulZeroOneClass
       induction' y using WithTop.recTopCoe with y
       · have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
         simp [mul_top hx, mul_top this]
-      · -- Porting note: todo: `simp [← coe_mul]` times out
+      · -- Porting note (#11215): TODO: `simp [← coe_mul]` times out
         simp only [map_coe, ← coe_mul, map_mul] }
 #align monoid_with_zero_hom.with_top_map MonoidWithZeroHom.withTopMap
 

Mathlib/Algebra/Ring/BooleanRing.lean

@@ -183,7 +183,7 @@ def inf : Inf α :=
   ⟨(· * ·)⟩
 #align boolean_ring.has_inf BooleanRing.inf
 
--- Porting note: TODO: add priority 100. lower instance priority
+-- Porting note (#11215): TODO: add priority 100. lower instance priority
 scoped [BooleanAlgebraOfBooleanRing] attribute [instance] BooleanRing.sup
 scoped [BooleanAlgebraOfBooleanRing] attribute [instance] BooleanRing.inf
 open BooleanAlgebraOfBooleanRing
@@ -263,7 +263,7 @@ def toBooleanAlgebra : BooleanAlgebra α :=
       rw [← add_assoc, add_self] }
 #align boolean_ring.to_boolean_algebra BooleanRing.toBooleanAlgebra
 
--- Porting note: TODO: add priority 100. lower instance priority
+-- Porting note (#11215): TODO: add priority 100. lower instance priority
 scoped[BooleanAlgebraOfBooleanRing] attribute [instance] BooleanRing.toBooleanAlgebra
 
 end BooleanRing

Mathlib/Algebra/Star/Module.lean

@@ -145,7 +145,7 @@ theorem IsSelfAdjoint.selfAdjointPart_apply {x : A} (hx : IsSelfAdjoint x) :
     selfAdjointPart R x = ⟨x, hx⟩ :=
   Subtype.eq (hx.coe_selfAdjointPart_apply R)
 
--- Porting note: todo: make it a `simp`
+-- Porting note (#11215): TODO: make it a `simp`
 theorem selfAdjointPart_comp_subtype_selfAdjoint :
     (selfAdjointPart R).comp (selfAdjoint.submodule R A).subtype = .id :=
   LinearMap.ext fun x ↦ x.2.selfAdjointPart_apply R
@@ -154,17 +154,17 @@ theorem IsSelfAdjoint.skewAdjointPart_apply {x : A} (hx : IsSelfAdjoint x) :
     skewAdjointPart R x = 0 := Subtype.eq <| by
   rw [skewAdjointPart_apply_coe, hx.star_eq, sub_self, smul_zero, ZeroMemClass.coe_zero]
 
--- Porting note: todo: make it a `simp`
+-- Porting note (#11215): TODO: make it a `simp`
 theorem skewAdjointPart_comp_subtype_selfAdjoint :
     (skewAdjointPart R).comp (selfAdjoint.submodule R A).subtype = 0 :=
   LinearMap.ext fun x ↦ x.2.skewAdjointPart_apply R
 
--- Porting note: todo: make it a `simp`
+-- Porting note (#11215): TODO: make it a `simp`
 theorem selfAdjointPart_comp_subtype_skewAdjoint :
     (selfAdjointPart R).comp (skewAdjoint.submodule R A).subtype = 0 :=
   LinearMap.ext fun ⟨x, (hx : _ = _)⟩ ↦ Subtype.eq <| by simp [hx]
 
--- Porting note: todo: make it a `simp`
+-- Porting note (#11215): TODO: make it a `simp`
 theorem skewAdjointPart_comp_subtype_skewAdjoint :
     (skewAdjointPart R).comp (skewAdjoint.submodule R A).subtype = .id :=
   LinearMap.ext fun ⟨x, (hx : _ = _)⟩ ↦ Subtype.eq <| by

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

@@ -1365,7 +1365,7 @@ theorem ContDiffOn.neg {s : Set E} {f : E → F} (hf : ContDiffOn 𝕜 n f s) :
 
 variable {i : ℕ}
 
--- Porting note: TODO: define `Neg` instance on `ContinuousLinearEquiv`,
+-- Porting note (#11215): TODO: define `Neg` instance on `ContinuousLinearEquiv`,
 -- prove it from `ContinuousLinearEquiv.iteratedFDerivWithin_comp_left`
 theorem iteratedFDerivWithin_neg_apply {f : E → F} (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
     iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x := by
@@ -1617,7 +1617,7 @@ end SMul
 
 /-! ### Constant scalar multiplication
 
-Porting note: TODO: generalize results in this section.
+Porting note (#11215): TODO: generalize results in this section.
 
 1. It should be possible to assume `[Monoid R] [DistribMulAction R F] [SMulCommClass 𝕜 R F]`.
 2. If `c` is a unit (or `R` is a group), then one can drop `ContDiff*` assumptions in some

Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean

@@ -56,7 +56,7 @@ variable {b : E × F → G} {u : Set (E × F)}
 
 open NormedField
 
--- Porting note: todo: rewrite/golf using analytic functions?
+-- Porting note (#11215): TODO: rewrite/golf using analytic functions?
 @[fun_prop]
 theorem IsBoundedBilinearMap.hasStrictFDerivAt (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) :
     HasStrictFDerivAt b (h.deriv p) p := by

Mathlib/Analysis/Normed/Group/Quotient.lean

@@ -404,7 +404,7 @@ theorem norm_lift_le {N : Type*} [SeminormedAddCommGroup N] (S : AddSubgroup M)
     ‖lift S f hf‖ ≤ ‖f‖ :=
   opNorm_le_bound _ (norm_nonneg f) (norm_lift_apply_le f hf)
 
--- Porting note: todo: deprecate?
+-- Porting note (#11215): TODO: deprecate?
 theorem lift_norm_le {N : Type*} [SeminormedAddCommGroup N] (S : AddSubgroup M)
     (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0) {c : ℝ≥0} (fb : ‖f‖ ≤ c) :
     ‖lift S f hf‖ ≤ c :=

Mathlib/Analysis/SpecialFunctions/Exp.lean

@@ -353,11 +353,13 @@ theorem tendsto_exp_comp_nhds_zero {f : α → ℝ} :
 theorem openEmbedding_exp : OpenEmbedding exp :=
   isOpen_Ioi.openEmbedding_subtype_val.comp expOrderIso.toHomeomorph.openEmbedding
 
--- Porting note: new lemma; TODO: backport & make `@[simp]`
+-- Porting note: new lemma;
+-- Porting note (#11215): TODO: backport & make `@[simp]`
 theorem map_exp_nhds (x : ℝ) : map exp (𝓝 x) = 𝓝 (exp x) :=
   openEmbedding_exp.map_nhds_eq x
 
--- Porting note: new lemma; TODO: backport & make `@[simp]`
+-- Porting note: new lemma;
+-- Porting note (#11215): TODO: backport & make `@[simp]`
 theorem comap_exp_nhds_exp (x : ℝ) : comap exp (𝓝 (exp x)) = 𝓝 x :=
   (openEmbedding_exp.nhds_eq_comap x).symm
 

Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean

@@ -221,7 +221,8 @@ open scoped BigOperators
 where the main point of the bound is that it tends to `0`. The goal is to deduce the series
 expansion of the logarithm, in `hasSum_pow_div_log_of_abs_lt_1`.
 
-Porting note: TODO: use one of generic theorems about Taylor's series to prove this estimate.
+Porting note (#11215): TODO: use one of generic theorems about Taylor's series
+to prove this estimate.
 -/
 theorem abs_log_sub_add_sum_range_le {x : ℝ} (h : |x| < 1) (n : ℕ) :
     |(∑ i in range n, x ^ (i + 1) / (i + 1)) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|) := by

Mathlib/CategoryTheory/Conj.lean

@@ -118,7 +118,7 @@ theorem conj_pow (f : End X) (n : ℕ) : α.conj (f ^ n) = α.conj f ^ n :=
   α.conj.toMonoidHom.map_pow f n
 #align category_theory.iso.conj_pow CategoryTheory.Iso.conj_pow
 
--- Porting note: todo: change definition so that `conjAut_apply` becomes a `rfl`?
+-- Porting note (#11215): TODO: change definition so that `conjAut_apply` becomes a `rfl`?
 /-- `conj` defines a group isomorphisms between groups of automorphisms -/
 def conjAut : Aut X ≃* Aut Y :=
   (Aut.unitsEndEquivAut X).symm.trans <| (Units.mapEquiv α.conj).trans <| Aut.unitsEndEquivAut Y

Mathlib/CategoryTheory/Endomorphism.lean

@@ -59,11 +59,11 @@ def of (f : X ⟶ X) : End X := f
 def asHom (f : End X) : X ⟶ X := f
 #align category_theory.End.as_hom CategoryTheory.End.asHom
 
-@[simp] -- Porting note: todo: use `of`/`asHom`?
+@[simp] -- Porting note (#11215): TODO: use `of`/`asHom`?
 theorem one_def : (1 : End X) = 𝟙 X := rfl
 #align category_theory.End.one_def CategoryTheory.End.one_def
 
-@[simp] -- Porting note: todo: use `of`/`asHom`?
+@[simp] -- Porting note (#11215): TODO: use `of`/`asHom`?
 theorem mul_def (xs ys : End X) : xs * ys = ys ≫ xs := rfl
 #align category_theory.End.mul_def CategoryTheory.End.mul_def
 

Mathlib/CategoryTheory/Monoidal/Functor.lean

@@ -90,7 +90,7 @@ structure LaxMonoidalFunctor extends C ⥤ D where
     by aesop_cat
 #align category_theory.lax_monoidal_functor CategoryTheory.LaxMonoidalFunctor
 
--- Porting note: todo: remove this configuration and use the default configuration.
+-- Porting note (#11215): TODO: remove this configuration and use the default configuration.
 -- We keep this to be consistent with Lean 3.
 -- See also `initialize_simps_projections MonoidalFunctor` below.
 -- This may require waiting on https://github.com/leanprover-community/mathlib4/pull/2936

Mathlib/CategoryTheory/PathCategory.lean

@@ -181,7 +181,7 @@ theorem composePath_comp {X Y Z : C} (f : Path X Y) (g : Path Y Z) :
 #align category_theory.compose_path_comp CategoryTheory.composePath_comp
 
 @[simp]
--- Porting note: TODO get rid of `(id X : C)` somehow?
+-- Porting note (#11215): TODO get rid of `(id X : C)` somehow?
 theorem composePath_id {X : Paths C} : composePath (𝟙 X) = 𝟙 (id X : C) := rfl
 #align category_theory.compose_path_id CategoryTheory.composePath_id
 

Mathlib/Combinatorics/Configuration.lean

@@ -58,7 +58,7 @@ instance [Finite P] : Finite (Dual P) :=
 instance [h : Fintype P] : Fintype (Dual P) :=
   h
 
--- Porting note: TODO: figure out if this is needed.
+-- Porting note (#11215): TODO: figure out if this is needed.
 set_option synthInstance.checkSynthOrder false in
 instance : Membership (Dual L) (Dual P) :=
   ⟨Function.swap (Membership.mem : P → L → Prop)⟩

Mathlib/Combinatorics/Young/YoungDiagram.lean

@@ -70,7 +70,7 @@ namespace YoungDiagram
 
 instance : SetLike YoungDiagram (ℕ × ℕ)
     where
-  -- Porting note: TODO: figure out how to do this correctly
+  -- Porting note (#11215): TODO: figure out how to do this correctly
   coe := fun y => y.cells
   coe_injective' μ ν h := by rwa [YoungDiagram.ext_iff, ← Finset.coe_inj]
 

Mathlib/Data/Analysis/Filter.lean

@@ -22,7 +22,7 @@ This file provides infrastructure to compute with filters.
 
 open Set Filter
 
--- Porting note: TODO write doc strings
+-- Porting note (#11215): TODO write doc strings
 /-- A `CFilter α σ` is a realization of a filter (base) on `α`,
   represented by a type `σ` together with operations for the top element and
   the binary `inf` operation. -/
@@ -94,7 +94,7 @@ theorem mem_toFilter_sets (F : CFilter (Set α) σ) {a : Set α} : a ∈ F.toFil
 
 end CFilter
 
--- Porting note: TODO write doc strings
+-- Porting note (#11215): TODO write doc strings
 /-- A realizer for filter `f` is a cfilter which generates `f`. -/
 structure Filter.Realizer (f : Filter α) where
   σ : Type*