[Merged by Bors] - chore: classify new theorem / theorem porting notes

Mathlib/Algebra/FreeMonoid/Basic.lean

@@ -231,7 +231,7 @@ def lift : (α → M) ≃ (FreeMonoid α →* M) where
 #align free_monoid.lift FreeMonoid.lift
 #align free_add_monoid.lift FreeAddMonoid.lift
 
--- Porting note: new
+-- Porting note (#10756): new theorem
 @[to_additive (attr := simp)]
 theorem lift_ofList (f : α → M) (l : List α) : lift f (ofList l) = (l.map f).prod :=
   prodAux_eq _

Mathlib/Algebra/Ring/Equiv.lean

@@ -285,7 +285,7 @@ theorem symm_symm (e : R ≃+* S) : e.symm.symm = e :=
   ext fun _ => rfl
 #align ring_equiv.symm_symm RingEquiv.symm_symm
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 @[simp]
 theorem symm_refl : (RingEquiv.refl R).symm = RingEquiv.refl R :=
   rfl

Mathlib/Algebra/Star/Basic.lean

@@ -338,7 +338,7 @@ theorem star_natCast [NonAssocSemiring R] [StarRing R] (n : ℕ) : star (n : R)
   (congr_arg unop (map_natCast (starRingEquiv : R ≃+* Rᵐᵒᵖ) n)).trans (unop_natCast _)
 #align star_nat_cast star_natCast
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 @[simp]
 theorem star_ofNat [NonAssocSemiring R] [StarRing R] (n : ℕ) [n.AtLeastTwo] :
     star (no_index (OfNat.ofNat n) : R) = OfNat.ofNat n :=

Mathlib/Analysis/Calculus/Deriv/Add.lean

@@ -81,7 +81,7 @@ theorem deriv_add (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g
   (hf.hasDerivAt.add hg.hasDerivAt).deriv
 #align deriv_add deriv_add
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 theorem HasStrictDerivAt.add_const (c : F) (hf : HasStrictDerivAt f f' x) :
     HasStrictDerivAt (fun y ↦ f y + c) f' x :=
   add_zero f' ▸ hf.add (hasStrictDerivAt_const x c)
@@ -115,7 +115,7 @@ theorem deriv_add_const' (c : F) : (deriv fun y => f y + c) = deriv f :=
   funext fun _ => deriv_add_const c
 #align deriv_add_const' deriv_add_const'
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 theorem HasStrictDerivAt.const_add (c : F) (hf : HasStrictDerivAt f f' x) :
     HasStrictDerivAt (fun y ↦ c + f y) f' x :=
   zero_add f' ▸ (hasStrictDerivAt_const x c).add hf

Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

@@ -67,13 +67,13 @@ end Module
 
 namespace FormalMultilinearSeries
 
-@[simp] -- Porting note: new; was not needed in Lean 3
+@[simp] -- Porting note (#10756): new theorem; was not needed in Lean 3
 theorem zero_apply (n : ℕ) : (0 : FormalMultilinearSeries 𝕜 E F) n = 0 := rfl
 
-@[simp] -- Porting note: new; was not needed in Lean 3
+@[simp] -- Porting note (#10756): new theorem; was not needed in Lean 3
 theorem neg_apply (f : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : (-f) n = - f n := rfl
 
-@[ext] -- Porting note: new theorem
+@[ext] -- Porting note (#10756): new theorem
 protected theorem ext {p q : FormalMultilinearSeries 𝕜 E F} (h : ∀ n, p n = q n) : p = q :=
   funext h
 

Mathlib/Analysis/Convex/Body.lean

@@ -67,7 +67,7 @@ protected theorem isCompact (K : ConvexBody V) : IsCompact (K : Set V) :=
   K.isCompact'
 #align convex_body.is_compact ConvexBody.isCompact
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 protected theorem isClosed [T2Space V] (K : ConvexBody V) : IsClosed (K : Set V) :=
   K.isCompact.isClosed
 

Mathlib/Analysis/Matrix.lean

@@ -76,10 +76,10 @@ protected def seminormedAddCommGroup : SeminormedAddCommGroup (Matrix m n α) :=
 
 attribute [local instance] Matrix.seminormedAddCommGroup
 
--- Porting note: new (along with all the uses of this lemma below)
+-- Porting note (#10756): new theorem (along with all the uses of this lemma below)
 theorem norm_def (A : Matrix m n α) : ‖A‖ = ‖fun i j => A i j‖ := rfl
 
--- Porting note: new  (along with all the uses of this lemma below)
+-- Porting note (#10756): new theorem (along with all the uses of this lemma below)
 theorem nnnorm_def (A : Matrix m n α) : ‖A‖₊ = ‖fun i j => A i j‖₊ := rfl
 
 theorem norm_le_iff {r : ℝ} (hr : 0 ≤ r) {A : Matrix m n α} : ‖A‖ ≤ r ↔ ∀ i j, ‖A i j‖ ≤ r := by

Mathlib/Analysis/Normed/Group/AddTorsor.lean

@@ -96,7 +96,7 @@ theorem dist_vadd_cancel_left (v : V) (x y : P) : dist (v +ᵥ x) (v +ᵥ y) = d
   dist_vadd _ _ _
 #align dist_vadd_cancel_left dist_vadd_cancel_left
 
--- Porting note: new
+-- Porting note (#10756): new theorem
 theorem nndist_vadd_cancel_left (v : V) (x y : P) : nndist (v +ᵥ x) (v +ᵥ y) = nndist x y :=
   NNReal.eq <| dist_vadd_cancel_left _ _ _
 
@@ -143,7 +143,7 @@ theorem dist_vsub_cancel_left (x y z : P) : dist (x -ᵥ y) (x -ᵥ z) = dist y
   rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]
 #align dist_vsub_cancel_left dist_vsub_cancel_left
 
--- Porting note: new
+-- Porting note (#10756): new theorem
 @[simp]
 theorem nndist_vsub_cancel_left (x y z : P) : nndist (x -ᵥ y) (x -ᵥ z) = nndist y z :=
   NNReal.eq <| dist_vsub_cancel_left _ _ _

Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean

@@ -80,7 +80,7 @@ theorem le_opNorm₂ [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[
 alias le_op_norm₂ :=
   le_opNorm₂ -- deprecated on 2024-02-02
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 theorem le_of_opNorm₂_le_of_le [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) {x : E} {y : F}
     {a b c : ℝ} (hf : ‖f‖ ≤ a) (hx : ‖x‖ ≤ b) (hy : ‖y‖ ≤ c) :
     ‖f x y‖ ≤ a * b * c :=

Mathlib/Analysis/SpecialFunctions/Exp.lean

@@ -353,12 +353,12 @@ 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;
+-- Porting note (#10756): 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;
+-- Porting note (#10756): 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/Basic.lean

@@ -383,7 +383,7 @@ theorem log_prod {α : Type*} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈ s
     simp [ih hf.2, log_mul hf.1 (Finset.prod_ne_zero_iff.2 hf.2)]
 #align real.log_prod Real.log_prod
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 protected theorem _root_.Finsupp.log_prod {α β : Type*} [Zero β] (f : α →₀ β) (g : α → β → ℝ)
     (hg : ∀ a, g a (f a) = 0 → f a = 0) : log (f.prod g) = f.sum fun a b ↦ log (g a b) :=
   log_prod _ _ fun _x hx h₀ ↦ Finsupp.mem_support_iff.1 hx <| hg _ h₀

Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean

@@ -164,7 +164,7 @@ theorem one_of_one_le (h : 1 ≤ x) : smoothTransition x = 1 :=
   (div_eq_one_iff_eq <| (pos_denom x).ne').2 <| by rw [zero_of_nonpos (sub_nonpos.2 h), add_zero]
 #align real.smooth_transition.one_of_one_le Real.smoothTransition.one_of_one_le
 
-@[simp] -- Porting note: new theorem
+@[simp] -- Porting note (#10756): new theorem
 nonrec theorem zero_iff_nonpos : smoothTransition x = 0 ↔ x ≤ 0 := by
   simp only [smoothTransition, _root_.div_eq_zero_iff, (pos_denom x).ne', zero_iff_nonpos, or_false]
 

Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean

@@ -45,7 +45,7 @@ class IsReflexivePair (f g : A ⟶ B) : Prop where
   common_section' : ∃ s : B ⟶ A, s ≫ f = 𝟙 B ∧ s ≫ g = 𝟙 B
 #align category_theory.is_reflexive_pair CategoryTheory.IsReflexivePair
 
--- Porting note: added theorem, because of unsupported infer kinds
+-- Porting note (#10756): added theorem, because of unsupported infer kinds
 theorem IsReflexivePair.common_section (f g : A ⟶ B) [IsReflexivePair f g] :
     ∃ s : B ⟶ A, s ≫ f = 𝟙 B ∧ s ≫ g = 𝟙 B := IsReflexivePair.common_section'
 
@@ -56,7 +56,7 @@ class IsCoreflexivePair (f g : A ⟶ B) : Prop where
   common_retraction' : ∃ s : B ⟶ A, f ≫ s = 𝟙 A ∧ g ≫ s = 𝟙 A
 #align category_theory.is_coreflexive_pair CategoryTheory.IsCoreflexivePair
 
--- Porting note: added theorem, because of unsupported infer kinds
+-- Porting note (#10756): added theorem, because of unsupported infer kinds
 theorem IsCoreflexivePair.common_retraction (f g : A ⟶ B) [IsCoreflexivePair f g] :
     ∃ s : B ⟶ A, f ≫ s = 𝟙 A ∧ g ≫ s = 𝟙 A := IsCoreflexivePair.common_retraction'
 

Mathlib/Data/Bool/Basic.lean

@@ -68,11 +68,11 @@ theorem decide_or (p q : Prop) [Decidable p] [Decidable q] : decide (p ∨ q) =
 theorem not_false' : ¬false := nofun
 #align bool.not_ff Bool.not_false'
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 theorem eq_iff_eq_true_iff {a b : Bool} : a = b ↔ ((a = true) ↔ (b = true)) := by
   cases a <;> cases b <;> simp
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 /- Even though `DecidableEq α` implies an instance of (`Lawful`)`BEq α`, we keep the seemingly
 redundant typeclass assumptions so that the theorem is also applicable for types that have
 overridden this default instance of `LawfulBEq α` -/
@@ -82,7 +82,7 @@ theorem beq_eq_decide_eq {α} [BEq α] [LawfulBEq α] [DecidableEq α]
   · simp [ne_of_beq_false h]
   · simp [eq_of_beq h]
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 theorem beq_comm {α} [BEq α] [LawfulBEq α] {a b : α} : (a == b) = (b == a) :=
   eq_iff_eq_true_iff.2 (by simp [@eq_comm α])
 

Mathlib/Data/Complex/Basic.lean

@@ -502,7 +502,7 @@ theorem I_pow_bit1 (n : ℕ) : I ^ bit1 n = (-1 : ℂ) ^ n * I := by rw [pow_bit
 set_option linter.uppercaseLean3 false in
 #align complex.I_pow_bit1 Complex.I_pow_bit1
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 -- See note [no_index around OfNat.ofNat]
 @[simp, norm_cast]
 theorem ofReal_ofNat (n : ℕ) [n.AtLeastTwo] :

Mathlib/Data/ENNReal/Basic.lean

@@ -426,7 +426,7 @@ lemma coe_ne_one : (r : ℝ≥0∞) ≠ 1 ↔ r ≠ 1 := coe_eq_one.not
 #noalign ennreal.coe_bit1
 
 -- See note [no_index around OfNat.ofNat]
-@[simp, norm_cast] -- Porting note: new
+@[simp, norm_cast] -- Porting note (#10756): new theorem
 theorem coe_ofNat (n : ℕ) [n.AtLeastTwo] :
     ((no_index (OfNat.ofNat n) : ℝ≥0) : ℝ≥0∞) = OfNat.ofNat n := rfl
 

Mathlib/Data/ENat/Basic.lean

@@ -128,13 +128,13 @@ def recTopCoe {C : ℕ∞ → Sort*} (top : C ⊤) (coe : ∀ a : ℕ, C a) : 
   | none => top
   | Option.some a => coe a
 
--- Porting note: new theorem copied from `WithTop`
+-- Porting note (#10756): new theorem copied from `WithTop`
 @[simp]
 theorem recTopCoe_top {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) :
     @recTopCoe C d f ⊤ = d :=
   rfl
 
--- Porting note: new theorem copied from `WithTop`
+-- Porting note (#10756): new theorem copied from `WithTop`
 @[simp]
 theorem recTopCoe_coe {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) (x : ℕ) :
     @recTopCoe C d f ↑x = f x :=
@@ -154,7 +154,7 @@ theorem recTopCoe_ofNat {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a
     @recTopCoe C d f (no_index (OfNat.ofNat x)) = f (OfNat.ofNat x) :=
   rfl
 
--- Porting note: new theorem copied from `WithTop`
+-- Porting note (#10756): new theorem copied from `WithTop`
 @[simp]
 theorem top_ne_coe (a : ℕ) : ⊤ ≠ (a : ℕ∞) :=
   nofun
@@ -164,7 +164,7 @@ theorem top_ne_coe (a : ℕ) : ⊤ ≠ (a : ℕ∞) :=
 theorem top_ne_ofNat (a : ℕ) [a.AtLeastTwo] : ⊤ ≠ (no_index (OfNat.ofNat a : ℕ∞)) :=
   nofun
 
--- Porting note: new theorem copied from `WithTop`
+-- Porting note (#10756): new theorem copied from `WithTop`
 @[simp]
 theorem coe_ne_top (a : ℕ) : (a : ℕ∞) ≠ ⊤ :=
   nofun
@@ -174,7 +174,7 @@ theorem coe_ne_top (a : ℕ) : (a : ℕ∞) ≠ ⊤ :=
 theorem ofNat_ne_top (a : ℕ) [a.AtLeastTwo] : (no_index (OfNat.ofNat a : ℕ∞)) ≠ ⊤ :=
   nofun
 
--- Porting note: new theorem copied from `WithTop`
+-- Porting note (#10756): new theorem copied from `WithTop`
 @[simp]
 theorem top_sub_coe (a : ℕ) : (⊤ : ℕ∞) - a = ⊤ :=
   WithTop.top_sub_coe
@@ -192,7 +192,7 @@ theorem top_sub_ofNat (a : ℕ) [a.AtLeastTwo] : (⊤ : ℕ∞) - (no_index (OfN
 theorem zero_lt_top : (0 : ℕ∞) < ⊤ :=
   WithTop.zero_lt_top
 
--- Porting note: new theorem copied from `WithTop`
+-- Porting note (#10756): new theorem copied from `WithTop`
 theorem sub_top (a : ℕ∞) : a - ⊤ = 0 :=
   WithTop.sub_top
 

Mathlib/Data/Fintype/Card.lean

@@ -637,7 +637,7 @@ namespace Finite
 
 variable [Finite α]
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 theorem surjective_of_injective {f : α → α} (hinj : Injective f) : Surjective f := by
   intro x
   have := Classical.propDecidable

Mathlib/Data/List/AList.lean

@@ -480,7 +480,7 @@ theorem mem_lookup_union {a} {b : β a} {s₁ s₂ : AList β} :
   mem_dlookup_kunion
 #align alist.mem_lookup_union AList.mem_lookup_union
 
--- Porting note: new theorem, version of `mem_lookup_union` with LHS in simp-normal form
+-- Porting note (#10756): new theorem, version of `mem_lookup_union` with LHS in simp-normal form
 @[simp]
 theorem lookup_union_eq_some {a} {b : β a} {s₁ s₂ : AList β} :
     lookup a (s₁ ∪ s₂) = some b ↔ lookup a s₁ = some b ∨ a ∉ s₁ ∧ lookup a s₂ = some b :=

Mathlib/Data/List/Chain.lean

@@ -376,7 +376,7 @@ theorem Chain'.append_overlap {l₁ l₂ l₃ : List α} (h₁ : Chain' R (l₁
     simpa only [getLast?_append_of_ne_nil _ hn] using (chain'_append.1 h₂).2.2
 #align list.chain'.append_overlap List.Chain'.append_overlap
 
--- Porting note: new
+-- Porting note (#10756): new lemma
 lemma chain'_join : ∀ {L : List (List α)}, [] ∉ L →
     (Chain' R L.join ↔ (∀ l ∈ L, Chain' R l) ∧
     L.Chain' (fun l₁ l₂ => ∀ᵉ (x ∈ l₁.getLast?) (y ∈ l₂.head?), R x y))

Mathlib/Data/List/Cycle.lean

@@ -261,7 +261,7 @@ theorem prev_mem (h : x ∈ l) : l.prev x h ∈ l := by
       · exact mem_cons_of_mem _ (hl _ _)
 #align list.prev_mem List.prev_mem
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 theorem next_get : ∀ (l : List α) (_h : Nodup l) (i : Fin l.length),
     next l (l.get i) (get_mem _ _ _) = l.get ⟨(i + 1) % l.length,
       Nat.mod_lt _ (i.1.zero_le.trans_lt i.2)⟩
@@ -846,7 +846,7 @@ nonrec theorem prev_reverse_eq_next (s : Cycle α) : ∀ (hs : Nodup s) (x : α)
   Quotient.inductionOn' s prev_reverse_eq_next
 #align cycle.prev_reverse_eq_next Cycle.prev_reverse_eq_next
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 @[simp]
 nonrec theorem prev_reverse_eq_next' (s : Cycle α) (hs : Nodup s.reverse) (x : α)
     (hx : x ∈ s.reverse) :
@@ -859,7 +859,7 @@ theorem next_reverse_eq_prev (s : Cycle α) (hs : Nodup s) (x : α) (hx : x ∈
   simp [← prev_reverse_eq_next]
 #align cycle.next_reverse_eq_prev Cycle.next_reverse_eq_prev
 
--- Porting note: new theorem
+-- Porting note (#10756): new theorem
 @[simp]
 theorem next_reverse_eq_prev' (s : Cycle α) (hs : Nodup s.reverse) (x : α) (hx : x ∈ s.reverse) :
     s.reverse.next hs x hx = s.prev (nodup_reverse_iff.mp hs) x (mem_reverse_iff.mp hx) := by

Mathlib/Data/List/Indexes.lean

@@ -42,7 +42,7 @@ theorem mapIdx_nil {α β} (f : ℕ → α → β) : mapIdx f [] = [] :=
   rfl
 #align list.map_with_index_nil List.mapIdx_nil
 
--- Porting note: new theorem.
+-- Porting note (#10756): new theorem.
 protected theorem oldMapIdxCore_eq (l : List α) (f : ℕ → α → β) (n : ℕ) :
     l.oldMapIdxCore f n = l.oldMapIdx fun i a ↦ f (i + n) a := by
   induction' l with hd tl hl generalizing f n
@@ -56,7 +56,7 @@ protected theorem oldMapIdxCore_eq (l : List α) (f : ℕ → α → β) (n : 
 --   1. Prove that `oldMapIdxCore f (l ++ [e]) = oldMapIdxCore f l ++ [f l.length e]`
 --   2. Prove that `oldMapIdx f (l ++ [e]) = oldMapIdx f l ++ [f l.length e]`
 --   3. Prove list induction using `∀ l e, p [] → (p l → p (l ++ [e])) → p l`
--- Porting note: new theorem.
+-- Porting note (#10756): new theorem.
 theorem list_reverse_induction (p : List α → Prop) (base : p [])
     (ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])) : (∀ (l : List α), p l) := by
   let q := fun l ↦ p (reverse l)
@@ -69,7 +69,7 @@ theorem list_reverse_induction (p : List α → Prop) (base : p [])
   · apply pq; simp only [reverse_nil, base]
   · apply pq; simp only [reverse_cons]; apply ind; apply qp; rw [reverse_reverse]; exact ih
 
--- Porting note: new theorem.
+-- Porting note (#10756): new theorem.
 protected theorem oldMapIdxCore_append : ∀ (f : ℕ → α → β) (n : ℕ) (l₁ l₂ : List α),
     List.oldMapIdxCore f n (l₁ ++ l₂) =
     List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂ := by
@@ -90,15 +90,15 @@ protected theorem oldMapIdxCore_append : ∀ (f : ℕ → α → β) (n : ℕ) (
         simp only [length_append, h]
       rw [Nat.add_assoc]; simp only [Nat.add_comm]
 
--- Porting note: new theorem.
+-- Porting note (#10756): new theorem.
 protected theorem oldMapIdx_append : ∀ (f : ℕ → α → β) (l : List α) (e : α),
     List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f l.length e] := by
   intros f l e
   unfold List.oldMapIdx
   rw [List.oldMapIdxCore_append f 0 l [e]]
   simp only [zero_add, append_cancel_left_eq]; rfl
 
--- Porting note: new theorem.
+-- Porting note (#10756): new theorem.
 theorem mapIdxGo_append : ∀ (f : ℕ → α → β) (l₁ l₂ : List α) (arr : Array β),
     mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (List.toArray (mapIdx.go f l₁ arr)) := by
   intros f l₁ l₂ arr
@@ -115,7 +115,7 @@ theorem mapIdxGo_append : ∀ (f : ℕ → α → β) (l₁ l₂ : List α) (arr
       · simp only [cons_append, length_cons, length_append, Nat.succ.injEq] at h
         simp only [length_append, h]
 
--- Porting note: new theorem.
+-- Porting note (#10756): new theorem.
 theorem mapIdxGo_length : ∀ (f : ℕ → α → β) (l : List α) (arr : Array β),
     length (mapIdx.go f l arr) = length l + arr.size := by
   intro f l
@@ -124,7 +124,7 @@ theorem mapIdxGo_length : ∀ (f : ℕ → α → β) (l : List α) (arr : Array
   · intro; simp only [mapIdx.go]; rw [ih]; simp only [Array.size_push, length_cons];
     simp only [Nat.add_succ, add_zero, Nat.add_comm]
 
--- Porting note: new theorem.
+-- Porting note (#10756): new theorem.
 theorem mapIdx_append_one : ∀ (f : ℕ → α → β) (l : List α) (e : α),
     mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e] := by
   intros f l e
@@ -133,7 +133,7 @@ theorem mapIdx_append_one : ∀ (f : ℕ → α → β) (l : List α) (e : α),
   simp only [mapIdx.go, Array.size_toArray, mapIdxGo_length, length_nil, add_zero, Array.toList_eq,
     Array.push_data, Array.data_toArray]
 
--- Porting note: new theorem.
+-- Porting note (#10756): new theorem.
 protected theorem new_def_eq_old_def :
     ∀ (f : ℕ → α → β) (l : List α), l.mapIdx f = List.oldMapIdx f l := by
   intro f