chore: adaptations for nightly-2024-02-01

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -491,7 +491,7 @@ end CategoryTheory.Aut
 instance GroupCat.forget_reflects_isos : ReflectsIsomorphisms (forget GroupCat.{u}) where
   reflects {X Y} f _ := by
     let i := asIso ((forget GroupCat).map f)
-    let e : X ≃* Y := { i.toEquiv with map_mul' := by aesop }
+    let e : X ≃* Y := { i.toEquiv with map_mul' := map_mul _ }
     exact IsIso.of_iso e.toGroupCatIso
 set_option linter.uppercaseLean3 false in
 #align Group.forget_reflects_isos GroupCat.forget_reflects_isos
@@ -502,7 +502,7 @@ set_option linter.uppercaseLean3 false in
 instance CommGroupCat.forget_reflects_isos : ReflectsIsomorphisms (forget CommGroupCat.{u}) where
   reflects {X Y} f _ := by
     let i := asIso ((forget CommGroupCat).map f)
-    let e : X ≃* Y := { i.toEquiv with map_mul' := by aesop }
+    let e : X ≃* Y := { i.toEquiv with map_mul' := map_mul _}
     exact IsIso.of_iso e.toCommGroupCatIso
 set_option linter.uppercaseLean3 false in
 #align CommGroup.forget_reflects_isos CommGroupCat.forget_reflects_isos

Mathlib/Algebra/DirectSum/Basic.lean

@@ -309,7 +309,7 @@ variable {α : Option ι → Type w} [∀ i, AddCommMonoid (α i)]
 -- include dec_ι
 
 /-- Isomorphism obtained by separating the term of index `none` of a direct sum over `Option ι`.-/
-@[simps]
+@[simps!]
 noncomputable def addEquivProdDirectSum : (⨁ i, α i) ≃+ α none × ⨁ i, α (some i) :=
   { DFinsupp.equivProdDFinsupp with map_add' := DFinsupp.equivProdDFinsupp_add }
 #align direct_sum.add_equiv_prod_direct_sum DirectSum.addEquivProdDirectSum

Mathlib/Algebra/Group/Equiv/TypeTags.lean

@@ -109,14 +109,14 @@ abbrev MulEquiv.toAdditive'' [AddZeroClass G] [MulOneClass H] :
 
 /-- Multiplicative equivalence between multiplicative endomorphisms of a `MulOneClass` `M`
 and additive endomorphisms of `Additive M`. -/
-@[simps] def monoidEndToAdditive (M : Type*) [MulOneClass M] :
+@[simps!] def monoidEndToAdditive (M : Type*) [MulOneClass M] :
     Monoid.End M ≃* AddMonoid.End (Additive M) :=
   { MonoidHom.toAdditive with
     map_mul' := fun _ _ => rfl }
 
 /-- Multiplicative equivalence between additive endomorphisms of an `AddZeroClass` `A`
 and multiplicative endomorphisms of `Multiplicative A`. -/
-@[simps] def addMonoidEndToMultiplicative (A : Type*) [AddZeroClass A] :
+@[simps!] def addMonoidEndToMultiplicative (A : Type*) [AddZeroClass A] :
     AddMonoid.End A ≃* Monoid.End (Multiplicative A) :=
   { AddMonoidHom.toMultiplicative with
     map_mul' := fun _ _ => rfl }

Mathlib/Algebra/Lie/Subalgebra.lean

@@ -193,7 +193,6 @@ theorem mk_coe (S : Set L) (h₁ h₂ h₃ h₄) :
   rfl
 #align lie_subalgebra.mk_coe LieSubalgebra.mk_coe
 
-@[simp]
 theorem coe_to_submodule_mk (p : Submodule R L) (h) :
     (({ p with lie_mem' := h } : LieSubalgebra R L) : Submodule R L) = p := by
   cases p

Mathlib/Algebra/Lie/Submodule.lean

@@ -128,7 +128,6 @@ theorem coe_toSet_mk (S : Set M) (h₁ h₂ h₃ h₄) :
   rfl
 #align lie_submodule.coe_to_set_mk LieSubmodule.coe_toSet_mk
 
-@[simp]
 theorem coe_toSubmodule_mk (p : Submodule R M) (h) :
     (({ p with lie_mem := h } : LieSubmodule R L M) : Submodule R M) = p := by cases p; rfl
 #align lie_submodule.coe_to_submodule_mk LieSubmodule.coe_toSubmodule_mk

Mathlib/Algebra/Lie/Weights/Linear.lean

@@ -76,13 +76,13 @@ instance instLinearWeightsOfIsLieAbelian [IsLieAbelian L] [NoZeroSMulDivisors R
       rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, LieHom.map_zero]
     intro χ hχ x y
     simp_rw [Ne.def, ← LieSubmodule.coe_toSubmodule_eq_iff, weightSpace, weightSpaceOf,
-      LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule, Submodule.eta] at hχ
+      LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule] at hχ
     exact Module.End.map_add_of_iInf_generalizedEigenspace_ne_bot_of_commute
       (toEndomorphism R L M).toLinearMap χ hχ h x y
   { map_add := aux
     map_smul := fun χ hχ t x ↦ by
       simp_rw [Ne.def, ← LieSubmodule.coe_toSubmodule_eq_iff, weightSpace, weightSpaceOf,
-        LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule, Submodule.eta] at hχ
+        LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule] at hχ
       exact Module.End.map_smul_of_iInf_generalizedEigenspace_ne_bot
         (toEndomorphism R L M).toLinearMap χ hχ t x
     map_lie := fun χ hχ t x ↦ by

Mathlib/Algebra/Module/Injective.lean

@@ -187,7 +187,6 @@ def ExtensionOf.max {c : Set (ExtensionOf i f)} (hchain : IsChain (· ≤ ·) c)
       -- porting note: this subgoal didn't exist before the reenableeta branch
       -- follow-up note: the subgoal was moved from after `refine'` in `is_extension` to here
       -- after the behavior of `refine'` changed.
-      exact (IsChain.directedOn <| chain_linearPMap_of_chain_extensionOf hchain)
     is_extension := fun m => by
       refine' Eq.trans (hnonempty.some.is_extension m) _
       symm

Mathlib/Algebra/Order/WithZero.lean

@@ -281,8 +281,10 @@ theorem OrderIso.mulRight₀'_symm {a : α} (ha : a ≠ 0) :
   rfl
 #align order_iso.mul_right₀'_symm OrderIso.mulRight₀'_symm
 
+set_option synthInstance.maxHeartbeats 0 in
+set_option maxHeartbeats 0 in
 instance : LinearOrderedAddCommGroupWithTop (Additive αᵒᵈ) :=
   { Additive.subNegMonoid, instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual,
     Additive.instNontrivial with
     neg_top := @inv_zero _ (_)
-    add_neg_cancel := fun a ha ↦ mul_inv_cancel (id ha : Additive.toMul a ≠ 0) }
+    add_neg_cancel := fun a ha ↦ mul_inv_cancel (G₀ := α) (id ha : Additive.toMul a ≠ 0) }

Mathlib/Algebra/Ring/Pi.lean

@@ -134,7 +134,7 @@ variable {I : Type u}
 
 /-- Evaluation of functions into an indexed collection of non-unital rings at a point is a
 non-unital ring homomorphism. This is `Function.eval` as a `NonUnitalRingHom`. -/
-@[simps]
+@[simps!]
 def Pi.evalNonUnitalRingHom (f : I → Type v) [∀ i, NonUnitalNonAssocSemiring (f i)] (i : I) :
     (∀ i, f i) →ₙ+* f i :=
   { Pi.evalMulHom f i, Pi.evalAddMonoidHom f i with }

Mathlib/Analysis/NormedSpace/AffineIsometry.lean

@@ -876,7 +876,7 @@ namespace AffineSubspace
 /-- An affine subspace is isomorphic to its image under an injective affine map.
 This is the affine version of `Submodule.equivMapOfInjective`.
 -/
-@[simps]
+@[simps linear, simps! toFun]
 noncomputable def equivMapOfInjective (E : AffineSubspace 𝕜 P₁) [Nonempty E] (φ : P₁ →ᵃ[𝕜] P₂)
     (hφ : Function.Injective φ) : E ≃ᵃ[𝕜] E.map φ :=
   { Equiv.Set.image _ (E : Set P₁) hφ with

Mathlib/CategoryTheory/Monad/EquivMon.lean

@@ -95,11 +95,11 @@ def monToMonad : Mon_ (C ⥤ C) ⥤ Monad C where
         erw [← NatTrans.comp_app, f.one_hom]
         rfl
       app_μ := by
-        intro Z
+        intro z
         erw [← NatTrans.comp_app, f.mul_hom]
         dsimp
-        simp only [NatTrans.naturality, NatTrans.hcomp_app, assoc, NatTrans.comp_app,
-          ofMon_μ] }
+        simp only [Category.assoc, NatTrans.naturality, ofMon_obj]
+        rfl }
 #align category_theory.Monad.Mon_to_Monad CategoryTheory.Monad.monToMonad
 
 /-- Oh, monads are just monoids in the category of endofunctors (equivalence of categories). -/

Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean

@@ -112,7 +112,7 @@ section
 variable [Preadditive C] [HasFiniteBiproducts C]
 
 /-- `HomOrthogonal.matrixDecomposition` as an additive equivalence. -/
-@[simps]
+@[simps!]
 noncomputable def matrixDecompositionAddEquiv (o : HomOrthogonal s) {α β : Type} [Fintype α]
     [Fintype β] {f : α → ι} {g : β → ι} :
     ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃+

Mathlib/Combinatorics/Composition.lean

@@ -801,7 +801,7 @@ def compositionAsSetEquiv (n : ℕ) : CompositionAsSet n ≃ Finset (Fin (n - 1)
     · simp only [or_iff_not_imp_left]
       intro i_mem i_ne_zero i_ne_last
       simp? [Fin.ext_iff] at i_ne_zero i_ne_last says
-        simp only [Fin.isValue, Fin.ext_iff, Fin.val_zero, Fin.val_last] at i_ne_zero i_ne_last
+        simp only [Fin.ext_iff, Fin.val_zero, Fin.val_last] at i_ne_zero i_ne_last
       have A : (1 + (i - 1) : ℕ) = (i : ℕ) := by
         rw [add_comm]
         exact Nat.succ_pred_eq_of_pos (pos_iff_ne_zero.mpr i_ne_zero)

Mathlib/Data/MvPolynomial/Expand.lean

@@ -55,6 +55,7 @@ theorem expand_monomial (p : ℕ) (d : σ →₀ ℕ) (r : R) :
 theorem expand_one_apply (f : MvPolynomial σ R) : expand 1 f = f := by
   simp only [expand, pow_one, eval₂Hom_eq_bind₂, bind₂_C_left, RingHom.toMonoidHom_eq_coe,
     RingHom.coe_monoidHom_id, AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.id_apply]
+  rfl
 #align mv_polynomial.expand_one_apply MvPolynomial.expand_one_apply
 
 @[simp]

Mathlib/Data/Sign.lean

@@ -373,6 +373,7 @@ theorem sign_nonneg_iff : 0 ≤ sign a ↔ 0 ≤ a := by
   · simp [h, h.le]
   · simp [← h]
   · simp [h, h.not_le]
+
 #align sign_nonneg_iff sign_nonneg_iff
 
 @[simp]

Mathlib/Lean/Meta/Simp.lean

@@ -160,18 +160,18 @@ convert `e` into that simplified type, using a combination of type hints and `Eq
 -/
 def simpType (S : Expr → MetaM Simp.Result) (e : Expr) : MetaM Expr := do
   match (← S (← inferType e)) with
-  | ⟨ty', none, _⟩ => mkExpectedTypeHint e ty'
+  | ⟨ty', none, _, _⟩ => mkExpectedTypeHint e ty'
   -- We use `mkExpectedTypeHint` in this branch as well, in order to preserve the binder types.
-  | ⟨ty', some prf, _⟩ => mkExpectedTypeHint (← mkEqMP prf e) ty'
+  | ⟨ty', some prf, _, _⟩ => mkExpectedTypeHint (← mkEqMP prf e) ty'
 
 /-- Independently simplify both the left-hand side and the right-hand side
 of an equality. The equality is allowed to be under binders.
 Returns the simplified equality and a proof of it. -/
 def simpEq (S : Expr → MetaM Simp.Result) (type pf : Expr) : MetaM (Expr × Expr) := do
   forallTelescope type fun fvars type => do
     let .app (.app (.app (.const `Eq [u]) α) lhs) rhs := type | throwError "simpEq expecting Eq"
-    let ⟨lhs', lhspf?, _⟩ ← S lhs
-    let ⟨rhs', rhspf?, _⟩ ← S rhs
+    let ⟨lhs', lhspf?, _, _⟩ ← S lhs
+    let ⟨rhs', rhspf?, _, _⟩ ← S rhs
     let mut pf' := mkAppN pf fvars
     if let some lhspf := lhspf? then
       pf' ← mkEqTrans (← mkEqSymm lhspf) pf'

Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean

@@ -255,7 +255,9 @@ theorem coe_toEven_reverse_involute (x : CliffordAlgebra Q) :
     simp only [involute_ι, Subalgebra.coe_neg, toEven_ι, reverse.map_mul, reverse_v, reverse_e0,
       reverse_ι, neg_e0_mul_v, map_neg]
   | h_mul x y hx hy => simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy]
-  | h_add x y hx hy => simp only [map_add, Subalgebra.coe_add, hx, hy]
+  | h_add x y hx hy =>
+    repeat (rw [map_add])
+    simp only [map_add, Subalgebra.coe_add, hx, hy]
 #align clifford_algebra.coe_to_even_reverse_involute CliffordAlgebra.coe_toEven_reverse_involute
 
 /-! ### Constructions needed for `CliffordAlgebra.evenEquivEvenNeg` -/

Mathlib/LinearAlgebra/Projectivization/Subspace.lean

@@ -133,8 +133,7 @@ instance instInfSet : InfSet (Subspace K V) :=
 
 /-- The subspaces of a projective space form a complete lattice. -/
 instance : CompleteLattice (Subspace K V) :=
-  { (inferInstance : Inf (Subspace K V)),
-    completeLatticeOfInf (Subspace K V)
+  { completeLatticeOfInf (Subspace K V)
       (by
         refine fun s => ⟨fun a ha x hx => hx _ ⟨a, ha, rfl⟩, fun a ha x hx E => ?_⟩
         rintro ⟨E, hE, rfl⟩

Mathlib/NumberTheory/LucasLehmer.lean

@@ -153,7 +153,7 @@ theorem residue_eq_zero_iff_sMod_eq_zero (p : ℕ) (w : 1 < p) :
     intro h
     simp? [ZMod.int_cast_zmod_eq_zero_iff_dvd] at h says
       simp only [ZMod.int_cast_zmod_eq_zero_iff_dvd, gt_iff_lt, zero_lt_two, pow_pos, cast_pred,
-        cast_pow, cast_ofNat, Int.isPosValue] at h
+        cast_pow, cast_ofNat] at h
     apply Int.eq_zero_of_dvd_of_nonneg_of_lt _ _ h <;> clear h
     · exact sMod_nonneg _ (by positivity) _
     · exact sMod_lt _ (by positivity) _
@@ -426,7 +426,7 @@ theorem ω_pow_formula (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) :
   rw [sZMod_eq_s p'] at h
   simp? [ZMod.int_cast_zmod_eq_zero_iff_dvd] at h says
     simp only [add_tsub_cancel_right, ZMod.int_cast_zmod_eq_zero_iff_dvd, gt_iff_lt, zero_lt_two,
-      pow_pos, cast_pred, cast_pow, cast_ofNat, Int.isPosValue] at h
+      pow_pos, cast_pred, cast_pow, cast_ofNat] at h
   cases' h with k h
   use k
   replace h := congr_arg (fun n : ℤ => (n : X (q (p' + 2)))) h

Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean

@@ -102,6 +102,6 @@ noncomputable instance hilbert90 : Unique (H1 (Rep.ofAlgebraAutOnUnits K L)) whe
     refine' Additive.toMul.bijective.1 _
     show Units.map g β⁻¹ / β⁻¹ = Additive.toMul (x.1 g)
     rw [map_inv, div_inv_eq_mul, mul_comm]
-    exact mul_inv_eq_iff_eq_mul.2 (hβ g).symm
+    apply mul_inv_eq_iff_eq_mul.2 (hβ g).symm
 
 end groupCohomology

Mathlib/RingTheory/DedekindDomain/Ideal.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2020 Kenji Nakagawa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenji Nakagawa, Anne Baanen, Filippo A. E. Nuccio
@@ -598,9 +598,9 @@
 -- Porting note: added noncomputable because otherwise it fails, so it seems that the goal
 -- is not achieved...
 noncomputable instance FractionalIdeal.cancelCommMonoidWithZero :
-    CancelCommMonoidWithZero (FractionalIdeal A⁰ K) :=
-  { @FractionalIdeal.commSemiring A _ A⁰ K _ _,  -- Project out the computable fields first.
-    (by infer_instance : CancelCommMonoidWithZero (FractionalIdeal A⁰ K)) with }
+    CancelCommMonoidWithZero (FractionalIdeal A⁰ K) := inferInstance
+  -- { @FractionalIdeal.commSemiring A _ A⁰ K _ _,  -- Project out the computable fields first.
+  --   (by infer_instance : CancelCommMonoidWithZero (FractionalIdeal A⁰ K)) with }
 #align fractional_ideal.cancel_comm_monoid_with_zero FractionalIdeal.cancelCommMonoidWithZero
 
 instance Ideal.cancelCommMonoidWithZero : CancelCommMonoidWithZero (Ideal A) :=

Mathlib/RingTheory/HahnSeries.lean

@@ -389,7 +389,7 @@ theorem min_order_le_order_add {Γ} [Zero Γ] [LinearOrder Γ] {x y : HahnSeries
 #align hahn_series.min_order_le_order_add HahnSeries.min_order_le_order_add
 
 /-- `single` as an additive monoid/group homomorphism -/
-@[simps]
+@[simps!]
 def single.addMonoidHom (a : Γ) : R →+ HahnSeries Γ R :=
   { single a with
     map_add' := fun x y => by

Mathlib/RingTheory/Valuation/ValuationSubring.lean

@@ -385,7 +385,7 @@ def primeSpectrumEquiv : PrimeSpectrum A ≃ {S // A ≤ S} where
 #align valuation_subring.prime_spectrum_equiv ValuationSubring.primeSpectrumEquiv
 
 /-- An ordered variant of `primeSpectrumEquiv`. -/
-@[simps]
+@[simps!]
 def primeSpectrumOrderEquiv : (PrimeSpectrum A)ᵒᵈ ≃o {S // A ≤ S} :=
   { primeSpectrumEquiv A with
     map_rel_iff' :=

Mathlib/Tactic/Abel.lean

@@ -299,7 +299,7 @@ lemma subst_into_negg {α} [AddCommGroup α] (a ta t : α)
 def evalSMul' (eval : Expr → M (NormalExpr × Expr))
     (is_smulg : Bool) (orig e₁ e₂ : Expr) : M (NormalExpr × Expr) := do
   trace[abel] "Calling NormNum on {e₁}"
-  let ⟨e₁', p₁, _⟩ ← try Meta.NormNum.eval e₁ catch _ => pure { expr := e₁ }
+  let ⟨e₁', p₁, _, _⟩ ← try Meta.NormNum.eval e₁ catch _ => pure { expr := e₁ }
   let p₁ ← p₁.getDM (mkEqRefl e₁')
   match e₁'.int? with
   | some n => do
@@ -442,7 +442,7 @@ partial def abelNFCore
     let thms := [``term_eq, ``termg_eq, ``add_zero, ``one_nsmul, ``one_zsmul, ``zsmul_zero]
     let ctx' := { ctx with simpTheorems := #[← thms.foldlM (·.addConst ·) {:_}] }
     pure fun r' : Simp.Result ↦ do
-      Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := ← Lean.Meta.Simp.mkDefaultMethods)).1
+      r'.mkEqTrans (← Simp.main r'.expr ctx' (methods := ← Lean.Meta.Simp.mkDefaultMethods)).1
   let rec
     /-- The recursive case of `abelNF`.
     * `root`: true when the function is called directly from `abelNFCore`
@@ -452,7 +452,7 @@ partial def abelNFCore
       `go -> eval -> evalAtom -> go` which makes no progress.
     -/
     go root parent :=
-      let pre e :=
+      let pre : Simp.Simproc := fun e =>
         try
           guard <| root || parent != e -- recursion guard
           let e ← withReducible <| whnf e
@@ -462,8 +462,8 @@ partial def abelNFCore
           let r ← simp { expr := a, proof? := pa }
           if ← withReducible <| isDefEq r.expr e then return .done { expr := r.expr }
           pure (.done r)
-        catch _ => pure <| .visit { expr := e }
-      let post := (Simp.postDefault · fun _ ↦ none)
+        catch _ => pure <| .continue
+      let post : Simp.Simproc := Simp.postDefault #[]
       (·.1) <$> Simp.main parent ctx (methods := { pre, post }),
     /-- The `evalAtom` implementation passed to `eval` calls `go` if `cfg.recursive` is true,
     and does nothing otherwise. -/

Mathlib/Tactic/Attr/Register.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Lean.Meta.Tactic.Simp.SimpTheorems
+import Lean.Meta.Tactic.Simp.RegisterCommand
 import Std.Tactic.LabelAttr
 
 /-!

Mathlib/Tactic/DeriveTraversable.lean

@@ -427,7 +427,7 @@ def traversableDeriveHandler : DerivingHandlerNoArgs :=
 initialize registerDerivingHandler ``Traversable traversableDeriveHandler
 
 /-- Simplify the goal `m` using `functor_norm`. -/
-def simpFunctorGoal (m : MVarId) (s : Simp.Context) (simprocs : Simprocs := {})
+def simpFunctorGoal (m : MVarId) (s : Simp.Context) (simprocs : Simp.SimprocsArray := {})
     (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
     (usedSimps : Simp.UsedSimps := {}) :

Mathlib/Tactic/FieldSimp.lean

@@ -71,8 +71,8 @@ partial def discharge (prop : Expr) : SimpM (Option Expr) :=
     --   2) mathlib3 norm_num1 is able to handle any needed discharging, or
     --   3) some other reason?
     let ⟨simpResult, usedTheorems'⟩ ←
-      simp prop { ctx with dischargeDepth := ctx.dischargeDepth + 1 } (← Simp.getSimprocs) discharge
-        usedTheorems
+      simp prop { ctx with dischargeDepth := ctx.dischargeDepth + 1 } #[(← Simp.getSimprocs)]
+        discharge usedTheorems
     set {(← get) with usedTheorems := usedTheorems'}
     if simpResult.expr.isConstOf ``True then
       try

Mathlib/Tactic/NormNum/Core.lean

@@ -189,10 +189,12 @@ initialize registerBuiltinAttribute {
     modifyEnv fun env => normNumExt.modifyState env fun _ => s
 }
 
-/-- A simp plugin which calls `NormNum.eval`. -/
-def tryNormNum? (post := false) (e : Expr) : SimpM (Option Simp.Step) := do
-  try return some (.done (← eval e post))
-  catch _ => return none
+/-- A simplifier step for `norm_num`. -/
+def tryNormNum (post := false) (e : Expr) : SimpM Simp.Step := do
+  try
+    return .done (← eval e post)
+  catch _ =>
+    return .continue
 
 variable (ctx : Simp.Context) (useSimp := true) in
 mutual
@@ -202,14 +204,12 @@ mutual
   /-- A `Methods` implementation which calls `norm_num`. -/
   partial def methods : Simp.Methods :=
     if useSimp then {
-      pre := fun e ↦ do
-        Simp.andThen (← Simp.preDefault e discharge) tryNormNum?
-      post := fun e ↦ do
-        Simp.andThen (← Simp.postDefault e discharge) (tryNormNum? (post := true))
+      pre := Simp.preDefault #[] >> tryNormNum
+      post := Simp.postDefault #[] >> tryNormNum (post := true)
       discharge? := discharge
     } else {
-      pre := fun e ↦ Simp.andThen (.visit { expr := e }) tryNormNum?
-      post := fun e ↦ Simp.andThen (.visit { expr := e }) (tryNormNum? (post := true))
+      pre := tryNormNum
+      post := tryNormNum (post := true)
       discharge? := discharge
     }
 

Mathlib/Tactic/PushNeg.lean

@@ -69,7 +69,7 @@ def transformNegationStep (e : Expr) : SimpM (Option Simp.Step) := do
       return some <| mkSimpStep rhs thm
     catch _ => return none
   let e_whnf ← whnfR e
-  let some ex := e_whnf.not? | return Simp.Step.visit { expr := e }
+  let some ex := e_whnf.not? | return Simp.Step.continue
   let ex := (← instantiateMVars ex).cleanupAnnotations
   match ex.getAppFnArgs with
   | (``Not, #[e]) =>
@@ -126,12 +126,12 @@ def transformNegationStep (e : Expr) : SimpM (Option Simp.Step) := do
 /-- Recursively push negations at the top level of the current expression. This is needed
 to handle e.g. triple negation. -/
 partial def transformNegation (e : Expr) : SimpM Simp.Step := do
-  let Simp.Step.visit r₁ ← transformNegationStep e | return Simp.Step.visit { expr := e }
+  let Simp.Step.visit r₁ ← transformNegationStep e | return Simp.Step.continue
   match r₁.proof? with
-  | none => return Simp.Step.visit r₁
+  | none => return Simp.Step.continue r₁
   | some _ => do
       let Simp.Step.visit r₂ ← transformNegation r₁.expr | return Simp.Step.visit r₁
-      return Simp.Step.visit (← Simp.mkEqTrans r₁ r₂)
+      return Simp.Step.visit (← r₁.mkEqTrans r₂)
 
 /-- Common entry point to `push_neg` as a conv. -/
 def pushNegCore (tgt : Expr) : MetaM Simp.Result := do