leanprover-community · pitmonticone · Feb 18, 2024
diff --git a/Mathlib/Algebra/MonoidAlgebra/Basic.lean b/Mathlib/Algebra/MonoidAlgebra/Basic.lean
@@ -754,7 +754,7 @@ def singleOneRingHom [Semiring k] [MulOneClass G] : k →+* MonoidAlgebra k G :=
   { Finsupp.singleAddHom 1 with
     map_one' := rfl
     map_mul' := fun x y => by
-      -- Porting note: Was `rw`.
+      -- Porting note (#10691): Was `rw`.
       simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, singleAddHom_apply,
         single_mul_single, mul_one] }
 #align monoid_algebra.single_one_ring_hom MonoidAlgebra.singleOneRingHom
@@ -1857,7 +1857,7 @@ section Algebra
 def singleZeroRingHom [Semiring k] [AddMonoid G] : k →+* k[G] :=
   { Finsupp.singleAddHom 0 with
     map_one' := rfl
-    -- Porting note: Was `rw`.
+    -- Porting note (#10691): Was `rw`.
     map_mul' := fun x y => by simp only [singleAddHom, single_mul_single, zero_add] }
 #align add_monoid_algebra.single_zero_ring_hom AddMonoidAlgebra.singleZeroRingHom
 #align add_monoid_algebra.single_zero_ring_hom_apply AddMonoidAlgebra.singleZeroRingHom_apply

diff --git a/Mathlib/Algebra/Order/ToIntervalMod.lean b/Mathlib/Algebra/Order/ToIntervalMod.lean
@@ -889,7 +889,7 @@ private theorem toIxxMod_total' (a b c : α) :
     Thus if a ≠ b and b ≠ c then ({a-b} + {b-c}) + ({c-b} + {b-a}) = 2 * period, so one of
     `{a-b} + {b-c}` and `{c-b} + {b-a}` must be `≤ period` -/
   have := congr_arg₂ (· + ·) (toIcoMod_add_toIocMod_zero hp a b) (toIcoMod_add_toIocMod_zero hp c b)
-  simp only [add_add_add_comm] at this -- Porting note: was `rw`
+  simp only [add_add_add_comm] at this -- Porting note (#10691): Was `rw`
   rw [_root_.add_comm (toIocMod _ _ _), add_add_add_comm, ← two_nsmul] at this
   replace := min_le_of_add_le_two_nsmul this.le
   rw [min_le_iff] at this

diff --git a/Mathlib/AlgebraicGeometry/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/OpenImmersion.lean
@@ -559,11 +559,11 @@ theorem range_pullback_snd_of_left :
   rw [←
     show _ = (pullback.snd : pullback f g ⟶ _).1.base from
       PreservesPullback.iso_hom_snd Scheme.forgetToTop f g]
-  -- Porting note : was `rw`
+  -- Porting note (#10691): was `rw`
   erw [coe_comp]
   rw [Set.range_comp, Set.range_iff_surjective.mpr, ←
     @Set.preimage_univ _ _ (pullback.fst : pullback f.1.base g.1.base ⟶ _)]
-  -- Porting note : was `rw`
+  -- Porting note (#10691): was `rw`
   erw [TopCat.pullback_snd_image_fst_preimage]
   rw [Set.image_univ]
   rfl
@@ -577,11 +577,11 @@ theorem range_pullback_fst_of_right :
   rw [←
     show _ = (pullback.fst : pullback g f ⟶ _).1.base from
       PreservesPullback.iso_hom_fst Scheme.forgetToTop g f]
-  -- Porting note : was `rw`
+  -- Porting note (#10691): was `rw`
   erw [coe_comp]
   rw [Set.range_comp, Set.range_iff_surjective.mpr, ←
     @Set.preimage_univ _ _ (pullback.snd : pullback g.1.base f.1.base ⟶ _)]
-  -- Porting note : was `rw`
+  -- Porting note (#10691): was `rw`
   erw [TopCat.pullback_fst_image_snd_preimage]
   rw [Set.image_univ]
   rfl
@@ -705,7 +705,7 @@ theorem image_basicOpen {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {U
     f.opensFunctor.obj (X.basicOpen r) = Y.basicOpen (Scheme.Hom.invApp f U r) := by
   have e := Scheme.preimage_basicOpen f (Scheme.Hom.invApp f U r)
   rw [Scheme.Hom.invApp] at e
-  -- Porting note : was `rw`
+  -- Porting note (#10691): was `rw`
   erw [PresheafedSpace.IsOpenImmersion.invApp_app_apply] at e
   rw [Scheme.basicOpen_res, inf_eq_right.mpr _] at e
   rw [← e]

diff --git a/Mathlib/Data/Polynomial/Laurent.lean b/Mathlib/Data/Polynomial/Laurent.lean
@@ -356,7 +356,7 @@ theorem trunc_C_mul_T (n : ℤ) (r : R) : trunc (C r * T n) = ite (0 ≤ n) (mon
   have : Function.Injective Int.ofNat := fun x y h => Int.ofNat_inj.mp h
   apply (toFinsuppIso R).injective
   rw [← single_eq_C_mul_T, trunc, AddMonoidHom.coe_comp, Function.comp_apply]
-  -- Porting note: was `rw`
+  -- Porting note (#10691): was `rw`
   erw [comapDomain.addMonoidHom_apply this]
   rw [toFinsuppIso_apply]
   -- Porting note: rewrote proof below relative to mathlib3.

diff --git a/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean b/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
@@ -62,7 +62,7 @@ def domCoprod.summand (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→
       TensorProduct.smul_tmul']
     simp only [Sum.map_inr, Perm.sumCongrHom_apply, Perm.sumCongr_apply, Sum.map_inl,
       Function.comp_apply, Perm.coe_mul]
-    -- Porting note: Was `rw`.
+    -- Porting note (#10691): was `rw`.
     erw [← a.map_congr_perm fun i => v (σ₁ _), ← b.map_congr_perm fun i => v (σ₁ _)]
 #align alternating_map.dom_coprod.summand AlternatingMap.domCoprod.summand
 

diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
@@ -139,7 +139,7 @@ def toEven : CliffordAlgebra Q →ₐ[R] CliffordAlgebra.even (Q' Q) := by
 @[simp]
 theorem toEven_ι (m : M) : (toEven Q (ι Q m) : CliffordAlgebra (Q' Q)) = e0 Q * v Q m := by
   rw [toEven, CliffordAlgebra.lift_ι_apply]
-  -- porting note: was `rw`
+  -- Porting note (#10691): was `rw`
   erw [LinearMap.codRestrict_apply]
   rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.mulLeft_apply]
 #align clifford_algebra.to_even_ι CliffordAlgebra.toEven_ι

diff --git a/Mathlib/Probability/Kernel/MeasurableIntegral.lean b/Mathlib/Probability/Kernel/MeasurableIntegral.lean
@@ -175,7 +175,7 @@ theorem _root_.Measurable.lintegral_kernel_prod_right {f : α → β → ℝ≥0
         (fun a => ∫⁻ b, g₁ (a, b) ∂κ a) + fun a => ∫⁻ b, g₂ (a, b) ∂κ a := by
       ext1 a
       rw [Pi.add_apply]
-      -- Porting note: was `rw` (`Function.comp` reducibility)
+      -- Porting note (#10691): was `rw` (`Function.comp` reducibility)
       erw [lintegral_add_left (g₁.measurable.comp measurable_prod_mk_left)]
       simp_rw [Function.comp_apply]
     rw [h_add]

diff --git a/Mathlib/RingTheory/Localization/Ideal.lean b/Mathlib/RingTheory/Localization/Ideal.lean
@@ -201,7 +201,7 @@ theorem surjective_quotientMap_of_maximal_of_localization {I : Ideal S} [I.IsPri
               (Ideal.Quotient.eq_zero_iff_mem.2
                 (Ideal.mem_comap.2 (Ideal.Quotient.eq_zero_iff_mem.1 hn))))
           (_root_.trans hn ?_))
-    -- Porting note: was `rw`, but this took extremely long.
+    -- Porting note (#10691): was `rw`, but this took extremely long.
     refine Eq.trans ?_ (RingHom.map_mul (Ideal.Quotient.mk I) (algebraMap R S m) (mk' S 1 ⟨m, hm⟩))
     rw [← mk'_eq_mul_mk'_one, mk'_self, RingHom.map_one]
 #align is_localization.surjective_quotient_map_of_maximal_of_localization IsLocalization.surjective_quotientMap_of_maximal_of_localization