style: fix typos in porting notes (#10931)

Mathlib/Algebra/Group/Units.lean

@@ -528,7 +528,7 @@ theorem divp_divp_eq_divp_mul (x : α) (u₁ u₂ : αˣ) : x /ₚ u₁ /ₚ u
   simp only [divp, mul_inv_rev, Units.val_mul, mul_assoc]
 #align divp_divp_eq_divp_mul divp_divp_eq_divp_mul
 
-/- Port note: to match the mathlib3 behavior, this needs to have higher simp
+/- Porting note: to match the mathlib3 behavior, this needs to have higher simp
 priority than eq_divp_iff_mul_eq. -/
 @[field_simps 1010]
 theorem divp_eq_iff_mul_eq {x : α} {u : αˣ} {y : α} : x /ₚ u = y ↔ y * u = x :=

Mathlib/Algebra/Group/WithOne/Defs.lean

@@ -180,7 +180,7 @@ protected theorem cases_on {P : WithOne α → Prop} : ∀ x : WithOne α, P 1 
 #align with_one.cases_on WithOne.cases_on
 #align with_zero.cases_on WithZero.cases_on
 
--- port note: I don't know if `elab_as_elim` is being added to the additivised declaration.
+-- Porting note: I don't know if `elab_as_elim` is being added to the additivised declaration.
 attribute [elab_as_elim] WithZero.cases_on
 
 @[to_additive]

Mathlib/CategoryTheory/Sites/Subsheaf.lean

@@ -168,7 +168,7 @@ def Subpresheaf.familyOfElementsOfSection {U : Cᵒᵖ} (s : F.obj U) :
 theorem Subpresheaf.family_of_elements_compatible {U : Cᵒᵖ} (s : F.obj U) :
     (G.familyOfElementsOfSection s).Compatible := by
   intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ e
-  refine Subtype.ext ?_ -- port note: `ext1` does not work here
+  refine Subtype.ext ?_ -- Porting note: `ext1` does not work here
   change F.map g₁.op (F.map f₁.op s) = F.map g₂.op (F.map f₂.op s)
   rw [← FunctorToTypes.map_comp_apply, ← FunctorToTypes.map_comp_apply, ← op_comp, ← op_comp, e]
 #align category_theory.grothendieck_topology.subpresheaf.family_of_elements_compatible CategoryTheory.GrothendieckTopology.Subpresheaf.family_of_elements_compatible
@@ -459,7 +459,7 @@ noncomputable def imageFactorization {F F' : Sheaf J TypeMax.{v, u}} (f : F ⟶
   F := imageMonoFactorization f
   isImage :=
     { lift := fun I => by
-        -- port note: need to specify the target category (TypeMax.{v, u}) for this to work.
+        -- Porting note: need to specify the target category (TypeMax.{v, u}) for this to work.
         haveI M := (Sheaf.Hom.mono_iff_presheaf_mono J TypeMax.{v, u} _).mp I.m_mono
         haveI := isIso_toImagePresheaf I.m.1
         refine' ⟨Subpresheaf.homOfLe _ ≫ inv (toImagePresheaf I.m.1)⟩

Mathlib/Data/List/Sublists.lean

@@ -165,7 +165,7 @@ theorem sublists_append (l₁ l₂ : List α) :
     simp [List.bind, join_join, Function.comp]
 #align list.sublists_append List.sublists_append
 
---Portin note: New theorem
+--Porting note: New theorem
 theorem sublists_cons (a : α) (l : List α) :
     sublists (a :: l) = sublists l >>= (fun x => [x, a :: x]) :=
   show sublists ([a] ++ l) = _ by

Mathlib/Data/Matrix/DMatrix.lean

@@ -78,7 +78,7 @@ def row {α : n → Type v} (v : ∀ j, α j) : DMatrix Unit n fun _i j => α j
   | _x, y => v y
 #align dmatrix.row DMatrix.row
 
--- port note: Old proof is Pi.inhabited.
+-- Porting note: Old proof is Pi.inhabited.
 instance [inst : ∀ i j, Inhabited (α i j)] : Inhabited (DMatrix m n α) :=
   ⟨fun i j => (inst i j).default⟩
 
@@ -115,7 +115,7 @@ instance [∀ i j, AddCommGroup (α i j)] : AddCommGroup (DMatrix m n α) :=
 instance [∀ i j, Unique (α i j)] : Unique (DMatrix m n α) :=
   Pi.unique
 
--- Port note: old proof is Pi.Subsingleton
+-- Porting note: old proof is Pi.Subsingleton
 instance [∀ i j, Subsingleton (α i j)] : Subsingleton (DMatrix m n α) :=
   by constructor; simp only [DMatrix, eq_iff_true_of_subsingleton, implies_true]
 

Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

@@ -323,7 +323,7 @@ theorem opensImagePreimageMap_app_assoc (i j k : D.J) (U : Opens (D.U i).carrier
 /-- (Implementation) Given an open subset of one of the spaces `U ⊆ Uᵢ`, the sheaf component of
 the image `ι '' U` in the glued space is the limit of this diagram. -/
 abbrev diagramOverOpen {i : D.J} (U : Opens (D.U i).carrier) :
-    -- Portinge note : ↓ these need to be explicit
+    -- Porting note : ↓ these need to be explicit
     (WalkingMultispan D.diagram.fstFrom D.diagram.sndFrom)ᵒᵖ ⥤ C :=
   componentwiseDiagram 𝖣.diagram.multispan ((D.ι_openEmbedding i).isOpenMap.functor.obj U)
 #align algebraic_geometry.PresheafedSpace.glue_data.diagram_over_open AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpen

Mathlib/Logic/Embedding/Basic.lean

@@ -20,7 +20,7 @@ universe u v w x
 
 namespace Function
 
--- port note: in Lean 3 this was tagged @[nolint has_nonempty_instance]
+-- Porting note: in Lean 3 this was tagged @[nolint has_nonempty_instance]
 /-- `α ↪ β` is a bundled injective function. -/
 structure Embedding (α : Sort*) (β : Sort*) where
   /-- An embedding as a function. Use coercion instead. -/
@@ -96,7 +96,7 @@ instance Equiv.Perm.coeEmbedding : Coe (Equiv.Perm α) (α ↪ α) :=
   Equiv.coeEmbedding
 #align equiv.perm.coe_embedding Equiv.Perm.coeEmbedding
 
--- port note : `theorem Equiv.coe_eq_to_embedding : ↑f = f.toEmbedding` is a
+-- Porting note : `theorem Equiv.coe_eq_to_embedding : ↑f = f.toEmbedding` is a
 -- syntactic tautology in Lean 4
 
 end Equiv
@@ -114,7 +114,7 @@ theorem ext {α β} {f g : Embedding α β} (h : ∀ x, f x = g x) : f = g :=
   DFunLike.ext f g h
 #align function.embedding.ext Function.Embedding.ext
 
--- port note : in Lean 3 `DFunLike.ext_iff.symm` works
+-- Porting note : in Lean 3 `DFunLike.ext_iff.symm` works
 theorem ext_iff {α β} {f g : Embedding α β} : (∀ x, f x = g x) ↔ f = g :=
   Iff.symm (DFunLike.ext_iff)
 #align function.embedding.ext_iff Function.Embedding.ext_iff

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -1034,7 +1034,7 @@ lemma exists_eq_of_iSup_eq_of_not_isLimit
   rw [← le_zero_iff] at h ⊢
   exact (le_ciSup hf _).trans h
 
--- Portin note: simpNF is not happy with universe levels.
+-- Porting note: simpNF is not happy with universe levels.
 @[simp, nolint simpNF]
 theorem lift_mk_shrink (α : Type u) [Small.{v} α] :
     Cardinal.lift.{max u w} #(Shrink.{v} α) = Cardinal.lift.{max v w} #α :=

Mathlib/Tactic/FieldSimp.lean

@@ -64,7 +64,7 @@ partial def discharge (prop : Expr) : SimpM (Option Expr) :=
     let ctx ← readThe Simp.Context
     let usedTheorems := (← get).usedTheorems
 
-    -- Port note: mathlib3's analogous field_simp discharger `field_simp.ne_zero`
+    -- Porting note: mathlib3's analogous field_simp discharger `field_simp.ne_zero`
     -- does not explicitly call `simp` recursively like this. It's unclear to me
     -- whether this is because
     --   1) Lean 3 simp dischargers automatically call `simp` recursively. (Do they?),