chore: resolve some simp-related porting notes (#12074)

In all cases, the original proof works now. I presume this is due to simp changes in Lean 4.7, but haven't verified.

Mathlib/Algebra/Polynomial/Basic.lean

@@ -688,9 +688,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 (#10745): was `simp [← ofFinsupp_single, coeff, LinearMap.coe_mk]`.
-  rw [← ofFinsupp_single]
-  simp only [coeff, LinearMap.coe_mk]
+  simp only [← ofFinsupp_single, coeff, LinearMap.coe_mk]
   rw [Finsupp.single_apply]
 #align polynomial.coeff_monomial Polynomial.coeff_monomial
 
@@ -956,8 +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 (#10745): was `simp [← ofFinsupp_single, Finsupp.single_left_inj ha]`
-  rw [← ofFinsupp_single, ← ofFinsupp_single, ofFinsupp.injEq, Finsupp.single_left_inj ha]
+  simp only [← ofFinsupp_single, ofFinsupp.injEq, Finsupp.single_left_inj ha]
 #align polynomial.monomial_left_inj Polynomial.monomial_left_inj
 
 theorem binomial_eq_binomial {k l m n : ℕ} {u v : R} (hu : u ≠ 0) (hv : v ≠ 0) :

Mathlib/Analysis/Complex/Conformal.lean

@@ -58,10 +58,8 @@ 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 (#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₁]
+    -- porting note (#10745): was `simp`; explicitly supplied simp lemma
+    simp [smul_inv_smul₀ minor₁]
 #align is_conformal_map_complex_linear isConformalMap_complex_linear
 
 theorem isConformalMap_complex_linear_conj {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) :
@@ -87,17 +85,10 @@ 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 (#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]
+    simp
   · refine' Or.inr ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, _⟩
     ext1
-    -- 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,
-      ContinuousLinearEquiv.coe_coe, conjCLE_apply, conjLIE_apply, conj_conj]
+    simp
 #align is_conformal_map.is_complex_or_conj_linear IsConformalMap.is_complex_or_conj_linear
 
 /-- A real continuous linear map on the complex plane is conformal if and only if the map or its

Mathlib/Analysis/NormedSpace/AddTorsor.lean

@@ -70,10 +70,8 @@ theorem nndist_homothety_center (p₁ p₂ : P) (c : 𝕜) :
 theorem dist_lineMap_lineMap (p₁ p₂ : P) (c₁ c₂ : 𝕜) :
     dist (lineMap p₁ p₂ c₁) (lineMap p₁ p₂ c₂) = dist c₁ c₂ * dist p₁ p₂ := by
   rw [dist_comm p₁ p₂]
-  -- Porting note: was `simp only [lineMap_apply, dist_eq_norm_vsub, vadd_vsub_vadd_cancel_right,`
-  -- `← sub_smul, norm_smul, vsub_eq_sub]`
-  rw [lineMap_apply, lineMap_apply, dist_eq_norm_vsub V, vadd_vsub_vadd_cancel_right,
-    ← sub_smul, norm_smul, ← vsub_eq_sub, ← dist_eq_norm_vsub V, ← dist_eq_norm_vsub 𝕜]
+  simp only [lineMap_apply, dist_eq_norm_vsub, vadd_vsub_vadd_cancel_right,
+    ← sub_smul, norm_smul, vsub_eq_sub]
 #align dist_line_map_line_map dist_lineMap_lineMap
 
 @[simp]
@@ -89,9 +87,7 @@ theorem lipschitzWith_lineMap (p₁ p₂ : P) : LipschitzWith (nndist p₁ p₂)
 
 @[simp]
 theorem dist_lineMap_left (p₁ p₂ : P) (c : 𝕜) : dist (lineMap p₁ p₂ c) p₁ = ‖c‖ * dist p₁ p₂ := by
-  -- Porting note: was
-  -- simpa only [lineMap_apply_zero, dist_zero_right] using dist_lineMap_lineMap p₁ p₂ c 0
-  rw [← dist_zero_right, ← dist_lineMap_lineMap, lineMap_apply_zero]
+  simpa only [lineMap_apply_zero, dist_zero_right] using dist_lineMap_lineMap p₁ p₂ c 0
 #align dist_line_map_left dist_lineMap_left
 
 @[simp]
@@ -114,9 +110,7 @@ theorem nndist_left_lineMap (p₁ p₂ : P) (c : 𝕜) :
 @[simp]
 theorem dist_lineMap_right (p₁ p₂ : P) (c : 𝕜) :
     dist (lineMap p₁ p₂ c) p₂ = ‖1 - c‖ * dist p₁ p₂ := by
-  -- Porting note: was
-  -- `simpa only [lineMap_apply_one, dist_eq_norm'] using dist_lineMap_lineMap p₁ p₂ c 1`
-  rw [← dist_eq_norm', ← dist_lineMap_lineMap, lineMap_apply_one]
+  simpa only [lineMap_apply_one, dist_eq_norm'] using dist_lineMap_lineMap p₁ p₂ c 1
 #align dist_line_map_right dist_lineMap_right
 
 @[simp]

Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean

@@ -189,29 +189,20 @@ noncomputable instance : NormedAddCommGroup (V →A[𝕜] W) :=
       neg' := fun f => by
         simp [(ContinuousAffineMap.neg_apply)]
       add_le' := fun f g => by
-        simp only [coe_add, max_le_iff]
-        -- Porting note: previously `Pi.add_apply, add_contLinear, ` in the previous `simp only`
-        -- suffices, but now they don't fire.
-        rw [add_contLinear]
+        simp only [coe_add, max_le_iff, Pi.add_apply, add_contLinear]
         exact
           ⟨(norm_add_le _ _).trans (add_le_add (le_max_left _ _) (le_max_left _ _)),
             (norm_add_le _ _).trans (add_le_add (le_max_right _ _) (le_max_right _ _))⟩
       eq_zero_of_map_eq_zero' := fun f h₀ => by
         rcases max_eq_iff.mp h₀ with (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩) <;> rw [h₁] at h₂
         · rw [norm_le_zero_iff, contLinear_eq_zero_iff_exists_const] at h₂
           obtain ⟨q, rfl⟩ := h₂
-          simp only [norm_eq_zero] at h₁
-          -- Porting note: prevously `coe_const, Function.const_apply` were in the previous
-          -- `simp only`, but now they don't fire.
-          rw [coe_const, Function.const_apply] at h₁
+          simp only [norm_eq_zero, coe_const, Function.const_apply] at h₁
           rw [h₁]
           rfl
         · rw [norm_eq_zero', contLinear_eq_zero_iff_exists_const] at h₁
           obtain ⟨q, rfl⟩ := h₁
-          simp only [norm_le_zero_iff] at h₂
-          -- Porting note: prevously `coe_const, Function.const_apply` were in the previous
-          -- `simp only`, but now they don't fire.
-          rw [coe_const, Function.const_apply] at h₂
+          simp only [norm_le_zero_iff, coe_const, Function.const_apply] at h₂
           rw [h₂]
           rfl }
 

Mathlib/Analysis/NormedSpace/lpSpace.lean

@@ -502,9 +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 (#10745): was `simp [lp.eq_zero' f]`
-            rw [lp.eq_zero' f]
-            simp only [zero_add, norm_zero, le_refl] -- porting note (#11083): just `simp` was slow
+          · simp only [lp.eq_zero' f, zero_add, norm_zero, le_refl]
           refine' (lp.isLUB_norm (f + g)).2 _
           rintro x ⟨i, rfl⟩
           refine' le_trans _ (add_mem_upperBounds_add

Mathlib/Analysis/PSeries.lean

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

Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

@@ -137,13 +137,10 @@ theorem colimitLimitToLimitColimit_injective :
     ext j
     -- Now it's just a calculation using `W` and `w`.
     simp only [Functor.comp_map, Limit.map_π_apply, curry_obj_map_app, swap_map]
-    rw [← W _ _ (fH j)]
-    rw [← W _ _ (gH j)]
-    -- Porting note: this was `simp [w]` in lean 3; this is presumably a confluence issue
-    rw [lim_map, lim_map, Limit.map_π_apply, Limit.map_π_apply, Functor.map_comp,
-      Functor.map_comp, FunctorToTypes.comp, FunctorToTypes.comp, curry_obj_map_app,
-      curry_obj_map_app, curry_obj_map_app, Functor.comp_map, Functor.comp_map,
-      Functor.comp_map, swap_map, swap_map, swap_map, w]
+    rw [← W _ _ (fH j), ← W _ _ (gH j)]
+    -- Porting note(#10745): had to add `Limit.map_π_apply`
+    -- (which was un-tagged simp since "simp can prove it")
+    simp [Limit.map_π_apply, w]
 #align category_theory.limits.colimit_limit_to_limit_colimit_injective CategoryTheory.Limits.colimitLimitToLimitColimit_injective
 
 end

Mathlib/CategoryTheory/Sites/DenseSubsite.lean

@@ -200,12 +200,8 @@ theorem pushforwardFamily_compatible {X} (x : ℱ.obj (op X)) :
   erw [← α.naturality (G.preimage _).op]
   erw [← α.naturality (G.preimage _).op]
   refine' congr_fun _ x
-  -- Porting note: these next 3 tactics (simp, rw, simp) were just one big `simp only` in Lean 3
-  -- but I can't get `simp` to do the `rw` line.
-  simp only [Functor.comp_map, ← Category.assoc, Functor.op_map, Quiver.Hom.unop_op]
-  rw [← ℱ.map_comp, ← ℱ.map_comp] -- `simp only [← ℱ.map_comp]` does nothing, even if I add
-  -- the relevant explicit inputs
-  simp only [← op_comp, G.image_preimage]
+  simp only [Functor.comp_map, ← Category.assoc, Functor.op_map, Quiver.Hom.unop_op,
+    ← ℱ.map_comp, ← op_comp, G.image_preimage]
   congr 3
   simp [e]
 #align category_theory.cover_dense.types.pushforward_family_compatible CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible

Mathlib/FieldTheory/RatFunc.lean

@@ -1543,7 +1543,7 @@ theorem eval_mul {x y : RatFunc K} (hx : Polynomial.eval₂ f a (denom x) ≠ 0)
     cases mul_eq_zero.mp this <;> contradiction
   rw [div_mul_div_comm, eq_div_iff (mul_ne_zero hx hy), div_eq_mul_inv, mul_right_comm, ←
     div_eq_mul_inv, div_eq_iff hxy]
-  simp only [← Polynomial.eval₂_mul]  -- Porting note: was `repeat' rw [← Polynomial.eval₂_mul]`
+  repeat' rw [← Polynomial.eval₂_mul]
   congr 1
   apply num_denom_mul
 #align ratfunc.eval_mul RatFunc.eval_mul

Mathlib/MeasureTheory/Constructions/Prod/Integral.lean

@@ -234,9 +234,7 @@ theorem hasFiniteIntegral_prod_iff ⦃f : α × β → E⦄ (h1f : StronglyMeasu
     HasFiniteIntegral f (μ.prod ν) ↔
       (∀ᵐ x ∂μ, HasFiniteIntegral (fun y => f (x, y)) ν) ∧
         HasFiniteIntegral (fun x => ∫ y, ‖f (x, y)‖ ∂ν) μ := by
-  simp only [HasFiniteIntegral]
-  -- porting note (#10745): was `simp`
-  rw [lintegral_prod_of_measurable _ h1f.ennnorm]
+  simp only [HasFiniteIntegral, lintegral_prod_of_measurable _ h1f.ennnorm]
   have (x) : ∀ᵐ y ∂ν, 0 ≤ ‖f (x, y)‖ := by filter_upwards with y using norm_nonneg _
   simp_rw [integral_eq_lintegral_of_nonneg_ae (this _)
       (h1f.norm.comp_measurable measurable_prod_mk_left).aestronglyMeasurable,

Mathlib/RingTheory/Valuation/Basic.lean

@@ -486,9 +486,7 @@ theorem isEquiv_iff_val_lt_one [LinearOrderedCommGroupWithZero Γ₀]
   · rw [isEquiv_iff_val_eq_one]
     intro h x
     by_cases hx : x = 0
-    · -- Porting note: this proof was `simp only [(zero_iff _).2 hx, zero_ne_one]`
-      rw [(zero_iff _).2 hx, (zero_iff _).2 hx]
-      simp only [zero_ne_one]
+    · simp only [(zero_iff _).2 hx, zero_ne_one]
     constructor
     · intro hh
       by_contra h_1

Mathlib/Topology/Compactness/SigmaCompact.lean

@@ -247,8 +247,7 @@ instance [Countable ι] {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
     refine' ⟨⟨fun n => ⋃ k ≤ n, Sigma.mk (f k) '' compactCovering (X (f k)) n, fun n => _, _⟩⟩
     · refine' (finite_le_nat _).isCompact_biUnion fun k _ => _
       exact (isCompact_compactCovering _ _).image continuous_sigmaMk
-    · simp only [iUnion_eq_univ_iff, Sigma.forall, mem_iUnion]
-      rw [hf.forall] -- Porting note: `simp only` failed to use `hf.forall`
+    · simp only [iUnion_eq_univ_iff, Sigma.forall, mem_iUnion, hf.forall]
       intro k y
       rcases exists_mem_compactCovering y with ⟨n, hn⟩
       refine' ⟨max k n, k, le_max_left _ _, mem_image_of_mem _ _⟩