[Merged by Bors] - chore: change from plural to singular in porting notes

Mathlib/Algebra/Group/Pi/Basic.lean

@@ -388,7 +388,7 @@ theorem mulSingle_one (i : I) : mulSingle i (1 : f i) = 1 :=
 #align pi.mul_single_one Pi.mulSingle_one
 #align pi.single_zero Pi.single_zero
 
--- Porting notes:
+-- Porting note:
 -- 1) Why do I have to specify the type of `mulSingle i x` explicitly?
 -- 2) Why do I have to specify the type of `(1 : I → β)`?
 -- 3) Removed `{β : Sort*}` as `[One β]` converts it to a type anyways.
@@ -400,7 +400,7 @@ theorem mulSingle_apply [One β] (i : I) (x : β) (i' : I) :
 #align pi.mul_single_apply Pi.mulSingle_apply
 #align pi.single_apply Pi.single_apply
 
--- Porting notes : Same as above.
+-- Porting note: Same as above.
 /-- On non-dependent functions, `Pi.mulSingle` is symmetric in the two indices. -/
 @[to_additive "On non-dependent functions, `Pi.single` is symmetric in the two indices."]
 theorem mulSingle_comm [One β] (i : I) (x : β) (i' : I) :

Mathlib/Algebra/Group/ULift.lean

@@ -104,7 +104,7 @@ def _root_.MulEquiv.ulift [Mul α] : ULift α ≃* α :=
   { Equiv.ulift with map_mul' := fun _ _ => rfl }
 #align mul_equiv.ulift MulEquiv.ulift
 
--- porting notes: below failed due to error above, manually added
+-- Porting note: below failed due to error above, manually added
 --@[to_additive]
 instance semigroup [Semigroup α] : Semigroup (ULift α) :=
   (MulEquiv.ulift.injective.semigroup _) fun _ _ => rfl

Mathlib/Algebra/PUnitInstances.lean

@@ -97,12 +97,12 @@ instance normalizedGCDMonoid : NormalizedGCDMonoid PUnit where
   normalize_gcd := by intros; rfl
   normalize_lcm := by intros; rfl
 
---porting notes: simpNF lint: simp can prove this @[simp]
+--Porting note: simpNF lint: simp can prove this @[simp]
 theorem gcd_eq : gcd x y = unit :=
   rfl
 #align punit.gcd_eq PUnit.gcd_eq
 
---porting notes: simpNF lint: simp can prove this @[simp]
+--Porting note: simpNF lint: simp can prove this @[simp]
 theorem lcm_eq : lcm x y = unit :=
   rfl
 #align punit.lcm_eq PUnit.lcm_eq

Mathlib/Algebra/Ring/Pi.lean

@@ -14,7 +14,7 @@ import Mathlib.Algebra.Ring.Hom.Defs
 This file defines instances for ring, semiring and related structures on Pi Types
 -/
 
--- Porting notes: used to import `tactic.pi_instances`
+-- Porting note: used to import `tactic.pi_instances`
 
 namespace Pi
 

Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -435,7 +435,7 @@ theorem adjunction_unit_app_app_top (X : Scheme) :
     SpecΓIdentity.hom.app (X.presheaf.obj (op ⊤)) := by
   have := congr_app ΓSpec.adjunction.left_triangle X
   dsimp at this
-  -- Porting Notes: Slightly changed some rewrites.
+  -- Porting note: Slightly changed some rewrites.
   -- Originally:
   --  rw [← is_iso.eq_comp_inv] at this
   --  simp only [Γ_Spec.LocallyRingedSpace_adjunction_counit, nat_trans.op_app, category.id_comp,

Mathlib/CategoryTheory/Sums/Associator.lean

@@ -133,10 +133,10 @@ theorem inverseAssociator_map_inr_inr {X Y : E} (f : inr (inr X) ⟶ inr (inr Y)
 def associativity : Sum (Sum C D) E ≌ Sum C (Sum D E) :=
   Equivalence.mk (associator C D E) (inverseAssociator C D E)
     (NatIso.ofComponents (fun X => eqToIso
-      (by rcases X with ((_|_)|_) <;> rfl)) -- Porting notes: aesop_cat fails
+      (by rcases X with ((_|_)|_) <;> rfl)) -- Porting note: aesop_cat fails
       (by rintro ((_|_)|_) ((_|_)|_) f <;> first | cases f | aesop_cat))
     (NatIso.ofComponents (fun X => eqToIso
-      (by rcases X with (_|(_|_)) <;> rfl)) -- Porting notes: aesop_cat fails
+      (by rcases X with (_|(_|_)) <;> rfl)) -- Porting note: aesop_cat fails
       (by rintro (_|(_|_)) (_|(_|_)) f <;> first | cases f | aesop_cat))
 #align category_theory.sum.associativity CategoryTheory.sum.associativity
 

Mathlib/Combinatorics/Partition.lean

@@ -59,7 +59,7 @@ structure Partition (n : ℕ) where
   parts_pos : ∀ {i}, i ∈ parts → 0 < i
   /-- proof that the `parts` sum to `n`-/
   parts_sum : parts.sum = n
-  -- porting notes: chokes on `parts_pos`
+  -- Porting note: chokes on `parts_pos`
   --deriving DecidableEq
 #align nat.partition Nat.Partition
 

Mathlib/Data/ENat/Lattice.lean

@@ -19,8 +19,8 @@ of `WithTop.some`.
 
 open Set
 
--- porting notes: was `deriving instance` but "default handlers have not been implemented yet"
--- porting notes: `noncomputable` through 'Nat.instConditionallyCompleteLinearOrderBotNat'
+-- Porting note: was `deriving instance` but "default handlers have not been implemented yet"
+-- Porting note: `noncomputable` through 'Nat.instConditionallyCompleteLinearOrderBotNat'
 noncomputable instance : CompleteLinearOrder ENat :=
   inferInstanceAs (CompleteLinearOrder (WithTop ℕ))
 

Mathlib/Data/Finsupp/Fin.lean

@@ -47,7 +47,7 @@ theorem cons_zero : cons y s 0 = y :=
 
 @[simp]
 theorem cons_succ : cons y s i.succ = s i :=
-  -- porting notes: was Fin.cons_succ _ _ _
+  -- Porting note: was Fin.cons_succ _ _ _
   rfl
 #align finsupp.cons_succ Finsupp.cons_succ
 

Mathlib/Data/Finsupp/Order.lean

@@ -19,7 +19,7 @@ This file lifts order structures on `α` to `ι →₀ α`.
   functions.
 -/
 
--- porting notes: removed from module documentation because it moved to `data.finsupp.multiset`
+-- Porting note: removed from module documentation because it moved to `data.finsupp.multiset`
 -- TODO: move to `Data.Finsupp.Multiset` when that is ported
 -- * `Finsupp.orderIsoMultiset`: The order isomorphism between `ℕ`-valued finitely supported
 --   functions and multisets.

Mathlib/Data/Finsupp/ToDFinsupp.lean

@@ -371,7 +371,7 @@ attribute [-instance] Finsupp.addMonoid
 @[simps]
 def sigmaFinsuppLequivDFinsupp [AddCommMonoid N] [Module R N] :
     ((Σi, η i) →₀ N) ≃ₗ[R] Π₀ i, η i →₀ N :=
-    -- porting notes: was
+    -- Porting note: was
     -- sigmaFinsuppAddEquivDFinsupp with map_smul' := sigmaFinsuppEquivDFinsupp_smul
     -- but times out
   { sigmaFinsuppEquivDFinsupp with

Mathlib/Data/Fintype/Perm.lean

@@ -75,7 +75,7 @@ theorem mem_permsOfList_of_mem {l : List α} {f : Perm α} (h : ∀ x, f x ≠ x
 #align mem_perms_of_list_of_mem mem_permsOfList_of_mem
 
 theorem mem_of_mem_permsOfList :
-    -- porting notes: was `∀ {x}` but need to capture the `x`
+    -- Porting note: was `∀ {x}` but need to capture the `x`
     ∀ {l : List α} {f : Perm α}, f ∈ permsOfList l → (x :α ) → f x ≠ x → x ∈ l
   | [], f, h, heq_iff_eq => by
     have : f = 1 := by simpa [permsOfList] using h

Mathlib/Data/FunLike/Fintype.lean

@@ -28,7 +28,7 @@ You can use these to produce instances for specific `DFunLike` types.
 They can't be instances themselves since they can cause loops.
 -/
 
--- porting notes: `Type` is a reserved word, switched to `Type'`
+-- Porting note: `Type` is a reserved word, switched to `Type'`
 section Type'
 
 variable (F G : Type*) {α γ : Type*} {β : α → Type*} [DFunLike F α β] [FunLike G α γ]
@@ -54,7 +54,7 @@ noncomputable def FunLike.fintype [DecidableEq α] [Fintype α] [Fintype γ] : F
 
 end Type'
 
--- porting notes: `Sort` is a reserved word, switched to `Sort'`
+-- Porting note: `Sort` is a reserved word, switched to `Sort'`
 section Sort'
 
 variable (F G : Sort*) {α γ : Sort*} {β : α → Sort*} [DFunLike F α β] [FunLike G α γ]

Mathlib/Data/List/Defs.lean

@@ -49,7 +49,7 @@ instance [DecidableEq α] : SDiff (List α) :=
 #noalign list.to_array
 
 #align list.nthd List.getD
--- porting notes: see
+-- Porting note: see
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/List.2Ehead/near/313204716
 -- for the fooI naming convention.
 /-- "Inhabited" `get` function: returns `default` instead of `none` in the case
@@ -151,7 +151,7 @@ end foldIdxM
 
 section mapIdxM
 
--- porting notes: This was defined in `mathlib` with an `Applicative`
+-- Porting note: This was defined in `mathlib` with an `Applicative`
 -- constraint on `m` and have been `#align`ed to the `Std` versions defined
 -- with a `Monad` typeclass constraint.
 -- Since all `Monad`s are `Applicative` this won't cause issues

Mathlib/Data/Nat/Pairing.lean

@@ -32,14 +32,14 @@ open Prod Decidable Function
 namespace Nat
 
 /-- Pairing function for the natural numbers. -/
--- porting notes: no pp_nodot
+-- Porting note: no pp_nodot
 --@[pp_nodot]
 def pair (a b : ℕ) : ℕ :=
   if a < b then b * b + a else a * a + a + b
 #align nat.mkpair Nat.pair
 
 /-- Unpairing function for the natural numbers. -/
--- porting notes: no pp_nodot
+-- Porting note: no pp_nodot
 --@[pp_nodot]
 def unpair (n : ℕ) : ℕ × ℕ :=
   let s := sqrt n

Mathlib/Data/Ordmap/Ordnode.lean

@@ -197,7 +197,7 @@ instance {α} [Repr α] : Repr (Ordnode α) :=
 O(1). Rebalance a tree which was previously balanced but has had its left
 side grow by 1, or its right side shrink by 1. -/
 def balanceL (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode α := by
-  -- porting notes: removed `clean`
+  -- Porting note: removed `clean`
   cases' id r with rs
   · cases' id l with ls ll lx lr
     · exact ι x
@@ -233,7 +233,7 @@ def balanceL (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode α := by
 O(1). Rebalance a tree which was previously balanced but has had its right
 side grow by 1, or its left side shrink by 1. -/
 def balanceR (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode α := by
-  -- porting notes: removed `clean`
+  -- Porting note: removed `clean`
   cases' id l with ls
   · cases' id r with rs rl rx rr
     · exact ι x
@@ -269,7 +269,7 @@ def balanceR (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode α := by
 O(1). Rebalance a tree which was previously balanced but has had one side change
 by at most 1. -/
 def balance (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode α := by
-  -- porting notes: removed `clean`
+  -- Porting note: removed `clean`
   cases' id l with ls ll lx lr
   · cases' id r with rs rl rx rr
     · exact ι x

Mathlib/Data/PNat/Find.lean

@@ -101,7 +101,7 @@ theorem lt_find_iff (n : ℕ+) : n < PNat.find h ↔ ∀ m ≤ n, ¬p m := by
 theorem find_eq_one : PNat.find h = 1 ↔ p 1 := by simp [find_eq_iff]
 #align pnat.find_eq_one PNat.find_eq_one
 
--- porting notes: deleted `@[simp]` to satisfy the linter because `le_find_iff` is more general
+-- Porting note: deleted `@[simp]` to satisfy the linter because `le_find_iff` is more general
 theorem one_le_find : 1 < PNat.find h ↔ ¬p 1 :=
   not_iff_not.mp <| by simp
 #align pnat.one_le_find PNat.one_le_find

Mathlib/Data/Quot.lean

@@ -367,7 +367,7 @@ noncomputable def Quot.out {r : α → α → Prop} (q : Quot r) : α :=
 /-- Unwrap the VM representation of a quotient to obtain an element of the equivalence class.
   Computable but unsound. -/
 unsafe def Quot.unquot {r : α → α → Prop} : Quot r → α :=
-  cast lcProof -- porting notes: was `unchecked_cast` before, which unfolds to `cast undefined`
+  cast lcProof -- Porting note: was `unchecked_cast` before, which unfolds to `cast undefined`
 
 @[simp]
 theorem Quot.out_eq {r : α → α → Prop} (q : Quot r) : Quot.mk r q.out = q :=

Mathlib/Data/Semiquot.lean

@@ -24,7 +24,7 @@ predicate `S`) but are not completely determined.
   of the set `s`. The specific element of `s` that the VM computes
   is hidden by a quotient construction, allowing for the representation
   of nondeterministic functions. -/
-  -- porting notes: removed universe parameter
+  -- Porting note: removed universe parameter
 structure Semiquot (α : Type*) where mk' ::
   /-- Set containing some element of `α`-/
   s : Set α

Mathlib/Data/Seq/Computation.lean

@@ -42,7 +42,7 @@ variable {α : Type u} {β : Type v} {γ : Type w}
 
 -- constructors
 /-- `pure a` is the computation that immediately terminates with result `a`. -/
--- porting notes: `return` is reserved, so changed to `pure`
+-- Porting note: `return` is reserved, so changed to `pure`
 def pure (a : α) : Computation α :=
   ⟨Stream'.const (some a), fun _ _ => id⟩
 #align computation.return Computation.pure
@@ -750,7 +750,7 @@ theorem bind_pure (f : α → β) (s) : bind s (pure ∘ f) = map f s := by
   · exact Or.inr ⟨s, rfl, rfl⟩
 #align computation.bind_ret Computation.bind_pure
 
--- porting notes: used to use `rw [bind_pure]`
+-- Porting note: used to use `rw [bind_pure]`
 @[simp]
 theorem bind_pure' (s : Computation α) : bind s pure = s := by
   apply eq_of_bisim fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure) ∧ c₂ = s
@@ -1175,7 +1175,7 @@ theorem liftRel_pure_right (R : α → β → Prop) (ca : Computation α) (b : 
     LiftRel R ca (pure b) ↔ ∃ a, a ∈ ca ∧ R a b := by rw [LiftRel.swap, liftRel_pure_left]
 #align computation.lift_rel_return_right Computation.liftRel_pure_right
 
--- porting notes: `simpNF` wants to simplify based on `liftRel_pure_right` but point is to prove
+-- Porting note: `simpNF` wants to simplify based on `liftRel_pure_right` but point is to prove
 -- a general invariant on `LiftRel`
 @[simp, nolint simpNF]
 theorem liftRel_pure (R : α → β → Prop) (a : α) (b : β) :
@@ -1222,7 +1222,7 @@ theorem liftRel_map {δ} (R : α → β → Prop) (S : γ → δ → Prop) {s1 :
   intros a b h; exact ⟨f1 a, ⟨ret_mem _, @h2 a b h⟩⟩
 #align computation.lift_rel_map Computation.liftRel_map
 
--- porting notes: deleted initial arguments `(_R : α → α → Prop) (_S : β → β → Prop)`: unused
+-- Porting note: deleted initial arguments `(_R : α → α → Prop) (_S : β → β → Prop)`: unused
 theorem map_congr {s1 s2 : Computation α} {f : α → β}
     (h1 : s1 ~ s2) : map f s1 ~ map f s2 := by
   rw [← lift_eq_iff_equiv]

Mathlib/Data/Vector.lean

@@ -87,7 +87,7 @@ def toList (v : Vector α n) : List α :=
   v.1
 #align vector.to_list Vector.toList
 
--- porting notes: align to `List` API
+-- Porting note: align to `List` API
 /-- nth element of a vector, indexed by a `Fin` type. -/
 def get : ∀ _ : Vector α n, Fin n → α
   | ⟨l, h⟩, i => l.nthLe i.1 (by rw [h]; exact i.2)

Mathlib/Data/Vector/Basic.lean

@@ -88,7 +88,7 @@ theorem mk_toList : ∀ (v : Vector α n) (h), (⟨toList v, h⟩ : Vector α n)
 
 @[simp] theorem length_val (v : Vector α n) : v.val.length = n := v.2
 
--- porting notes: not used in mathlib and coercions done differently in Lean 4
+-- Porting note: not used in mathlib and coercions done differently in Lean 4
 -- @[simp]
 -- theorem length_coe (v : Vector α n) :
 --     ((coe : { l : List α // l.length = n } → List α) v).length = n :=
@@ -118,7 +118,7 @@ theorem get_eq_get (v : Vector α n) (i : Fin n) :
   rfl
 #align vector.nth_eq_nth_le Vector.get_eq_getₓ
 
--- porting notes: `nthLe` deprecated for `get`
+-- Porting note: `nthLe` deprecated for `get`
 @[deprecated get_eq_get]
 theorem nth_eq_nthLe :
     ∀ (v : Vector α n) (i), get v i = v.toList.nthLe i.1 (by rw [toList_length]; exact i.2)
@@ -455,7 +455,7 @@ This can be used as `induction v using Vector.inductionOn`. -/
 @[elab_as_elim]
 def inductionOn {C : ∀ {n : ℕ}, Vector α n → Sort*} {n : ℕ} (v : Vector α n)
     (h_nil : C nil) (h_cons : ∀ {n : ℕ} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w)) : C v := by
-  -- porting notes: removed `generalizing`: already generalized
+  -- Porting note: removed `generalizing`: already generalized
   induction' n with n ih
   · rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
     exact h_nil
@@ -476,7 +476,7 @@ def inductionOn₂ {C : ∀ {n}, Vector α n → Vector β n → Sort*}
     (v : Vector α n) (w : Vector β n)
     (nil : C nil nil) (cons : ∀ {n a b} {x : Vector α n} {y}, C x y → C (a ::ᵥ x) (b ::ᵥ y)) :
     C v w := by
-  -- porting notes: removed `generalizing`: already generalized
+  -- Porting note: removed `generalizing`: already generalized
   induction' n with n ih
   · rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
     rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
@@ -496,7 +496,7 @@ def inductionOn₃ {C : ∀ {n}, Vector α n → Vector β n → Vector γ n →
     (u : Vector α n) (v : Vector β n) (w : Vector γ n) (nil : C nil nil nil)
     (cons : ∀ {n a b c} {x : Vector α n} {y z}, C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)) :
     C u v w := by
-  -- porting notes: removed `generalizing`: already generalized
+  -- Porting note: removed `generalizing`: already generalized
   induction' n with n ih
   · rcases u with ⟨_ | ⟨-, -⟩, - | -⟩
     rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
@@ -606,7 +606,7 @@ theorem insertNth_comm (a b : α) (i j : Fin (n + 1)) (h : i ≤ j) :
 
 end InsertNth
 
--- porting notes: renamed to `set` from `updateNth` to align with `List`
+-- Porting note: renamed to `set` from `updateNth` to align with `List`
 section ModifyNth
 
 /-- `set v n a` replaces the `n`th element of `v` with `a` -/

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -58,7 +58,7 @@ variable {α : Type u}
 
 attribute [local simp] List.append_eq_has_append
 
--- porting notes: to_additive.map_namespace is not supported yet
+-- Porting note: to_additive.map_namespace is not supported yet
 -- worked around it by putting a few extra manual mappings (but not too many all in all)
 -- run_cmd to_additive.map_namespace `FreeGroup `FreeAddGroup
 

Mathlib/Init/Algebra/Classes.lean

@@ -20,7 +20,7 @@ provided by mathlib, as they are not discoverable by `simp` unlike the current l
 being little to index on. The Wiki page linked above describes an algebraic normalizer, but it was
 never implemented in Lean 3.
 
-## Porting notes:
+## Porting note:
 This file is ancient, and it would be good to replace it with a clean version
 that provides what mathlib4 actually needs.
 

Mathlib/Order/Antisymmetrization.lean

@@ -24,7 +24,7 @@ such that `a ≤ b` and `b ≤ a`.
   preorder, `Antisymmetrization α` is a partial order.
 -/
 
-/- Porting Notes: There are many changes from `toAntisymmetrization (· ≤ ·)` to
+/- Porting note: There are many changes from `toAntisymmetrization (· ≤ ·)` to
 `@toAntisymmetrization α (· ≤ ·) _` -/
 
 open Function OrderDual
@@ -222,7 +222,7 @@ theorem OrderHom.coe_antisymmetrization (f : α →o β) :
   rfl
 #align order_hom.coe_antisymmetrization OrderHom.coe_antisymmetrization
 
-/- Porting notes: Removed @[simp] attribute. With this `simp` lemma the LHS of
+/- Porting note: Removed @[simp] attribute. With this `simp` lemma the LHS of
 `OrderHom.antisymmetrization_apply_mk` is not in normal-form -/
 theorem OrderHom.antisymmetrization_apply (f : α →o β) (a : Antisymmetrization α (· ≤ ·)) :
     f.antisymmetrization a = Quotient.map' f (liftFun_antisymmRel f) a :=

Mathlib/Order/InitialSeg.lean

@@ -55,7 +55,7 @@ structure InitialSeg {α β : Type*} (r : α → α → Prop) (s : β → β →
   init' : ∀ a b, s b (toRelEmbedding a) → ∃ a', toRelEmbedding a' = b
 #align initial_seg InitialSeg
 
--- Porting notes: Deleted `scoped[InitialSeg]`
+-- Porting note: Deleted `scoped[InitialSeg]`
 /-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≼i s` is an order
 embedding whose range is an initial segment. That is, whenever `b < f a` in `β` then `b` is in the
 range of `f`. -/
@@ -243,7 +243,7 @@ structure PrincipalSeg {α β : Type*} (r : α → α → Prop) (s : β → β 
   down' : ∀ b, s b top ↔ ∃ a, toRelEmbedding a = b
 #align principal_seg PrincipalSeg
 
--- Porting notes: deleted `scoped[InitialSeg]`
+-- Porting note: deleted `scoped[InitialSeg]`
 /-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≺i s` is an order
 embedding whose range is an open interval `(-∞, top)` for some element `top` of `β`. Such order
 embeddings are called principal segments -/