chore: remove porting notes about simp [(lemma)] (#8227)

Most (but not all) of these are now fixed, presumably due to the latest lean release.

There is still one porting note that remains, about a `(Submonoid.smul_def)` that cannot be un-parenthesized.

Mathlib/Analysis/Normed/Group/AddTorsor.lean

@@ -168,8 +168,7 @@ theorem nndist_vsub_cancel_right (x y z : P) : nndist (x -ᵥ z) (y -ᵥ z) = nn
 
 theorem dist_vadd_vadd_le (v v' : V) (p p' : P) :
     dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p' := by
-  -- porting note: added `()` and lemma name to help simp find a `@[simp]` lemma
-  simpa [(dist_vadd_cancel_right)] using dist_triangle (v +ᵥ p) (v' +ᵥ p) (v' +ᵥ p')
+  simpa using dist_triangle (v +ᵥ p) (v' +ᵥ p) (v' +ᵥ p')
 #align dist_vadd_vadd_le dist_vadd_vadd_le
 
 theorem nndist_vadd_vadd_le (v v' : V) (p p' : P) :
@@ -185,8 +184,7 @@ theorem dist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
 
 theorem nndist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
     nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄ := by
-  -- porting note: added `()` to help simp find a `@[simp]` lemma
-  simp only [← NNReal.coe_le_coe, NNReal.coe_add, ← dist_nndist, (dist_vsub_vsub_le)]
+  simp only [← NNReal.coe_le_coe, NNReal.coe_add, ← dist_nndist, dist_vsub_vsub_le]
 #align nndist_vsub_vsub_le nndist_vsub_vsub_le
 
 theorem edist_vadd_vadd_le (v v' : V) (p p' : P) :

Mathlib/Analysis/NormedSpace/AffineIsometry.lean

@@ -143,14 +143,12 @@ theorem dist_map (x y : P) : dist (f x) (f y) = dist x y := by
   rw [dist_eq_norm_vsub V₂, dist_eq_norm_vsub V, ← map_vsub, f.linearIsometry.norm_map]
 #align affine_isometry.dist_map AffineIsometry.dist_map
 
--- Porting note: added `(dist_map)` to simp
 @[simp]
-theorem nndist_map (x y : P) : nndist (f x) (f y) = nndist x y := by simp [nndist_dist, (dist_map)]
+theorem nndist_map (x y : P) : nndist (f x) (f y) = nndist x y := by simp [nndist_dist]
 #align affine_isometry.nndist_map AffineIsometry.nndist_map
 
--- Porting note: added `(dist_map)` to simp
 @[simp]
-theorem edist_map (x y : P) : edist (f x) (f y) = edist x y := by simp [edist_dist, (dist_map)]
+theorem edist_map (x y : P) : edist (f x) (f y) = edist x y := by simp [edist_dist]
 #align affine_isometry.edist_map AffineIsometry.edist_map
 
 protected theorem isometry : Isometry f :=

Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

@@ -76,8 +76,8 @@ theorem linear_toAffineMap (e : P₁ ≃ᵃ[k] P₂) : e.toAffineMap.linear = e.
 
 theorem toAffineMap_injective : Injective (toAffineMap : (P₁ ≃ᵃ[k] P₂) → P₁ →ᵃ[k] P₂) := by
   rintro ⟨e, el, h⟩ ⟨e', el', h'⟩ H
-  -- porting note: added `()`s and `AffineMap.mk.injEq`
-  simp only [(toAffineMap_mk), (AffineMap.mk.injEq), Equiv.coe_inj,
+  -- porting note: added `AffineMap.mk.injEq`
+  simp only [toAffineMap_mk, AffineMap.mk.injEq, Equiv.coe_inj,
     LinearEquiv.toLinearMap_inj] at H
   congr
   exacts [H.1, H.2]
@@ -167,13 +167,10 @@ def mk' (e : P₁ → P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ p' :
     P₁ ≃ᵃ[k] P₂ where
   toFun := e
   invFun := fun q' : P₂ => e'.symm (q' -ᵥ e p) +ᵥ p
-  -- Porting note: `simp` needs `()`
-  left_inv p' := by simp [h p', (vadd_vsub), (vsub_vadd)]
-  -- Porting note: `simp` needs `()`
-  right_inv q' := by simp [h (e'.symm (q' -ᵥ e p) +ᵥ p), (vadd_vsub), (vsub_vadd)]
+  left_inv p' := by simp [h p', vadd_vsub, vsub_vadd]
+  right_inv q' := by simp [h (e'.symm (q' -ᵥ e p) +ᵥ p), vadd_vsub, vsub_vadd]
   linear := e'
-  -- Porting note: `simp` needs `()`
-  map_vadd' p' v := by simp [h p', h (v +ᵥ p'), (vadd_vsub_assoc), (vadd_vadd)]
+  map_vadd' p' v := by simp [h p', h (v +ᵥ p'), vadd_vsub_assoc, vadd_vadd]
 #align affine_equiv.mk' AffineEquiv.mk'
 
 @[simp]
@@ -327,8 +324,7 @@ def trans (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : P₁ ≃ᵃ[k]
   toEquiv := e.toEquiv.trans e'.toEquiv
   linear := e.linear.trans e'.linear
   map_vadd' p v := by
-    -- porting note: added `()`
-    simp only [LinearEquiv.trans_apply, (coe_toEquiv), (· ∘ ·), Equiv.coe_trans, (map_vadd)]
+    simp only [LinearEquiv.trans_apply, coe_toEquiv, (· ∘ ·), Equiv.coe_trans, map_vadd]
 #align affine_equiv.trans AffineEquiv.trans
 
 @[simp]
@@ -455,8 +451,7 @@ def vaddConst (b : P₁) : V₁ ≃ᵃ[k] P₁ where
 def constVSub (p : P₁) : P₁ ≃ᵃ[k] V₁ where
   toEquiv := Equiv.constVSub p
   linear := LinearEquiv.neg k
-  -- porting note: added `coe_constVSub` and `()`s
-  map_vadd' p' v := by simp [(Equiv.coe_constVSub), (vsub_vadd_eq_vsub_sub), neg_add_eq_sub]
+  map_vadd' p' v := by simp [vsub_vadd_eq_vsub_sub, neg_add_eq_sub]
 #align affine_equiv.const_vsub AffineEquiv.constVSub
 
 @[simp]
@@ -649,8 +644,7 @@ theorem vadd_lineMap (v : V₁) (p₁ p₂ : P₁) (c : k) :
 variable {R' : Type*} [CommRing R'] [Module R' V₁]
 
 theorem homothety_neg_one_apply (c p : P₁) : homothety c (-1 : R') p = pointReflection R' c p := by
-  -- porting note: added `()`, `_`, and `neg_vsub_eq_vsub_rev`
-  simp [(homothety_apply), pointReflection_apply _, (neg_vsub_eq_vsub_rev)]
+  simp [homothety_apply, pointReflection_apply]
 #align affine_map.homothety_neg_one_apply AffineMap.homothety_neg_one_apply
 
 end AffineMap

Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

@@ -250,14 +250,10 @@ end SMul
 instance : Zero (P1 →ᵃ[k] V2) where zero := ⟨0, 0, fun _ _ => (zero_vadd _ _).symm⟩
 
 instance : Add (P1 →ᵃ[k] V2) where
-  add f g := ⟨f + g, f.linear + g.linear,
-      -- porting note: `simp` needs lemmas to be expressions
-      fun p v => by simp [add_add_add_comm, (map_vadd)]⟩
+  add f g := ⟨f + g, f.linear + g.linear, fun p v => by simp [add_add_add_comm]⟩
 
 instance : Sub (P1 →ᵃ[k] V2) where
-  sub f g := ⟨f - g, f.linear - g.linear,
-      -- porting note: `simp` needs lemmas to be expressions
-      fun p v => by simp [sub_add_sub_comm, (map_vadd)]⟩
+  sub f g := ⟨f - g, f.linear - g.linear, fun p v => by simp [sub_add_sub_comm]⟩
 
 instance : Neg (P1 →ᵃ[k] V2) where
   neg f := ⟨-f, -f.linear, fun p v => by simp [add_comm, map_vadd f]⟩
@@ -312,16 +308,12 @@ from `P1` to the vector space `V2` corresponding to `P2`. -/
 instance : AffineSpace (P1 →ᵃ[k] V2) (P1 →ᵃ[k] P2) where
   vadd f g :=
     ⟨fun p => f p +ᵥ g p, f.linear + g.linear,
-      -- porting note: `simp` needs lemmas to be expressions
-      letI : AddAction V2 P2 := inferInstance
-      fun p v => by simp [vadd_vadd, add_right_comm, (map_vadd)]⟩
+      fun p v => by simp [vadd_vadd, add_right_comm]⟩
   zero_vadd f := ext fun p => zero_vadd _ (f p)
   add_vadd f₁ f₂ f₃ := ext fun p => add_vadd (f₁ p) (f₂ p) (f₃ p)
   vsub f g :=
     ⟨fun p => f p -ᵥ g p, f.linear - g.linear, fun p v => by
-      -- porting note: `simp` needs lemmas to be expressions
-      simp [(map_vadd), (vsub_vadd_eq_vsub_sub), (vadd_vsub_assoc),
-        add_sub, sub_add_eq_add_sub]⟩
+      simp [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub, sub_add_eq_add_sub]⟩
   vsub_vadd' f g := ext fun p => vsub_vadd (f p) (g p)
   vadd_vsub' f g := ext fun p => vadd_vsub (f p) (g p)
 
@@ -542,9 +534,7 @@ theorem lineMap_linear (p₀ p₁ : P1) :
 #align affine_map.line_map_linear AffineMap.lineMap_linear
 
 theorem lineMap_same_apply (p : P1) (c : k) : lineMap p p c = p := by
-  letI : AddAction V1 P1 := inferInstance
-  -- porting note: `simp` needs lemmas to be expressions
-  simp [(lineMap_apply), (vsub_self)]
+  simp [lineMap_apply]
 #align affine_map.line_map_same_apply AffineMap.lineMap_same_apply
 
 @[simp]
@@ -554,15 +544,12 @@ theorem lineMap_same (p : P1) : lineMap p p = const k k p :=
 
 @[simp]
 theorem lineMap_apply_zero (p₀ p₁ : P1) : lineMap p₀ p₁ (0 : k) = p₀ := by
-  letI : AddAction V1 P1 := inferInstance
-  -- porting note: `simp` needs lemmas to be expressions
-  simp [(lineMap_apply)]
+  simp [lineMap_apply]
 #align affine_map.line_map_apply_zero AffineMap.lineMap_apply_zero
 
 @[simp]
 theorem lineMap_apply_one (p₀ p₁ : P1) : lineMap p₀ p₁ (1 : k) = p₁ := by
-  -- porting note: `simp` needs lemmas to be expressions
-  simp [(lineMap_apply), (vsub_vadd)]
+  simp [lineMap_apply]
 #align affine_map.line_map_apply_one AffineMap.lineMap_apply_one
 
 @[simp]
@@ -596,8 +583,7 @@ variable {k}
 @[simp]
 theorem apply_lineMap (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) (c : k) :
     f (lineMap p₀ p₁ c) = lineMap (f p₀) (f p₁) c := by
-  -- porting note: `simp` needs lemmas to be expressions
-  simp [(lineMap_apply), (map_vadd), (linearMap_vsub)]
+  simp [lineMap_apply]
 #align affine_map.apply_line_map AffineMap.apply_lineMap
 
 @[simp]