From 54b9575f87e5553376562f98fdb43da1d83c02a7 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 26 Feb 2024 01:47:59 +0000 Subject: [PATCH] style: fix typos in porting notes (#10931) --- Mathlib/Algebra/Group/Units.lean | 2 +- Mathlib/Algebra/Group/WithOne/Defs.lean | 2 +- Mathlib/CategoryTheory/Sites/Subsheaf.lean | 4 ++-- Mathlib/Data/List/Sublists.lean | 2 +- Mathlib/Data/Matrix/DMatrix.lean | 4 ++-- Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean | 2 +- Mathlib/Logic/Embedding/Basic.lean | 6 +++--- Mathlib/SetTheory/Cardinal/Basic.lean | 2 +- Mathlib/Tactic/FieldSimp.lean | 2 +- 9 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Mathlib/Algebra/Group/Units.lean b/Mathlib/Algebra/Group/Units.lean index 17add48d736d36..fe30f3fc6d79fb 100644 --- a/Mathlib/Algebra/Group/Units.lean +++ b/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 := diff --git a/Mathlib/Algebra/Group/WithOne/Defs.lean b/Mathlib/Algebra/Group/WithOne/Defs.lean index b6f8a8e725f636..b94b4857a82583 100644 --- a/Mathlib/Algebra/Group/WithOne/Defs.lean +++ b/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] diff --git a/Mathlib/CategoryTheory/Sites/Subsheaf.lean b/Mathlib/CategoryTheory/Sites/Subsheaf.lean index c82a6bd4bcff0d..c3868c71afdf99 100644 --- a/Mathlib/CategoryTheory/Sites/Subsheaf.lean +++ b/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)⟩ diff --git a/Mathlib/Data/List/Sublists.lean b/Mathlib/Data/List/Sublists.lean index 59abb0ea8e642b..d3d2b0c7d596ff 100644 --- a/Mathlib/Data/List/Sublists.lean +++ b/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 diff --git a/Mathlib/Data/Matrix/DMatrix.lean b/Mathlib/Data/Matrix/DMatrix.lean index 0dd4619b087e7d..24f5072de910ce 100644 --- a/Mathlib/Data/Matrix/DMatrix.lean +++ b/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] diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean index 9f0cf4a87d1d83..9f61098ec637ae 100644 --- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean +++ b/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 diff --git a/Mathlib/Logic/Embedding/Basic.lean b/Mathlib/Logic/Embedding/Basic.lean index f17b72d1d2e749..0553cf48651d01 100644 --- a/Mathlib/Logic/Embedding/Basic.lean +++ b/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 diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index 2371df9661b680..2680803e5f84cb 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/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} #α := diff --git a/Mathlib/Tactic/FieldSimp.lean b/Mathlib/Tactic/FieldSimp.lean index 674e551623329b..0cb88ff60ad8d9 100644 --- a/Mathlib/Tactic/FieldSimp.lean +++ b/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?),