diff --git a/Mathlib/Algebra/GCDMonoid/Basic.lean b/Mathlib/Algebra/GCDMonoid/Basic.lean
index 33ee935b116c2..651043428337f 100644
--- a/Mathlib/Algebra/GCDMonoid/Basic.lean
+++ b/Mathlib/Algebra/GCDMonoid/Basic.lean
@@ -1048,15 +1048,15 @@ noncomputable def gcdMonoidOfGCD [DecidableEq α] (gcd : α → α → α)
     lcm := fun a b =>
       if a = 0 then 0 else Classical.choose ((gcd_dvd_left a b).trans (Dvd.intro b rfl))
     gcd_mul_lcm := fun a b => by
-      -- Porting note (#10971): need `dsimp only` before `split_ifs`
-      dsimp only
+      -- Porting note(#12129): additional beta reduction needed
+      beta_reduce
       split_ifs with a0
       · rw [mul_zero, a0, zero_mul]
       · rw [← Classical.choose_spec ((gcd_dvd_left a b).trans (Dvd.intro b rfl))]
     lcm_zero_left := fun a => if_pos rfl
     lcm_zero_right := fun a => by
-      -- Porting note (#10971): need `dsimp only` before `split_ifs`
-      dsimp only
+      -- Porting note(#12129): additional beta reduction needed
+      beta_reduce
       split_ifs with a0
       · rfl
       have h := (Classical.choose_spec ((gcd_dvd_left a 0).trans (Dvd.intro 0 rfl))).symm
@@ -1108,8 +1108,8 @@ noncomputable def normalizedGCDMonoidOfGCD [NormalizationMonoid α] [DecidableEq
         rw [← normalize_gcd] at this
         rwa [normalize.map_mul, normalize_gcd, mul_right_inj' h1] at h2
     gcd_mul_lcm := fun a b => by
-      -- Porting note (#10971): need `dsimp only`
-      dsimp only
+      -- Porting note(#12129): additional beta reduction needed
+      beta_reduce
       split_ifs with a0
       · rw [mul_zero, a0, zero_mul]
       · rw [←
@@ -1117,8 +1117,8 @@ noncomputable def normalizedGCDMonoidOfGCD [NormalizationMonoid α] [DecidableEq
         exact normalize_associated (a * b)
     lcm_zero_left := fun a => if_pos rfl
     lcm_zero_right := fun a => by
-      -- Porting note (#10971): need `dsimp only`
-      dsimp only
+      -- Porting note(#12129): additional beta reduction needed
+      beta_reduce
       split_ifs with a0
       · rfl
       rw [← normalize_eq_zero] at a0
@@ -1141,8 +1141,8 @@ noncomputable def gcdMonoidOfLCM [DecidableEq α] (lcm : α → α → α)
   { lcm
     gcd := fun a b => if a = 0 then b else if b = 0 then a else Classical.choose (exists_gcd a b)
     gcd_mul_lcm := fun a b => by
-      -- Porting note (#10971): need `dsimp only`
-      dsimp only
+      -- Porting note(#12129): additional beta reduction needed
+      beta_reduce
       split_ifs with h h_1
       · rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]
       · rw [h_1, eq_zero_of_zero_dvd (dvd_lcm_right _ _)]
@@ -1150,8 +1150,8 @@ noncomputable def gcdMonoidOfLCM [DecidableEq α] (lcm : α → α → α)
     lcm_zero_left := fun a => eq_zero_of_zero_dvd (dvd_lcm_left _ _)
     lcm_zero_right := fun a => eq_zero_of_zero_dvd (dvd_lcm_right _ _)
     gcd_dvd_left := fun a b => by
-      -- Porting note (#10971): need `dsimp only`
-      dsimp only
+      -- Porting note(#12129): additional beta reduction needed
+      beta_reduce
       split_ifs with h h_1
       · rw [h]
         apply dvd_zero
@@ -1167,8 +1167,8 @@ noncomputable def gcdMonoidOfLCM [DecidableEq α] (lcm : α → α → α)
         mul_dvd_mul_iff_right h]
       apply dvd_lcm_right
     gcd_dvd_right := fun a b => by
-      -- Porting note (#10971): need `dsimp only`
-      dsimp only
+      -- Porting note(#12129): additional beta reduction needed
+      beta_reduce
       split_ifs with h h_1
       · exact dvd_rfl
       · rw [h_1]
@@ -1184,8 +1184,8 @@ noncomputable def gcdMonoidOfLCM [DecidableEq α] (lcm : α → α → α)
         mul_dvd_mul_iff_right h_1]
       apply dvd_lcm_left
     dvd_gcd := fun {a b c} ac ab => by
-      -- Porting note (#10971): need `dsimp only`
-      dsimp only
+      -- Porting note(#12129): additional beta reduction needed
+      beta_reduce
       split_ifs with h h_1
       · exact ab
       · exact ac
@@ -1219,7 +1219,7 @@ noncomputable def normalizedGCDMonoidOfLCM [NormalizationMonoid α] [DecidableEq
       if a = 0 then normalize b
       else if b = 0 then normalize a else Classical.choose (exists_gcd a b)
     gcd_mul_lcm := fun a b => by
-      dsimp only
+      beta_reduce
       split_ifs with h h_1
       · rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]
       · rw [h_1, eq_zero_of_zero_dvd (dvd_lcm_right _ _), mul_zero, mul_zero]
@@ -1247,7 +1247,7 @@ noncomputable def normalizedGCDMonoidOfLCM [NormalizationMonoid α] [DecidableEq
     lcm_zero_left := fun a => eq_zero_of_zero_dvd (dvd_lcm_left _ _)
     lcm_zero_right := fun a => eq_zero_of_zero_dvd (dvd_lcm_right _ _)
     gcd_dvd_left := fun a b => by
-      dsimp only
+      beta_reduce
       split_ifs with h h_1
       · rw [h]
         apply dvd_zero
@@ -1263,7 +1263,7 @@ noncomputable def normalizedGCDMonoidOfLCM [NormalizationMonoid α] [DecidableEq
         mul_comm, mul_dvd_mul_iff_right h]
       apply dvd_lcm_right
     gcd_dvd_right := fun a b => by
-      dsimp only
+      beta_reduce
       split_ifs with h h_1
       · exact (normalize_associated _).dvd
       · rw [h_1]
@@ -1279,7 +1279,7 @@ noncomputable def normalizedGCDMonoidOfLCM [NormalizationMonoid α] [DecidableEq
         mul_dvd_mul_iff_right h_1]
       apply dvd_lcm_left
     dvd_gcd := fun {a b c} ac ab => by
-      dsimp only
+      beta_reduce
       split_ifs with h h_1
       · apply dvd_normalize_iff.2 ab
       · apply dvd_normalize_iff.2 ac
@@ -1357,9 +1357,10 @@ instance (priority := 100) : NormalizedGCDMonoid G₀ where
   normUnit x := if h : x = 0 then 1 else (Units.mk0 x h)⁻¹
   normUnit_zero := dif_pos rfl
   normUnit_mul := fun {x y} x0 y0 => Units.eq_iff.1 (by
-    -- Porting note (#10971): need `dsimp only`, also `simp` reaches maximum heartbeat
+    -- Porting note(#12129): additional beta reduction needed
+    -- Porting note: `simp` reaches maximum heartbeat
     -- by Units.eq_iff.mp (by simp only [x0, y0, mul_comm])
-    dsimp only
+    beta_reduce
     split_ifs with h
     · rw [mul_eq_zero] at h
       cases h
@@ -1367,26 +1368,26 @@ instance (priority := 100) : NormalizedGCDMonoid G₀ where
       · exact absurd ‹y = 0› y0
     · rw [Units.mk0_mul, mul_inv_rev, mul_comm] )
   normUnit_coe_units u := by
-    -- Porting note (#10971): need `dsimp only`
-    dsimp only
+    -- Porting note(#12129): additional beta reduction needed
+    beta_reduce
     rw [dif_neg (Units.ne_zero _), Units.mk0_val]
   gcd a b := if a = 0 ∧ b = 0 then 0 else 1
   lcm a b := if a = 0 ∨ b = 0 then 0 else 1
   gcd_dvd_left a b := by
-    -- Porting note (#10971): need `dsimp only`
-    dsimp only
+    -- Porting note(#12129): additional beta reduction needed
+    beta_reduce
     split_ifs with h
     · rw [h.1]
     · exact one_dvd _
   gcd_dvd_right a b := by
-    -- Porting note (#10971): need `dsimp only`
-    dsimp only
+    -- Porting note(#12129): additional beta reduction needed
+    beta_reduce
     split_ifs with h
     · rw [h.2]
     · exact one_dvd _
   dvd_gcd := fun {a b c} hac hab => by
-    -- Porting note (#10971): need `dsimp only`
-    dsimp only
+    -- Porting note(#12129): additional beta reduction needed
+    beta_reduce
     split_ifs with h
     · apply dvd_zero
     · rw [not_and_or] at h
@@ -1402,8 +1403,8 @@ instance (priority := 100) : NormalizedGCDMonoid G₀ where
     · by_cases hb : b = 0
       · simp only [hb, and_true, or_true, ite_true, mul_zero]
         exact Associated.refl _
-      -- Porting note (#10971): need `dsimp only`
-      · dsimp only
+      -- Porting note(#12129): additional beta reduction needed
+      · beta_reduce
         rw [if_neg (not_and_of_not_left _ ha), one_mul, if_neg (not_or_of_not ha hb)]
         exact (associated_one_iff_isUnit.mpr ((IsUnit.mk0 _ ha).mul (IsUnit.mk0 _ hb))).symm
   lcm_zero_left b := if_pos (Or.inl rfl)
diff --git a/Mathlib/Algebra/GroupPower/IterateHom.lean b/Mathlib/Algebra/GroupPower/IterateHom.lean
index aecec79c13d47..8d805b07acd68 100644
--- a/Mathlib/Algebra/GroupPower/IterateHom.lean
+++ b/Mathlib/Algebra/GroupPower/IterateHom.lean
@@ -175,12 +175,13 @@ section Semigroup
 
 variable [Semigroup G] {a b c : G}
 
--- Porting note (#10971): need `dsimp only`, see https://leanprover.zulipchat.com/#narrow/stream/
+-- Porting note(#12129): additional beta reduction needed
+-- see also https://leanprover.zulipchat.com/#narrow/stream/
 -- 287929-mathlib4/topic/dsimp.20before.20rw/near/317063489
 @[to_additive]
 theorem SemiconjBy.function_semiconj_mul_left (h : SemiconjBy a b c) :
     Function.Semiconj (a * ·) (b * ·) (c * ·) := fun j => by
-  dsimp only; rw [← mul_assoc, h.eq, mul_assoc]
+  beta_reduce; rw [← mul_assoc, h.eq, mul_assoc]
 #align semiconj_by.function_semiconj_mul_left SemiconjBy.function_semiconj_mul_left
 #align add_semiconj_by.function_semiconj_add_left AddSemiconjBy.function_semiconj_add_left
 
diff --git a/Mathlib/Algebra/MonoidAlgebra/Basic.lean b/Mathlib/Algebra/MonoidAlgebra/Basic.lean
index 4596d05217605..628af7d731f7f 100644
--- a/Mathlib/Algebra/MonoidAlgebra/Basic.lean
+++ b/Mathlib/Algebra/MonoidAlgebra/Basic.lean
@@ -699,8 +699,8 @@ def liftMagma [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] :
     { liftAddHom fun x => (smulAddHom k A).flip (f x) with
       toFun := fun a => a.sum fun m t => t • f m
       map_smul' := fun t' a => by
-        -- Porting note: `dsimp` is required for beta reduction.
-        dsimp only []
+        -- Porting note(#12129): additional beta reduction needed
+        beta_reduce
         rw [Finsupp.smul_sum, sum_smul_index']
         · simp_rw [smul_assoc, MonoidHom.id_apply]
         · intro m
@@ -1038,8 +1038,8 @@ def equivariantOfLinearOfComm : V →ₗ[MonoidAlgebra k G] W where
   toFun := f
   map_add' v v' := by simp
   map_smul' c v := by
-    -- Porting note: `dsimp` is required for beta reduction.
-    dsimp only []
+    -- Porting note(#12129): additional beta reduction needed
+    beta_reduce
     -- Porting note: Was `apply`.
     refine Finsupp.induction c ?_ ?_
     · simp
@@ -1757,8 +1757,8 @@ protected def AddMonoidAlgebra.toMultiplicative [Semiring k] [Add G] :
       Multiplicative.ofAdd with
     toFun := equivMapDomain Multiplicative.ofAdd
     map_mul' := fun x y => by
-      -- Porting note: `dsimp` is required for beta reduction.
-      dsimp only []
+      -- Porting note: added `dsimp only`; `beta_reduce` alone is not sufficient
+      dsimp only
       repeat' rw [equivMapDomain_eq_mapDomain (M := k)]
       dsimp [Multiplicative.ofAdd]
       exact MonoidAlgebra.mapDomain_mul (α := Multiplicative G) (β := k)
@@ -1771,8 +1771,8 @@ protected def MonoidAlgebra.toAdditive [Semiring k] [Mul G] :
   { Finsupp.domCongr Additive.ofMul with
     toFun := equivMapDomain Additive.ofMul
     map_mul' := fun x y => by
-      -- Porting note: `dsimp` is required for beta reduction.
-      dsimp only []
+      -- Porting note: added `dsimp only`; `beta_reduce` alone is not sufficient
+      dsimp only
       repeat' rw [equivMapDomain_eq_mapDomain (M := k)]
       dsimp [Additive.ofMul]
       convert MonoidAlgebra.mapDomain_mul (β := k) (MulHom.id G) x y }
diff --git a/Mathlib/Algebra/Polynomial/Coeff.lean b/Mathlib/Algebra/Polynomial/Coeff.lean
index 27dadc71e11a7..c7bcaaffe48e4 100644
--- a/Mathlib/Algebra/Polynomial/Coeff.lean
+++ b/Mathlib/Algebra/Polynomial/Coeff.lean
@@ -81,8 +81,8 @@ def lsum {R A M : Type*} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R A
   toFun p := p.sum (f · ·)
   map_add' p q := sum_add_index p q _ (fun n => (f n).map_zero) fun n _ _ => (f n).map_add _ _
   map_smul' c p := by
-    -- Porting note: `dsimp only []` is required for beta reduction.
-    dsimp only []
+    -- Porting note: added `dsimp only`; `beta_reduce` alone is not sufficient
+    dsimp only
     rw [sum_eq_of_subset (f · ·) (fun n => (f n).map_zero) (support_smul c p)]
     simp only [sum_def, Finset.smul_sum, coeff_smul, LinearMap.map_smul, RingHom.id_apply]
 #align polynomial.lsum Polynomial.lsum
diff --git a/Mathlib/Computability/TuringMachine.lean b/Mathlib/Computability/TuringMachine.lean
index 3c276a209f84c..584ee9b788cf0 100644
--- a/Mathlib/Computability/TuringMachine.lean
+++ b/Mathlib/Computability/TuringMachine.lean
@@ -2688,11 +2688,10 @@ theorem tr_respects_aux {q v T k} {S : ∀ k, List (Γ k)}
 attribute [local simp] Respects TM2.step TM2.stepAux trNormal
 
 theorem tr_respects : Respects (TM2.step M) (TM1.step (tr M)) TrCfg := by
-  -- Porting note: `simp only`s are required for beta reductions.
+  -- Porting note(#12129): additional beta reduction needed
   intro c₁ c₂ h
   cases' h with l v S L hT
   cases' l with l; · constructor
-  simp only [TM2.step, Respects, Option.map_some']
   rsuffices ⟨b, c, r⟩ : ∃ b, _ ∧ Reaches (TM1.step (tr M)) _ _
   · exact ⟨b, c, TransGen.head' rfl r⟩
   simp only [tr]
@@ -2703,7 +2702,7 @@ theorem tr_respects : Respects (TM2.step M) (TM1.step (tr M)) TrCfg := by
   | H₂ a _ IH => exact IH _ hT
   | H₃ p q₁ q₂ IH₁ IH₂ =>
     unfold TM2.stepAux trNormal TM1.stepAux
-    simp only []
+    beta_reduce
     cases p v <;> [exact IH₂ _ hT; exact IH₁ _ hT]
   | H₄ => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
   | H₅ => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
diff --git a/Mathlib/Data/Finsupp/Basic.lean b/Mathlib/Data/Finsupp/Basic.lean
index 69b7a3113a295..894fd69c2fcf8 100644
--- a/Mathlib/Data/Finsupp/Basic.lean
+++ b/Mathlib/Data/Finsupp/Basic.lean
@@ -881,7 +881,7 @@ def filter (p : α → Prop) [DecidablePred p] (f : α →₀ M) : α →₀ M w
   toFun a := if p a then f a else 0
   support := f.support.filter p
   mem_support_toFun a := by
-    simp only -- Porting note: necessary to beta reduce to activate `split_ifs`
+    beta_reduce -- Porting note(#12129): additional beta reduction needed to activate `split_ifs`
     split_ifs with h <;>
       · simp only [h, mem_filter, mem_support_iff]
         tauto
diff --git a/Mathlib/FieldTheory/RatFunc.lean b/Mathlib/FieldTheory/RatFunc.lean
index 9fad4f7f73d97..802ca652b6f11 100644
--- a/Mathlib/FieldTheory/RatFunc.lean
+++ b/Mathlib/FieldTheory/RatFunc.lean
@@ -607,7 +607,7 @@ def map [MonoidHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap 
     RatFunc.liftOn f
       (fun n d => if h : φ d ∈ S[X]⁰ then ofFractionRing (Localization.mk (φ n) ⟨φ d, h⟩) else 0)
       fun {p q p' q'} hq hq' h => by
-      dsimp only -- Porting note: force the function to be applied
+      beta_reduce -- Porting note(#12129): force the function to be applied
       rw [dif_pos, dif_pos]
       congr 1 -- Porting note: this was a `rw [ofFractionRing.inj_eq]` which was overkill anyway
       rw [Localization.mk_eq_mk_iff]
@@ -617,12 +617,12 @@ def map [MonoidHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap 
       refine' Localization.r_of_eq _
       simpa only [map_mul] using congr_arg φ h
   map_one' := by
-    dsimp only -- Porting note: force the function to be applied
+    beta_reduce -- Porting note(#12129): force the function to be applied
     rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk, dif_pos]
     · simpa using ofFractionRing_one
     · simpa using Submonoid.one_mem _
   map_mul' x y := by
-    dsimp only -- Porting note: force the function to be applied
+    beta_reduce -- Porting note(#12129): force the function to be applied
     cases' x with x; cases' y with y
     -- Porting note: added `using Localization.rec` (`Localization.induction_on` didn't work)
     induction' x using Localization.rec with p q
@@ -699,7 +699,7 @@ def liftMonoidWithZeroHom (φ : R[X] →*₀ G₀) (hφ : R[X]⁰ ≤ G₀⁰.co
       rw [div_eq_div_iff, ← map_mul, mul_comm p, h, map_mul, mul_comm] <;>
         exact nonZeroDivisors.ne_zero (hφ ‹_›)
   map_one' := by
-    dsimp only -- Porting note: force the function to be applied
+    dsimp only -- Porting note: force the function to be applied (not just beta reduction!)
     rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk]
     simp only [map_one, OneMemClass.coe_one, div_one]
   map_mul' x y := by
@@ -712,7 +712,7 @@ def liftMonoidWithZeroHom (φ : R[X] →*₀ G₀) (hφ : R[X]⁰ ≤ G₀⁰.co
     · rfl
     · rfl
   map_zero' := by
-    dsimp only -- Porting note: force the function to be applied
+    beta_reduce -- Porting note(#12129): force the function to be applied
     rw [← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰), liftOn_ofFractionRing_mk]
     simp only [map_zero, zero_div]
 #align ratfunc.lift_monoid_with_zero_hom RatFunc.liftMonoidWithZeroHom
diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean
index 1cb6961b46df3..aa7629ab02243 100644
--- a/Mathlib/GroupTheory/OrderOfElement.lean
+++ b/Mathlib/GroupTheory/OrderOfElement.lean
@@ -42,10 +42,10 @@ variable [Monoid G] {a b x y : G} {n m : ℕ}
 
 section IsOfFinOrder
 
--- Porting note: we need a `dsimp` in the middle of the rewrite to do beta reduction
+-- Porting note(#12129): additional beta reduction needed
 @[to_additive]
 theorem isPeriodicPt_mul_iff_pow_eq_one (x : G) : IsPeriodicPt (x * ·) n 1 ↔ x ^ n = 1 := by
-  rw [IsPeriodicPt, IsFixedPt, mul_left_iterate]; dsimp; rw [mul_one]
+  rw [IsPeriodicPt, IsFixedPt, mul_left_iterate]; beta_reduce; rw [mul_one]
 #align is_periodic_pt_mul_iff_pow_eq_one isPeriodicPt_mul_iff_pow_eq_one
 #align is_periodic_pt_add_iff_nsmul_eq_zero isPeriodicPt_add_iff_nsmul_eq_zero
 
@@ -176,8 +176,8 @@ protected lemma IsOfFinOrder.orderOf_pos (h : IsOfFinOrder x) : 0 < orderOf x :=
 theorem pow_orderOf_eq_one (x : G) : x ^ orderOf x = 1 := by
   -- Porting note: was `convert`, but the `1` in the lemma is equal only after unfolding
   refine Eq.trans ?_ (isPeriodicPt_minimalPeriod (x * ·) 1)
-  -- Porting note: we need a `dsimp` in the middle of the rewrite to do beta reduction
-  rw [orderOf, mul_left_iterate]; dsimp; rw [mul_one]
+  -- Porting note(#12129): additional beta reduction needed in the middle of the rewrite
+  rw [orderOf, mul_left_iterate]; beta_reduce; rw [mul_one]
 #align pow_order_of_eq_one pow_orderOf_eq_one
 #align add_order_of_nsmul_eq_zero addOrderOf_nsmul_eq_zero
 
diff --git a/Mathlib/GroupTheory/Transfer.lean b/Mathlib/GroupTheory/Transfer.lean
index cc72434a3997d..42fd3076210f0 100644
--- a/Mathlib/GroupTheory/Transfer.lean
+++ b/Mathlib/GroupTheory/Transfer.lean
@@ -100,7 +100,9 @@ the transfer homomorphism is `transfer ϕ : G →+ A`."]
 noncomputable def transfer [FiniteIndex H] : G →* A :=
   let T : leftTransversals (H : Set G) := Inhabited.default
   { toFun := fun g => diff ϕ T (g • T)
-    map_one' := by simp only; rw [one_smul, diff_self] -- Porting note: added `simp only`
+    -- Porting note(#12129): additional beta reduction needed
+    map_one' := by beta_reduce; rw [one_smul, diff_self]
+    -- Porting note: added `simp only` (not just beta reduction)
     map_mul' := fun g h => by simp only; rw [mul_smul, ← diff_mul_diff, smul_diff_smul] }
 #align monoid_hom.transfer MonoidHom.transfer
 #align add_monoid_hom.transfer AddMonoidHom.transfer
diff --git a/Mathlib/LinearAlgebra/Basis.lean b/Mathlib/LinearAlgebra/Basis.lean
index ffde667cc0324..8d176c4eaae48 100644
--- a/Mathlib/LinearAlgebra/Basis.lean
+++ b/Mathlib/LinearAlgebra/Basis.lean
@@ -313,8 +313,8 @@ theorem repr_apply_eq (f : M → ι → R) (hadd : ∀ x y, f (x + y) = f x + f
     (x : M) (i : ι) : b.repr x i = f x i := by
   let f_i : M →ₗ[R] R :=
     { toFun := fun x => f x i
-      -- Porting note: `dsimp only []` is required for beta reduction.
-      map_add' := fun _ _ => by dsimp only []; rw [hadd, Pi.add_apply]
+      -- Porting note(#12129): additional beta reduction needed
+      map_add' := fun _ _ => by beta_reduce; rw [hadd, Pi.add_apply]
       map_smul' := fun _ _ => by simp [hsmul, Pi.smul_apply] }
   have : Finsupp.lapply i ∘ₗ ↑b.repr = f_i := by
     refine' b.ext fun j => _
diff --git a/Mathlib/LinearAlgebra/LinearPMap.lean b/Mathlib/LinearAlgebra/LinearPMap.lean
index ce5620e175b49..4df55565ca7dd 100644
--- a/Mathlib/LinearAlgebra/LinearPMap.lean
+++ b/Mathlib/LinearAlgebra/LinearPMap.lean
@@ -123,17 +123,17 @@ noncomputable def mkSpanSingleton' (x : E) (y : F) (H : ∀ c : R, c • x = 0 
       rw [← sub_eq_zero, ← sub_smul] at h ⊢
       exact H _ h
     { toFun := fun z => Classical.choose (mem_span_singleton.1 z.prop) • y
-      -- Porting note: `dsimp only []` are required.
+      -- Porting note(#12129): additional beta reduction needed
       -- Porting note: Were `Classical.choose_spec (mem_span_singleton.1 _)`.
       map_add' := fun y z => by
-        dsimp only []
+        beta_reduce
         rw [← add_smul]
         apply H
         simp only [add_smul, sub_smul,
           fun w : R ∙ x => Classical.choose_spec (mem_span_singleton.1 w.prop)]
         apply coe_add
       map_smul' := fun c z => by
-        dsimp only []
+        beta_reduce
         rw [smul_smul]
         apply H
         simp only [mul_smul,
diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean
index 81f8adc2b2611..f608fb935538e 100644
--- a/Mathlib/MeasureTheory/PiSystem.lean
+++ b/Mathlib/MeasureTheory/PiSystem.lean
@@ -670,11 +670,11 @@ theorem ofMeasurableSpace_toMeasurableSpace
 
 /-- If `s` is in a Dynkin system `d`, we can form the new Dynkin system `{s ∩ t | t ∈ d}`. -/
 def restrictOn {s : Set α} (h : d.Has s) : DynkinSystem α where
-  -- Porting note: `simp only []` required for a beta reduction
+  -- Porting note(#12129): additional beta reduction needed
   Has t := d.Has (t ∩ s)
   has_empty := by simp [d.has_empty]
   has_compl {t} hts := by
-    simp only []
+    beta_reduce
     have : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ := Set.ext fun x => by by_cases h : x ∈ s <;> simp [h]
     rw [this]
     exact
diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 453b9b7575bfd..cfca3760b5d64 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -223,7 +223,7 @@ def lift (h : IsAdjoinRoot S f) : S →+* T where
     rw [h.eval₂_repr_eq_eval₂_of_map_eq hx _ (h.repr z + h.repr w), eval₂_add]
     · rw [map_add, map_repr, map_repr]
   map_one' := by
-    dsimp only -- Porting note (#10752): added `dsimp only`
+    beta_reduce -- Porting note (#12129): additional beta reduction needed
     rw [h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ (map_one _), eval₂_one]
   map_mul' z w := by
     dsimp only -- Porting note (#10752): added `dsimp only`
@@ -371,7 +371,7 @@ def modByMonicHom (h : IsAdjoinRootMonic S f) : S →ₗ[R] R[X] where
   map_add' x y := by
     conv_lhs =>
       rw [← h.map_repr x, ← h.map_repr y, ← map_add]
-      dsimp only -- Porting note (#10752): added `dsimp only`
+      beta_reduce -- Porting note (#12129): additional beta reduction needed
       rw [h.modByMonic_repr_map, add_modByMonic]
   map_smul' c x := by
     rw [RingHom.id_apply, ← h.map_repr x, Algebra.smul_def, h.algebraMap_apply, ← map_mul]
@@ -446,7 +446,7 @@ def basis (h : IsAdjoinRootMonic S f) : Basis (Fin (natDegree f)) R S :=
         rintro i rfl
         exact i.prop.not_le hm
       map_add' := fun x y => by
-        dsimp only -- Porting note (#10752): added `dsimp only`
+        beta_reduce -- Porting note (#12129): additional beta reduction needed
         rw [map_add, toFinsupp_add, Finsupp.comapDomain_add_of_injective Fin.val_injective]
       -- Porting note: the original simp proof with the same lemmas does not work
       -- See https://github.com/leanprover-community/mathlib4/issues/5026
diff --git a/Mathlib/RingTheory/OreLocalization/Basic.lean b/Mathlib/RingTheory/OreLocalization/Basic.lean
index f7dedcac2ad46..5edf082108fdb 100644
--- a/Mathlib/RingTheory/OreLocalization/Basic.lean
+++ b/Mathlib/RingTheory/OreLocalization/Basic.lean
@@ -378,21 +378,22 @@ variable (hf : ∀ s : S, f s = fS s)
 
 /-- The universal lift from a morphism `R →* T`, which maps elements of `S` to units of `T`,
 to a morphism `R[S⁻¹] →* T`. -/
-def universalMulHom : R[S⁻¹] →* T
-    where
-  -- Porting note: `simp only []` required for beta reductions
+def universalMulHom : R[S⁻¹] →* T where
+  -- Porting note(#12129): additional beta reduction needed
   toFun x :=
     x.liftExpand (fun r s => f r * ((fS s)⁻¹ : Units T)) fun r t s ht => by
-      simp only []
+      beta_reduce
       have : (fS ⟨s * t, ht⟩ : T) = fS s * f t := by
         simp only [← hf, MonoidHom.map_mul]
       conv_rhs =>
         rw [MonoidHom.map_mul, ← mul_one (f r), ← Units.val_one, ← mul_left_inv (fS s)]
         rw [Units.val_mul, ← mul_assoc, mul_assoc _ (fS s : T), ← this, mul_assoc]
       simp only [mul_one, Units.mul_inv]
-  map_one' := by simp only []; rw [OreLocalization.one_def, liftExpand_of]; simp
+  map_one' := by beta_reduce; rw [OreLocalization.one_def, liftExpand_of]; simp
   map_mul' x y := by
-    simp only []
+    -- Porting note: `simp only []` required, not just for beta reductions
+    beta_reduce
+    simp only [] -- TODO more!
     induction' x using OreLocalization.ind with r₁ s₁
     induction' y using OreLocalization.ind with r₂ s₂
     rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'
@@ -822,8 +823,8 @@ variable {R : Type*} [Ring R] {S : Submonoid R} [OreSet S]
 /-- Negation on the Ore localization is defined via negation on the numerator. -/
 protected def neg : R[S⁻¹] → R[S⁻¹] :=
   liftExpand (fun (r : R) (s : S) => -r /ₒ s) fun r t s ht => by
-    -- Porting note: `simp only []` required for beta reductions
-    simp only []
+    -- Porting note(#12129): additional beta reduction needed
+    beta_reduce
     rw [neg_mul_eq_neg_mul, ← OreLocalization.expand]
 #align ore_localization.neg OreLocalization.neg
 
diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
index a13c89cc1caee..498cb3bb26225 100644
--- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean
+++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
@@ -803,9 +803,9 @@ theorem mul_le_of_limit {a b c : Ordinal} (h : IsLimit b) : a * b ≤ c ↔ ∀
 #align ordinal.mul_le_of_limit Ordinal.mul_le_of_limit
 
 theorem mul_isNormal {a : Ordinal} (h : 0 < a) : IsNormal (a * ·) :=
-  -- Porting note: `dsimp only` is required for beta reduction.
+  -- Porting note(#12129): additional beta reduction needed
   ⟨fun b => by
-      dsimp only
+      beta_reduce
       rw [mul_succ]
       simpa only [add_zero] using (add_lt_add_iff_left (a * b)).2 h,
     fun b l c => mul_le_of_limit l⟩
diff --git a/Mathlib/Topology/Gluing.lean b/Mathlib/Topology/Gluing.lean
index 59676e93a27e6..0826d1b1a3897 100644
--- a/Mathlib/Topology/Gluing.lean
+++ b/Mathlib/Topology/Gluing.lean
@@ -389,8 +389,8 @@ def mk' (h : MkCore.{u}) : TopCat.GlueData where
   V i := (Opens.toTopCat _).obj (h.V i.1 i.2)
   f i j := (h.V i j).inclusion
   f_id i := by
-    -- Porting note (#10752): added `dsimp only`
-    dsimp only
+    -- Porting note (#12129): additional beta reduction needed
+    beta_reduce
     exact (h.V_id i).symm ▸ IsIso.of_iso (Opens.inclusionTopIso (h.U i))
   f_open := fun i j : h.J => (h.V i j).openEmbedding
   t := h.t