[Merged by Bors] - chore: classify was simp porting notes

Mathlib/Algebra/Lie/Engel.lean

@@ -181,7 +181,7 @@ theorem Function.Surjective.isEngelian {f : L →ₗ⁅R⁆ L₂} (hf : Function
   have surj_id : Function.Surjective (LinearMap.id : M →ₗ[R] M) := Function.surjective_id
   haveI : LieModule.IsNilpotent R L M := h M hnp
   apply hf.lieModuleIsNilpotent surj_id
-  -- Porting note: was `simp`
+  -- porting note (#10745): was `simp`
   intros; simp only [LinearMap.id_coe, id_eq]; rfl
 #align function.surjective.is_engelian Function.Surjective.isEngelian
 

Mathlib/Algebra/MonoidAlgebra/Basic.lean

@@ -519,7 +519,7 @@ def of [MulOneClass G] : G →* MonoidAlgebra k G :=
 end
 
 theorem smul_of [MulOneClass G] (g : G) (r : k) : r • of k G g = single g r := by
-  -- Porting note: Was `simp`.
+  -- porting note (#10745): was `simp`.
   rw [of_apply, smul_single', mul_one]
 #align monoid_algebra.smul_of MonoidAlgebra.smul_of
 

Mathlib/Analysis/Calculus/Implicit.lean

@@ -207,7 +207,7 @@ theorem implicitFunction_hasStrictFDerivAt (g'inv : G →L[𝕜] E)
   convert this.comp (φ.rightFun φ.pt) ((hasStrictFDerivAt_const _ _).prod (hasStrictFDerivAt_id _))
   -- porting note: added parentheses to help `simp`
   simp only [ContinuousLinearMap.ext_iff, (ContinuousLinearMap.comp_apply)] at hg'inv hg'invf ⊢
-  -- porting note: was `simp [ContinuousLinearEquiv.eq_symm_apply]`;
+  -- porting note (#10745): was `simp [ContinuousLinearEquiv.eq_symm_apply]`;
   -- both `simp` and `rw` fail here, `erw` works
   intro x
   erw [ContinuousLinearEquiv.eq_symm_apply]

Mathlib/Analysis/Complex/Conformal.lean

@@ -58,7 +58,7 @@ theorem isConformalMap_complex_linear {map : ℂ →L[ℂ] E} (nonzero : map ≠
     simp only [map.coe_coe, map.map_smul, norm_smul, norm_inv, norm_norm]
     field_simp only [one_mul]
   · ext1
-    -- Porting note: was simp
+    -- porting note (#10745): was simp
     rw [coe_restrictScalars', coe_smul', LinearIsometry.coe_toContinuousLinearMap,
       LinearIsometry.coe_mk, Pi.smul_apply, LinearMap.smul_apply, LinearMap.coe_restrictScalars,
       coe_coe, smul_inv_smul₀ minor₁]
@@ -87,13 +87,13 @@ theorem IsConformalMap.is_complex_or_conj_linear (h : IsConformalMap g) :
   -- let rot := c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ,
   · refine' Or.inl ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, _⟩
     ext1
-    -- Porting note: was simp
+    -- porting note (#10745): was simp
     rw [coe_restrictScalars', smul_apply, smul_apply, smul_apply,
       LinearIsometry.coe_toContinuousLinearMap,
       LinearIsometryEquiv.coe_toLinearIsometry, rotation_apply, id_apply, smul_eq_mul]
   · refine' Or.inr ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, _⟩
     ext1
-    -- Porting note: was simp
+    -- porting note (#10745): was simp
     rw [coe_restrictScalars', smul_apply, smul_apply, comp_apply, smul_apply,
       LinearIsometry.coe_toContinuousLinearMap, LinearIsometryEquiv.coe_toLinearIsometry,
       LinearIsometryEquiv.trans_apply, rotation_apply, id_apply, smul_eq_mul,

Mathlib/Analysis/Normed/Group/AddTorsor.lean

@@ -46,7 +46,7 @@ variable {α V P W Q : Type*} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [
 
 instance (priority := 100) NormedAddTorsor.to_isometricVAdd : IsometricVAdd V P :=
   ⟨fun c => Isometry.of_dist_eq fun x y => by
-    -- Porting note: was `simp [NormedAddTorsor.dist_eq_norm']`
+    -- porting note (#10745): was `simp [NormedAddTorsor.dist_eq_norm']`
     rw [NormedAddTorsor.dist_eq_norm', NormedAddTorsor.dist_eq_norm', vadd_vsub_vadd_cancel_left]⟩
 #align normed_add_torsor.to_has_isometric_vadd NormedAddTorsor.to_isometricVAdd
 
@@ -112,7 +112,7 @@ theorem nndist_vadd_cancel_right (v₁ v₂ : V) (x : P) : nndist (v₁ +ᵥ x)
 
 @[simp]
 theorem dist_vadd_left (v : V) (x : P) : dist (v +ᵥ x) x = ‖v‖ := by
-  -- Porting note: was `simp [dist_eq_norm_vsub V _ x]`
+  -- porting note (#10745): was `simp [dist_eq_norm_vsub V _ x]`
   rw [dist_eq_norm_vsub V _ x, vadd_vsub]
 #align dist_vadd_left dist_vadd_left
 

Mathlib/Analysis/NormedSpace/AddTorsor.lean

@@ -44,7 +44,7 @@ theorem AffineSubspace.isClosed_direction_iff (s : AffineSubspace 𝕜 Q) :
 @[simp]
 theorem dist_center_homothety (p₁ p₂ : P) (c : 𝕜) :
     dist p₁ (homothety p₁ c p₂) = ‖c‖ * dist p₁ p₂ := by
-  -- Porting note: was `simp [homothety_def, norm_smul, ← dist_eq_norm_vsub, dist_comm]`
+  -- porting note (#10745): was `simp [homothety_def, norm_smul, ← dist_eq_norm_vsub, dist_comm]`
   rw [homothety_def, dist_eq_norm_vsub V]
   simp [norm_smul, ← dist_eq_norm_vsub V, dist_comm]
 #align dist_center_homothety dist_center_homothety

Mathlib/Analysis/NormedSpace/lpSpace.lean

@@ -502,7 +502,7 @@ instance normedAddCommGroup [hp : Fact (1 ≤ p)] : NormedAddCommGroup (lp E p)
       add_le' := fun f g => by
         rcases p.dichotomy with (rfl | hp')
         · cases isEmpty_or_nonempty α
-          · -- Porting note: was `simp [lp.eq_zero' f]`
+          · -- porting note (#10745): was `simp [lp.eq_zero' f]`
             rw [lp.eq_zero' f]
             simp only [zero_add, norm_zero, le_refl] -- porting note: just `simp` was slow
           refine' (lp.isLUB_norm (f + g)).2 _

Mathlib/Analysis/PSeries.lean

@@ -217,7 +217,7 @@ theorem Real.summable_nat_pow_inv {p : ℕ} :
 if and only if `1 < p`. -/
 theorem Real.summable_one_div_nat_pow {p : ℕ} :
     Summable (fun n => 1 / (n : ℝ) ^ p : ℕ → ℝ) ↔ 1 < p := by
-  -- Porting note: was `simp`
+  -- porting note (#10745): was `simp`
   simp only [one_div, Real.summable_nat_pow_inv]
 #align real.summable_one_div_nat_pow Real.summable_one_div_nat_pow
 

Mathlib/Combinatorics/Quiver/Covering.lean

@@ -161,7 +161,7 @@ theorem Prefunctor.symmetrifyStar (u : U) :
   -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
   erw [Equiv.eq_symm_comp]
   ext ⟨v, f | g⟩ <;>
-    -- Porting note: was `simp [Quiver.symmetrifyStar]`
+    -- porting note (#10745): was `simp [Quiver.symmetrifyStar]`
     simp only [Quiver.symmetrifyStar, Function.comp_apply] <;>
     erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply] <;>
     simp
@@ -174,7 +174,7 @@ protected theorem Prefunctor.symmetrifyCostar (u : U) :
   -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
   erw [Equiv.eq_symm_comp]
   ext ⟨v, f | g⟩ <;>
-    -- Porting note: was `simp [Quiver.symmetrifyCostar]`
+    -- porting note (#10745): was `simp [Quiver.symmetrifyCostar]`
     simp only [Quiver.symmetrifyCostar, Function.comp_apply] <;>
     erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply] <;>
     simp

Mathlib/Data/Fin/Tuple/Sort.lean

@@ -52,7 +52,7 @@ theorem graph.card (f : Fin n → α) : (graph f).card = n := by
   rw [graph, Finset.card_image_of_injective]
   · exact Finset.card_fin _
   · intro _ _
-    -- Porting note: was `simp`
+    -- porting note (#10745): was `simp`
     dsimp only
     rw [Prod.ext_iff]
     simp

Mathlib/Data/Finsupp/AList.lean

@@ -117,7 +117,7 @@ theorem insert_lookupFinsupp [DecidableEq α] (l : AList fun _x : α => M) (a :
 theorem singleton_lookupFinsupp (a : α) (m : M) :
     (singleton a m).lookupFinsupp = Finsupp.single a m := by
   classical
-  -- porting note: was `simp [← AList.insert_empty]` but timeout issues
+  -- porting note (#10745): was `simp [← AList.insert_empty]` but timeout issues
   simp only [← AList.insert_empty, insert_lookupFinsupp, empty_lookupFinsupp, Finsupp.zero_update]
 #align alist.singleton_lookup_finsupp AList.singleton_lookupFinsupp
 

Mathlib/Data/IsROrC/Basic.lean

@@ -181,7 +181,7 @@ theorem ofReal_inj {z w : ℝ} : (z : K) = (w : K) ↔ z = w :=
 #align is_R_or_C.of_real_inj IsROrC.ofReal_inj
 
 set_option linter.deprecated false in
-@[deprecated, isROrC_simps] -- porting note: was `simp` but `simp` can prove it
+@[deprecated, isROrC_simps] -- porting note (#10618): was `simp` but `simp` can prove it
 theorem bit0_re (z : K) : re (bit0 z) = bit0 (re z) :=
   map_bit0 _ _
 #align is_R_or_C.bit0_re IsROrC.bit0_re
@@ -192,7 +192,7 @@ theorem bit1_re (z : K) : re (bit1 z) = bit1 (re z) := by simp only [bit1, map_a
 #align is_R_or_C.bit1_re IsROrC.bit1_re
 
 set_option linter.deprecated false in
-@[deprecated, isROrC_simps] -- porting note: was `simp` but `simp` can prove it
+@[deprecated, isROrC_simps] -- porting note (#10618): was `simp` but `simp` can prove it
 theorem bit0_im (z : K) : im (bit0 z) = bit0 (im z) :=
   map_bit0 _ _
 #align is_R_or_C.bit0_im IsROrC.bit0_im
@@ -331,7 +331,7 @@ theorem I_im' (z : K) : im (I : K) * im z = im z := by rw [mul_comm, I_im]
 set_option linter.uppercaseLean3 false in
 #align is_R_or_C.I_im' IsROrC.I_im'
 
-@[isROrC_simps] -- porting note: was `simp`
+@[isROrC_simps] -- porting note (#10618): was `simp`
 theorem I_mul_re (z : K) : re (I * z) = -im z := by
   simp only [I_re, zero_sub, I_im', zero_mul, mul_re]
 set_option linter.uppercaseLean3 false in
@@ -369,13 +369,13 @@ theorem conj_ofReal (r : ℝ) : conj (r : K) = (r : K) := by
 #align is_R_or_C.conj_of_real IsROrC.conj_ofReal
 
 set_option linter.deprecated false in
-@[deprecated, isROrC_simps] -- porting note: was `simp` but `simp` can prove it
+@[deprecated, isROrC_simps] -- porting note (#10618): was `simp` but `simp` can prove it
 theorem conj_bit0 (z : K) : conj (bit0 z) = bit0 (conj z) :=
   map_bit0 _ _
 #align is_R_or_C.conj_bit0 IsROrC.conj_bit0
 
 set_option linter.deprecated false in
-@[deprecated, isROrC_simps] -- porting note: was `simp` but `simp` can prove it
+@[deprecated, isROrC_simps] -- porting note (#10618): was `simp` but `simp` can prove it
 theorem conj_bit1 (z : K) : conj (bit1 z) = bit1 (conj z) :=
   map_bit1 _ _
 #align is_R_or_C.conj_bit1 IsROrC.conj_bit1
@@ -495,7 +495,7 @@ theorem normSq_nonneg (z : K) : 0 ≤ normSq z :=
   add_nonneg (mul_self_nonneg _) (mul_self_nonneg _)
 #align is_R_or_C.norm_sq_nonneg IsROrC.normSq_nonneg
 
-@[isROrC_simps] -- porting note: was `simp`
+@[isROrC_simps] -- porting note (#10618): was `simp`
 theorem normSq_eq_zero {z : K} : normSq z = 0 ↔ z = 0 :=
   map_eq_zero _
 #align is_R_or_C.norm_sq_eq_zero IsROrC.normSq_eq_zero
@@ -514,7 +514,7 @@ theorem normSq_conj (z : K) : normSq (conj z) = normSq z := by
   simp only [normSq_apply, neg_mul, mul_neg, neg_neg, isROrC_simps]
 #align is_R_or_C.norm_sq_conj IsROrC.normSq_conj
 
-@[isROrC_simps] -- porting note: was `simp`
+@[isROrC_simps] -- porting note (#10618): was `simp`
 theorem normSq_mul (z w : K) : normSq (z * w) = normSq z * normSq w :=
   map_mul _ z w
 #align is_R_or_C.norm_sq_mul IsROrC.normSq_mul
@@ -586,7 +586,7 @@ theorem div_im (z w : K) : im (z / w) = im z * re w / normSq w - re z * im w / n
     isROrC_simps]
 #align is_R_or_C.div_im IsROrC.div_im
 
-@[isROrC_simps] -- porting note: was `simp`
+@[isROrC_simps] -- porting note (#10618): was `simp`
 theorem conj_inv (x : K) : conj x⁻¹ = (conj x)⁻¹ :=
   star_inv' _
 #align is_R_or_C.conj_inv IsROrC.conj_inv
@@ -636,17 +636,17 @@ theorem div_I (z : K) : z / I = -(z * I) := by rw [div_eq_mul_inv, inv_I, mul_ne
 set_option linter.uppercaseLean3 false in
 #align is_R_or_C.div_I IsROrC.div_I
 
-@[isROrC_simps] -- porting note: was `simp`
+@[isROrC_simps] -- porting note (#10618): was `simp`
 theorem normSq_inv (z : K) : normSq z⁻¹ = (normSq z)⁻¹ :=
   map_inv₀ normSq z
 #align is_R_or_C.norm_sq_inv IsROrC.normSq_inv
 
-@[isROrC_simps] -- porting note: was `simp`
+@[isROrC_simps] -- porting note (#10618): was `simp`
 theorem normSq_div (z w : K) : normSq (z / w) = normSq z / normSq w :=
   map_div₀ normSq z w
 #align is_R_or_C.norm_sq_div IsROrC.normSq_div
 
-@[isROrC_simps] -- porting note: was `simp`
+@[isROrC_simps] -- porting note (#10618): was `simp`
 theorem norm_conj {z : K} : ‖conj z‖ = ‖z‖ := by simp only [← sqrt_normSq_eq_norm, normSq_conj]
 #align is_R_or_C.norm_conj IsROrC.norm_conj
 

Mathlib/Data/Matrix/Basis.lean

@@ -204,7 +204,7 @@ theorem mul_of_ne {k l : n} (h : j ≠ k) (d : α) :
   ext a b
   simp only [mul_apply, boole_mul, stdBasisMatrix]
   by_cases h₁ : i = a
-  -- Porting note: was `simp [h₁, h, h.symm]`
+  -- porting note (#10745): was `simp [h₁, h, h.symm]`
   · simp only [h₁, true_and, mul_ite, ite_mul, zero_mul, mul_zero, ← ite_and, zero_apply]
     refine Finset.sum_eq_zero (fun x _ => ?_)
     apply if_neg

Mathlib/Data/Nat/Bitwise.lean

@@ -362,7 +362,7 @@ macro "bitwise_assoc_tac" : tactic => set_option hygiene false in `(tactic| (
   induction' m using Nat.binaryRec with b' m hm
   · simp
   induction' k using Nat.binaryRec with b'' k hk
-  -- Porting note: was `simp [hn]`
+  -- porting note (#10745): was `simp [hn]`
   -- This is necessary because these are simp lemmas in mathlib
   <;> simp [hn, Bool.or_assoc, Bool.and_assoc, Bool.bne_eq_xor]))
 

Mathlib/Data/Polynomial/Basic.lean

@@ -429,9 +429,9 @@ theorem card_support_eq_zero : p.support.card = 0 ↔ p = 0 := by simp
 /-- `monomial s a` is the monomial `a * X^s` -/
 def monomial (n : ℕ) : R →ₗ[R] R[X] where
   toFun t := ⟨Finsupp.single n t⟩
-  -- Porting note: Was `simp`.
+  -- porting note (#10745): was `simp`.
   map_add' x y := by simp; rw [ofFinsupp_add]
-  -- Porting note: Was `simp [← ofFinsupp_smul]`.
+  -- porting note (#10745): was `simp [← ofFinsupp_smul]`.
   map_smul' r x := by simp; rw [← ofFinsupp_smul, smul_single']
 #align polynomial.monomial Polynomial.monomial
 
@@ -686,7 +686,7 @@ theorem toFinsupp_apply (f : R[X]) (i) : f.toFinsupp i = f.coeff i := by cases f
 #align polynomial.to_finsupp_apply Polynomial.toFinsupp_apply
 
 theorem coeff_monomial : coeff (monomial n a) m = if n = m then a else 0 := by
-  -- Porting note: Was `simp [← ofFinsupp_single, coeff, LinearMap.coe_mk]`.
+  -- porting note (#10745): was `simp [← ofFinsupp_single, coeff, LinearMap.coe_mk]`.
   rw [← ofFinsupp_single]
   simp only [coeff, LinearMap.coe_mk]
   rw [Finsupp.single_apply]
@@ -826,7 +826,7 @@ theorem forall_eq_iff_forall_eq : (∀ f g : R[X], f = g) ↔ ∀ a b : R, a = b
 theorem ext_iff {p q : R[X]} : p = q ↔ ∀ n, coeff p n = coeff q n := by
   rcases p with ⟨f : ℕ →₀ R⟩
   rcases q with ⟨g : ℕ →₀ R⟩
-  -- Porting note: Was `simp [coeff, DFunLike.ext_iff]`
+  -- porting note (#10745): was `simp [coeff, DFunLike.ext_iff]`
   simpa [coeff] using DFunLike.ext_iff (f := f) (g := g)
 #align polynomial.ext_iff Polynomial.ext_iff
 
@@ -954,7 +954,7 @@ theorem support_X (H : ¬(1 : R) = 0) : (X : R[X]).support = singleton 1 := by
 
 theorem monomial_left_inj {a : R} (ha : a ≠ 0) {i j : ℕ} :
     monomial i a = monomial j a ↔ i = j := by
-  -- Porting note: Was `simp [← ofFinsupp_single, Finsupp.single_left_inj ha]`
+  -- porting note (#10745): was `simp [← ofFinsupp_single, Finsupp.single_left_inj ha]`
   rw [← ofFinsupp_single, ← ofFinsupp_single, ofFinsupp.injEq, Finsupp.single_left_inj ha]
 #align polynomial.monomial_left_inj Polynomial.monomial_left_inj
 

Mathlib/Data/Polynomial/Coeff.lean

@@ -114,7 +114,7 @@ theorem finset_sum_coeff {ι : Type*} (s : Finset ι) (f : ι → R[X]) (n : ℕ
 theorem coeff_sum [Semiring S] (n : ℕ) (f : ℕ → R → S[X]) :
     coeff (p.sum f) n = p.sum fun a b => coeff (f a b) n := by
   rcases p with ⟨⟩
-  -- Porting note: Was `simp [Polynomial.sum, support, coeff]`.
+  -- porting note (#10745): was `simp [Polynomial.sum, support, coeff]`.
   simp [Polynomial.sum, support_ofFinsupp, coeff_ofFinsupp]
 #align polynomial.coeff_sum Polynomial.coeff_sum
 

Mathlib/Data/Polynomial/Eval.lean

@@ -814,7 +814,7 @@ theorem coeff_map (n : ℕ) : coeff (p.map f) n = f (coeff p n) := by
   rw [map, eval₂_def, coeff_sum, sum]
   conv_rhs => rw [← sum_C_mul_X_pow_eq p, coeff_sum, sum, map_sum]
   refine' Finset.sum_congr rfl fun x _hx => _
-  -- Porting note: Was `simp [Function.comp, coeff_C_mul_X_pow, f.map_mul]`.
+  -- porting note (#10745): was `simp [Function.comp, coeff_C_mul_X_pow, f.map_mul]`.
   simp? [Function.comp, coeff_C_mul_X_pow, - map_mul, - coeff_C_mul] says
     simp only [RingHom.coe_comp, Function.comp_apply, coeff_C_mul_X_pow]
   split_ifs <;> simp [f.map_zero]

Mathlib/Data/Seq/Seq.lean

@@ -1031,7 +1031,7 @@ theorem join_join (SS : Seq (Seq1 (Seq1 α))) :
 theorem bind_assoc (s : Seq1 α) (f : α → Seq1 β) (g : β → Seq1 γ) :
     bind (bind s f) g = bind s fun x : α => bind (f x) g := by
   cases' s with a s
-  -- Porting note: Was `simp [bind, map]`.
+  -- porting note (#10745): was `simp [bind, map]`.
   simp only [bind, map_pair, map_join]
   rw [← map_comp]
   simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl]

Mathlib/Data/Seq/WSeq.lean

@@ -720,7 +720,7 @@ theorem dropn_cons (a : α) (s) (n) : drop (cons a s) (n + 1) = drop s n := by
   induction n with
   | zero => simp [drop]
   | succ n n_ih =>
-    -- Porting note: Was `simp [*, drop]`.
+    -- porting note (#10745): was `simp [*, drop]`.
     simp [drop, ← n_ih]
 #align stream.wseq.dropn_cons Stream'.WSeq.dropn_cons
 
@@ -1009,7 +1009,7 @@ theorem exists_get?_of_mem {s : WSeq α} {a} (h : a ∈ s) : ∃ n, some a ∈ g
       apply ret_mem
     · cases' h with n h
       exists n + 1
-      -- Porting note: Was `simp [get?]`.
+      -- porting note (#10745): was `simp [get?]`.
       simpa [get?]
   · intro s' h
     cases' h with n h

Mathlib/Data/Set/Prod.lean

@@ -181,7 +181,8 @@ theorem insert_prod : insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t := by
 
 theorem prod_insert : s ×ˢ insert b t = (fun a => (a, b)) '' s ∪ s ×ˢ t := by
   ext ⟨x, y⟩
-  -- Porting note: was `simp (config := { contextual := true }) [image, iff_def, or_imp, Imp.swap]`
+  -- porting note (#10745):
+  -- was `simp (config := { contextual := true }) [image, iff_def, or_imp, Imp.swap]`
   simp only [mem_prod, mem_insert_iff, image, mem_union, mem_setOf_eq, Prod.mk.injEq]
   refine ⟨fun h => ?_, fun h => ?_⟩
   · obtain ⟨hx, rfl|hy⟩ := h

Mathlib/Data/Sum/Interval.lean

@@ -210,8 +210,8 @@ lemma sumLexLift_nonempty :
       (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f₁ a₁ b₁).Nonempty) ∨
         (∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ ((g₁ a₁ b₂).Nonempty ∨ (g₂ a₁ b₂).Nonempty)) ∨
           ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (f₂ a₂ b₂).Nonempty := by
-  -- porting note: was `simp [nonempty_iff_ne_empty, sumLexLift_eq_empty, not_and_or]`. Could
-  -- add `-exists_and_left, -not_and, -exists_and_right` but easier to squeeze.
+  -- porting note (#10745): was `simp [nonempty_iff_ne_empty, sumLexLift_eq_empty, not_and_or]`.
+  -- Could add `-exists_and_left, -not_and, -exists_and_right` but easier to squeeze.
   simp only [nonempty_iff_ne_empty, Ne.def, sumLexLift_eq_empty, not_and_or, exists_prop,
     not_forall]
 #align finset.sum_lex_lift_nonempty Finset.sumLexLift_nonempty

Mathlib/Geometry/Manifold/Instances/Sphere.lean

@@ -223,7 +223,7 @@ theorem stereo_left_inv (hv : ‖v‖ = 1) {x : sphere (0 : E) 1} (hx : (x : E)
   have pythag : 1 = a ^ 2 + ‖y‖ ^ 2 := by
     have hvy' : ⟪a • v, y⟫_ℝ = 0 := by simp only [inner_smul_left, hvy, mul_zero]
     convert norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ hvy' using 2
-    -- Porting note: was simp [← split] but wasn't finding `norm_eq_of_mem_sphere`
+    -- porting note (#10745): was simp [← split] but wasn't finding `norm_eq_of_mem_sphere`
     · simp only [norm_eq_of_mem_sphere, Nat.cast_one, mul_one, ← split]
     · simp [norm_smul, hv, ← sq, sq_abs]
     · exact sq _

Mathlib/LinearAlgebra/Basic.lean

@@ -408,7 +408,7 @@ theorem isLinearMap_sub {R M : Type*} [Semiring R] [AddCommGroup M] [Module R M]
     IsLinearMap R fun x : M × M => x.1 - x.2 := by
   apply IsLinearMap.mk
   · intro x y
-    -- Porting note: was `simp [add_comm, add_left_comm, sub_eq_add_neg]`
+    -- porting note (#10745): was `simp [add_comm, add_left_comm, sub_eq_add_neg]`
     rw [Prod.fst_add, Prod.snd_add]
     abel
   · intro x y

Mathlib/LinearAlgebra/Determinant.lean

@@ -669,7 +669,8 @@ theorem Basis.det_unitsSMul (e : Basis ι R M) (w : ι → Rˣ) :
       (↑(∏ i, w i)⁻¹ : R) • Matrix.det fun i j => e.repr (f j) i
   simp only [e.repr_unitsSMul]
   convert Matrix.det_mul_column (fun i => (↑(w i)⁻¹ : R)) fun i j => e.repr (f j) i
-  simp only [← Finset.prod_inv_distrib] -- Porting note: was `simp [← Finset.prod_inv_distrib]`
+  -- porting note (#10745): was `simp [← Finset.prod_inv_distrib]`
+  simp only [← Finset.prod_inv_distrib]
   norm_cast
 #align basis.det_units_smul Basis.det_unitsSMul