chore: remove more simp-related porting notes which are fixed now (#1…

…2128)

Co-authored-by: Moritz Firsching <firsching@google.com>

Mathlib/Algebra/BigOperators/Associated.lean

@@ -109,12 +109,10 @@ theorem Finset.prod_primes_dvd [CancelCommMonoidWithZero α] [Unique αˣ] {s :
       Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
         (by simpa only [Multiset.map_id', Finset.mem_def] using div)
         (by
-          -- POrting note: was
-          -- `simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter, ←
-          --    Multiset.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup]`
+          simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter, ←
+            Multiset.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup]
+          -- Porting note: these lines were not necessary
           intro a
-          simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter]
-          change Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
           apply le_of_eq_of_le (Multiset.count_eq_card_filter_eq _ _).symm
           apply Multiset.nodup_iff_count_le_one.mp
           exact s.nodup)

Mathlib/Analysis/NormedSpace/AddTorsor.lean

@@ -44,9 +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 (#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]
+  simp [homothety_def, norm_smul, ← dist_eq_norm_vsub, dist_comm]
 #align dist_center_homothety dist_center_homothety
 
 @[simp]
@@ -276,8 +274,7 @@ theorem dist_midpoint_midpoint_le (p₁ p₂ p₃ p₄ : V) :
     dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2 := by
   -- Porting note: was `simpa using dist_midpoint_midpoint_le' p₁ p₂ p₃ p₄`
   have := dist_midpoint_midpoint_le' (𝕜 := ℝ) p₁ p₂ p₃ p₄
-  rw [Real.norm_eq_abs, abs_two] at this
-  exact this
+  simpa using this
 #align dist_midpoint_midpoint_le dist_midpoint_midpoint_le
 
 theorem nndist_midpoint_midpoint_le (p₁ p₂ p₃ p₄ : V) :

Mathlib/Order/Interval.lean

@@ -555,9 +555,7 @@ instance lattice : Lattice (Interval α) :=
         lift t to NonemptyInterval α using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hb
         lift c to NonemptyInterval α using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hc
         change _ ≤ dite _ _ _
-        -- Porting note: was `simp only` but that fails to use the second lemma.
-        rw [WithBot.some_eq_coe, WithBot.coe_le_coe] at hb hc
-        simp only [WithBot.some_eq_coe, WithBot.coe_le_coe] -- at hb hc ⊢
+        simp only [WithBot.some_eq_coe, WithBot.coe_le_coe] at hb hc ⊢
         rw [dif_pos, WithBot.coe_le_coe]
         exact ⟨sup_le hb.1 hc.1, le_inf hb.2 hc.2⟩
         -- Porting note: had to add the next 6 lines including the changes because

Mathlib/RingTheory/Polynomial/Dickson.lean

@@ -125,14 +125,10 @@ There is exactly one other Lambda structure on `ℤ[X]` in terms of binomial pol
 
 -/
 
-
 theorem dickson_one_one_eval_add_inv (x y : R) (h : x * y = 1) :
     ∀ n, (dickson 1 (1 : R) n).eval (x + y) = x ^ n + y ^ n
   | 0 => by
-    -- Porting note: Original proof was
-    -- `simp only [bit0, eval_one, eval_add, pow_zero, dickson_zero]; norm_num`
-    suffices eval (x + y) 2 = 2 by convert this <;> norm_num
-    exact eval_nat_cast
+    simp only [eval_one, eval_add, pow_zero, dickson_zero]; norm_num
   | 1 => by simp only [eval_X, dickson_one, pow_one]
   | n + 2 => by
     simp only [eval_sub, eval_mul, dickson_one_one_eval_add_inv x y h _, eval_X, dickson_add_two,

Mathlib/RingTheory/TensorProduct/Basic.lean

@@ -516,11 +516,9 @@ instance instCommSemiring : CommSemiring (A ⊗[R] B) where
       · intro a₂ b₂
         simp [mul_comm]
       · intro a₂ b₂ ha hb
-        -- porting note (#10745): was `simp` not `rw`
-        rw [mul_add, add_mul, ha, hb]
+        simp [mul_add, add_mul, ha, hb]
     · intro x₁ x₂ h₁ h₂
-      -- porting note (#10745): was `simp` not `rw`
-      rw [mul_add, add_mul, h₁, h₂]
+      simp [mul_add, add_mul, h₁, h₂]
 
 end CommSemiring
 
@@ -1214,7 +1212,7 @@ protected def module : Module (A ⊗[R] B) M where
   smul_add x m₁ m₂ := by simp only [(· • ·), map_add]
   add_smul x y m := by simp only [(· • ·), map_add, LinearMap.add_apply]
   one_smul m := by
-    -- Porting note: was one `simp only` not two in lean 3
+    -- Porting note: was one `simp only`, not two
     simp only [(· • ·), Algebra.TensorProduct.one_def]
     simp only [moduleAux_apply, one_smul]
   mul_smul x y m := by
@@ -1227,28 +1225,22 @@ protected def module : Module (A ⊗[R] B) M where
     · intro a b
       simp only [(· • ·), mul_zero, map_zero, LinearMap.zero_apply]
     · intro a₁ b₁ a₂ b₂
-      -- porting note; was one `simp only` not two and a `rw` in mathlib3
+      -- Porting note: was one `simp only`, not two
       simp only [(· • ·), Algebra.TensorProduct.tmul_mul_tmul]
-      simp only [moduleAux_apply, mul_smul]
-      rw [smul_comm a₁ b₂]
+      simp only [moduleAux_apply, mul_smul, smul_comm a₁ b₂]
     · intro z w hz hw a b
-      -- Porting note: was one `simp only` but random stuff doesn't work
+      -- Porting note: was one `simp only`, but random stuff doesn't work
       simp only [(· • ·)] at hz hw ⊢
-      simp only [moduleAux_apply]
-      rw [mul_add]  -- simp only doesn't work
-      simp only [LinearMap.map_add, LinearMap.add_apply, moduleAux_apply, hz, hw, smul_add]
+      simp only [moduleAux_apply, mul_add, LinearMap.map_add,
+        LinearMap.add_apply, moduleAux_apply, hz, hw, smul_add]
     · intro z w _ _
       simp only [(· • ·), mul_zero, map_zero, LinearMap.zero_apply]
     · intro a b z w hz hw
-      simp only [(· • ·)] at hz hw
-      simp only [(· • ·), LinearMap.map_add, add_mul, LinearMap.add_apply, hz, hw]
+      simp only [(· • ·)] at hz hw ⊢
+      simp only [LinearMap.map_add, add_mul, LinearMap.add_apply, hz, hw]
     · intro u v _ _ z w hz hw
-      simp only [(· • ·)] at hz hw
-      -- Porting note: no idea why this is such a struggle
-      simp only [(· • ·)]
-      rw [add_mul, LinearMap.map_add, LinearMap.add_apply, hz, hw]
-      simp only [LinearMap.map_add, LinearMap.add_apply]
-      rw [add_add_add_comm]
+      simp only [(· • ·)] at hz hw ⊢
+      simp only [add_mul, LinearMap.map_add, LinearMap.add_apply, hz, hw, add_add_add_comm]
 #align tensor_product.algebra.module TensorProduct.Algebra.module
 
 attribute [local instance] TensorProduct.Algebra.module

Mathlib/RingTheory/Trace.lean

@@ -142,13 +142,10 @@ theorem trace_trace_of_basis [Algebra S T] [IsScalarTower R S T] {ι κ : Type*}
   cases nonempty_fintype κ
   rw [trace_eq_matrix_trace (b.smul c), trace_eq_matrix_trace b, trace_eq_matrix_trace c,
     Matrix.trace, Matrix.trace, Matrix.trace, ← Finset.univ_product_univ, Finset.sum_product]
-  refine' Finset.sum_congr rfl fun i _ => _
+  refine Finset.sum_congr rfl fun i _ ↦ ?_
   simp only [AlgHom.map_sum, smul_leftMulMatrix, Finset.sum_apply,
-    Matrix.diag]
--- Porting note: the `rw` was inside `simp only`, but it doesn't work anymore.
-  rw [Finset.sum_apply
+    Matrix.diag, Finset.sum_apply
       i (Finset.univ : Finset κ) fun y => leftMulMatrix b (leftMulMatrix c x y y)]
-  apply Finset.sum_apply
 #align algebra.trace_trace_of_basis Algebra.trace_trace_of_basis
 
 theorem trace_comp_trace_of_basis [Algebra S T] [IsScalarTower R S T] {ι κ : Type*} [Finite ι]
@@ -434,7 +431,7 @@ theorem trace_eq_sum_automorphisms (x : L) [FiniteDimensional K L] [IsGalois K L
   rw [← Fintype.sum_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]
   · rw [← trace_eq_sum_embeddings (AlgebraicClosure L)]
     · simp only [algebraMap_eq_smul_one]
--- Porting note: `smul_one_smul` was in the `simp only`.
+      -- Porting note: `smul_one_smul` was in the `simp only`.
       apply smul_one_smul
   · intro σ
     simp only [Normal.algHomEquivAut, AlgHom.restrictNormal', Equiv.coe_fn_mk,