remove TODO

stage2 can be compiled without issues.

src/Init/Control/Lawful/Instances.lean

@@ -469,13 +469,13 @@ namespace EStateM
 
 instance : LawfulMonad (EStateM ε σ) := .mk'
   (id_map := fun x => funext <| fun s => by
-    dsimp only [EStateM.instMonad, EStateM.map]
+    simp only [Functor.map, EStateM.map]
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)
   (pure_bind := fun _ _ => by rfl)
   (bind_assoc := fun x _ _ => funext <| fun s => by
-    dsimp only [EStateM.instMonad, EStateM.bind]
+    simp only [bind, EStateM.bind]
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)

src/Init/Data/List/Lex.lean

@@ -85,7 +85,7 @@ theorem cons_lex_cons_iff : Lex r (a :: l₁) (b :: l₂) ↔ r a b ∨ a = b
 
 theorem cons_lt_cons_iff [LT α] {a b} {l₁ l₂ : List α} :
     (a :: l₁) < (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ < l₂ := by
-  dsimp only [instLT, List.lt]
+  simp only [LT.lt, List.lt]
   simp [cons_lex_cons_iff]
 
 @[simp] theorem cons_lt_cons_self [LT α] [i₀ : Std.Irrefl (· < · : α → α → Prop)] {l₁ l₂ : List α} :
@@ -101,7 +101,7 @@ theorem cons_le_cons_iff [LT α]
     [i₂ : Std.Trichotomous (· < · : α → α → Prop)]
     {a b} {l₁ l₂ : List α} :
     (a :: l₁) ≤ (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ ≤ l₂ := by
-  dsimp only [instLE, instLT, List.le, List.lt]
+  simp only [LE.le, LT.lt, List.le, List.lt]
   open Classical in
   simp only [not_cons_lex_cons_iff, ne_eq]
   constructor

src/Init/MetaTypes.lean

@@ -137,6 +137,11 @@ structure Config where
   For local theorems, use `+suggestions` instead.
   -/
   locals : Bool := false
+  /--
+  If `instances` is `true`, `dsimp` will visit instance arguments.
+  If option `backward.dsimp.instances` is `true`, it overrides this field.
+  -/
+  instances : Bool := false
   deriving Inhabited, BEq
 
 end DSimp
@@ -308,6 +313,11 @@ structure Config where
   For local theorems, use `+suggestions` instead.
   -/
   locals : Bool := false
+  /--
+  If `instances` is `true`, `dsimp` will visit instance arguments.
+  If option `backward.dsimp.instances` is `true`, it overrides this field.
+  -/
+  instances : Bool := false
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

src/Lean/Elab/Structure.lean

@@ -1272,9 +1272,6 @@ private def addProjections (params : Array Expr) (r : ElabHeaderResult) (fieldIn
   for fieldInfo in fieldInfos do
     if fieldInfo.kind.isSubobject then
       addDeclarationRangesFromSyntax fieldInfo.declName r.view.ref fieldInfo.ref
-  for decl in projDecls do
-    -- projections may generate equation theorems
-    enableRealizationsForConst decl.projName
 
 private def registerStructure (structName : Name) (infos : Array StructFieldInfo) : TermElabM Unit := do
   let fields ← infos.filterMapM fun info => do
@@ -1563,6 +1560,11 @@ def elabStructureCommand : InductiveElabDescr where
               checkResolutionOrder view.declName
               return {
                 finalize := do
+                  -- Enable realizations for projections here (after @[class] attribute is applied)
+                  -- so that the realization context has class information available.
+                  for fieldInfo in fieldInfos do
+                    if fieldInfo.kind.isInCtor then
+                      enableRealizationsForConst fieldInfo.declName
                   if view.isClass then
                     addParentInstances parentInfos
               }

src/Lean/Elab/Tactic/Simp.lean

@@ -87,10 +87,14 @@ private def mkDischargeWrapper (optDischargeSyntax : Syntax) : TacticM Simp.Disc
   `optConfig` is of the form `("(" "config" ":=" term ")")?`
 -/
 def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TacticM Meta.Simp.Config := do
-  match kind with
-  | .simp    => elabSimpConfigCore optConfig
-  | .simpAll => return (← elabSimpConfigCtxCore optConfig).toConfig
-  | .dsimp   => return { (← elabDSimpConfigCore optConfig) with }
+  let cfg ← match kind with
+    | .simp    => elabSimpConfigCore optConfig
+    | .simpAll => pure (← elabSimpConfigCtxCore optConfig).toConfig
+    | .dsimp   => pure { (← elabDSimpConfigCore optConfig) with }
+  if Simp.backward.dsimp.instances.get (← getOptions) then
+    return { cfg with instances := true }
+  else
+    return cfg
 
 inductive ResolveSimpIdResult where
   | none

src/Lean/Meta/ACLt.lean

@@ -117,7 +117,7 @@ where
         let infos ← getParamsInfo aFn aArgs.size
         for i in *...infos.size do
           -- We ignore instance implicit arguments during comparison
-          if !infos[i]!.isInstImplicit then
+          if !infos[i]!.isInstance then
             if (← lt aArgs[i]! bArgs[i]!) then
               return true
             else if (← lt bArgs[i]! aArgs[i]!) then
@@ -155,7 +155,7 @@ where
         let infos ← getParamsInfo f args.size
         for i in *...infos.size do
           -- We ignore instance implicit arguments during comparison
-          if !infos[i]!.isInstImplicit then
+          if !infos[i]!.isInstance then
             if !(← lt args[i]! b) then
               return false
         for h : i in infos.size...args.size do

src/Lean/Meta/Basic.lean

@@ -241,6 +241,8 @@ structure ParamInfo where
     This information affects the generation of congruence theorems.
   -/
   isDecInst      : Bool       := false
+  /-- `isInstance` is true if the parameter type is a class instance. -/
+  isInstance     : Bool       := false
   /--
     `higherOrderOutParam` is true if this parameter is a higher-order output parameter
     of local instance.

src/Lean/Meta/CongrTheorems.lean

@@ -197,7 +197,7 @@ def getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind) :
       result := result.push .fixed
     else if info.paramInfo[i].isProp then
       result := result.push .cast
-    else if info.paramInfo[i].isInstImplicit then
+    else if info.paramInfo[i].isInstance then
       if let some mask := mask? then
         if h2 : i < mask.size then
           if mask[i] then
@@ -226,7 +226,7 @@ def getCongrSimpKindsForArgZero (info : FunInfo) : MetaM (Array CongrArgKind) :=
       result := result.push .eq
     else if info.paramInfo[i].isProp then
       result := result.push .cast
-    else if info.paramInfo[i].isInstImplicit then
+    else if info.paramInfo[i].isInstance then
       if shouldUseSubsingletonInst info result i then
         result := result.push .subsingletonInst
       else

src/Lean/Meta/DiscrTree/Main.lean

@@ -104,7 +104,7 @@ private def tmpStar := mkMVar tmpMVarId
 private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Bool := do
   if h : i < infos.size then
     let info := infos[i]
-    if info.isInstImplicit then
+    if info.isInstance then
       return true
     else if info.isImplicit || info.isStrictImplicit then
       return !(← isType a)

src/Lean/Meta/ExprDefEq.lean

@@ -300,7 +300,13 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
     let a₁   := args₁[i]!
     let a₂   := args₂[i]!
     let info := finfo.paramInfo[i]!
-    if info.isInstImplicit then
+    /-
+    **Note**: We use `binderInfo.isInstImplicit` (the `[..]` annotation) rather than
+    `info.isInstance` (whether the type is a class). Type class synthesis should only
+    be triggered for parameters explicitly marked for instance resolution, not merely
+    for parameters whose types happen to be class types.
+    -/
+    if info.binderInfo.isInstImplicit then
       discard <| trySynthPending a₁
       discard <| trySynthPending a₂
     unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do
@@ -309,7 +315,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
     let a₁   := args₁[i]!
     let a₂   := args₂[i]!
     let info := finfo.paramInfo[i]!
-    if info.isInstImplicit then
+    if info.isInstance then
       unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do
        return false
     else

src/Lean/Meta/FunInfo.lean

@@ -85,26 +85,50 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
           let dependsOnHigherOrderOutParam :=
             !higherOrderOutParams.isEmpty
             && Option.isSome (decl.type.find? fun e => e.isFVar && higherOrderOutParams.contains e.fvarId!)
+          let className? ← isClass? decl.type
+          /-
+          **Note**: We use `isClass? decl.type` instead of relying solely on binder annotations
+          (`[...]`) because users sometimes use implicit binders for class types when the instance
+          is already available from context. For example:
+          ```
+          structure OrdSet (α : Type) [Hashable α] [BEq α] where ...
+          def OrdSet.insert {_ : Hashable α} {_ : BEq α} (s : OrdSet α) (a : α) : OrdSet α := ...
+          ```
+          Here, `Hashable` and `BEq` are classes, but implicit binders are used because the
+          instances come from `OrdSet`'s parameters.
+
+          However, we also require the binder to be non-explicit because structures extending
+          classes use explicit binders for their constructor parameters:
+          ```
+          structure MyGroupTopology (α : Type) extends MyTopology α, IsContinuousMul α
+          -- Constructor type:
+          -- MyGroupTopology.mk (toMyTopology : MyTopology α) (toIsContinuousMul : IsContinuousMul α) : ...
+          ```
+          These explicit parameters should not be treated as instances for automation purposes.
+
+          -/
+          let isInstance := className?.isSome && !decl.binderInfo.isExplicit
           paramInfo := updateHasFwdDeps paramInfo backDeps
           paramInfo := paramInfo.push {
-            backDeps, dependsOnHigherOrderOutParam
+            backDeps, dependsOnHigherOrderOutParam, isInstance
             binderInfo := decl.binderInfo
             isProp     := (← isProp decl.type)
             isDecInst  := (← forallTelescopeReducing decl.type fun _ type => return type.isAppOf ``Decidable)
           }
-          if decl.binderInfo == .instImplicit then
-            /- Collect higher order output parameters of this class -/
-            if let some className ← isClass? decl.type then
-              if let some outParamPositions := getOutParamPositions? (← getEnv) className then
-                unless outParamPositions.isEmpty do
-                  let args := decl.type.getAppArgs
-                  for h2 : i in *...args.size do
-                    if outParamPositions.contains i then
-                      let arg := args[i]
-                      if let some idx := fvars.idxOf? arg then
-                        if (← whnf (← inferType arg)).isForall then
-                          paramInfo := paramInfo.modify idx fun info => { info with higherOrderOutParam := true }
-                          higherOrderOutParams := higherOrderOutParams.insert arg.fvarId!
+          if isInstance then
+            /- Collect higher order output parameters of this class IF `isInstance` is `true` -/
+            let some className := className? | unreachable!
+            /- Collect higher order output parameters of this class IF `isInstance` is `true` -/
+            if let some outParamPositions := getOutParamPositions? (← getEnv) className then
+              unless outParamPositions.isEmpty do
+                let args := decl.type.getAppArgs
+                for h2 : i in *...args.size do
+                  if outParamPositions.contains i then
+                    let arg := args[i]
+                    if let some idx := fvars.idxOf? arg then
+                      if (← whnf (← inferType arg)).isForall then
+                        paramInfo := paramInfo.modify idx fun info => { info with higherOrderOutParam := true }
+                        higherOrderOutParams := higherOrderOutParams.insert arg.fvarId!
         let resultDeps := collectDeps fvars type
         paramInfo := updateHasFwdDeps paramInfo resultDeps
         return { resultDeps, paramInfo }

src/Lean/Meta/LazyDiscrTree.lean

@@ -78,7 +78,7 @@ def tmpStar := mkMVar tmpMVarId
 def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Bool := do
   if h : i < infos.size then
     let info := infos[i]
-    if info.isInstImplicit then
+    if info.isInstance then
       return true
     else if info.isImplicit || info.isStrictImplicit then
       return !(← isType a)

src/Lean/Meta/Tactic/Grind/Anchor.lean

@@ -74,9 +74,9 @@ public partial def getAnchor (e : Expr) : GrindM UInt64 := do
           let arg := args[i]
           if h : i < pinfos.size then
             let info := pinfos[i]
-            -- **Note**: we ignore implicit instances we computing stable hash codes
+            -- **Note**: we ignore instances we computing stable hash codes
             -- TODO: evaluate whether we should ignore regular implicit arguments too.
-            unless info.isInstImplicit do
+            unless info.isImplicit do
               r := mix r (← getAnchor arg)
           else
             r := mix r (← getAnchor arg)

src/Lean/Meta/Tactic/Grind/Canon.lean

@@ -174,7 +174,7 @@ See comments at `ShouldCanonResult`.
 private def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM ShouldCanonResult := do
   if h : i < pinfos.size then
     let pinfo := pinfos[i]
-    if pinfo.isInstImplicit then
+    if pinfo.isInstance then
       return .canonInst
     else if pinfo.isProp then
       return .visit

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -23,6 +23,11 @@ register_builtin_option backward.dsimp.proofs : Bool := {
     descr    := "Let `dsimp` simplify proof terms"
   }
 
+register_builtin_option backward.dsimp.instances : Bool := {
+    defValue := false
+    descr    := "Let `dsimp` simplify instance terms"
+  }
+
 register_builtin_option debug.simp.check.have : Bool := {
     defValue := false
     descr    := "(simp) enable consistency checks for `have` telescope simplification"
@@ -497,7 +502,11 @@ private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific >> doNotVisitCharLit >> doNotVisitProofs
   let post := m.dpost >> dsimpReduce
   withInDSimpWithCache fun cache => do
-    transformWithCache e cache (usedLetOnly := cfg.zeta || cfg.zetaUnused) (pre := pre) (post := post)
+    transformWithCache e cache
+      (usedLetOnly := cfg.zeta || cfg.zetaUnused)
+      (skipInstances := !cfg.instances)
+      (pre := pre)
+      (post := post)
 
 def visitFn (e : Expr) : SimpM Result := do
   let f := e.getAppFn

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -627,7 +627,7 @@ def congrArgs (r : Result) (args : Array Expr) : SimpM Result := do
       if h : i < infos.size then
         trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i].hasFwdDeps}"
         let info := infos[i]
-        if cfg.ground && info.isInstImplicit then
+        if cfg.ground && info.isInstance then
           -- We don't visit instance implicit arguments when we are reducing ground terms.
           -- Motivation: many instance implicit arguments are ground, and it does not make sense
           -- to reduce them if the parent term is not ground.
@@ -713,7 +713,7 @@ def simpAppUsingCongr (e : Expr) : SimpM Result := do
       if h : i < infos.size then
         let info := infos[i]
         trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {a} hasFwdDeps: {info.hasFwdDeps}"
-        if cfg.ground && info.isInstImplicit then
+        if cfg.ground && info.isInstance then
           -- We don't visit instance implicit arguments when we are reducing ground terms.
           -- Motivation: many instance implicit arguments are ground, and it does not make sense
           -- to reduce them if the parent term is not ground.
@@ -788,7 +788,7 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
   let mut i          := 0 -- index at args
   for arg in args, kind in cgrThm.argKinds do
     if h : config.ground ∧ i < infos.size then
-      if (infos[i]'h.2).isInstImplicit then
+      if (infos[i]'h.2).isInstance then
         -- Do not visit instance implicit arguments when `ground := true`
         -- See comment at `congrArgs`
         argsNew := argsNew.push arg

src/Lean/Meta/Transform.lean

@@ -4,12 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Basic
-
+public import Lean.Meta.FunInfo
 public section
-
 namespace Lean
 
 inductive TransformStep where
@@ -30,16 +28,18 @@ inductive TransformStep where
 namespace Core
 
 /--
-  Transform the expression `input` using `pre` and `post`.
-  - First `pre` is invoked with the current expression and recursion is continued according to the `TransformStep` result.
-    In all cases, the expression contained in the result, if any, must be definitionally equal to the current expression.
-  - After recursion, if any, `post` is invoked on the resulting expression.
+Recursively transforms `input` using `pre` and `post` callbacks.
 
-  The term `s` in both `pre s` and `post s` may contain loose bound variables. So, this method is not appropriate for
-  if one needs to apply operations (e.g., `whnf`, `inferType`) that do not handle loose bound variables.
-  Consider using `Meta.transform` to avoid loose bound variables.
+For each subexpression:
+1. `pre` is invoked first; recursion continues according to the `TransformStep` result.
+2. After recursion (if any), `post` is invoked on the resulting expression.
 
-  This method is useful for applying transformations such as beta-reduction and delta-reduction.
+The expressions passed to `pre` and `post` may contain loose bound variables.
+Use `Meta.transform` instead if you need operations like `whnf` or `inferType`
+that require expressions without loose bound variables.
+
+Results are cached using pointer equality (`ExprStructEq`), so structurally
+identical subexpressions are transformed only once.
 -/
 partial def transform {m} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m]
     (input : Expr)
@@ -70,6 +70,7 @@ partial def transform {m} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m]
         | _                => visitPost e
   visit input |>.run
 
+/-- Applies beta reduction to all beta-reducible subexpressions in `e`. -/
 def betaReduce (e : Expr) : CoreM Expr :=
   transform e (pre := fun e => return if e.isHeadBetaTarget then .visit e.headBeta else .continue)
 
@@ -78,12 +79,19 @@ end Core
 namespace Meta
 
 /--
-Similar to `Meta.transform`, but allows the use of a pre-existing cache.
+Like `Meta.transform`, but accepts and returns a cache for reuse across multiple calls.
 
-Warnings:
-- For the cache to be valid, it must always use the same `pre` and `post` functions.
-- It is important that there are no other references to `cache` when it is passed to
-  `transformWithCache`, to avoid unnecessary copying of the hash map.
+Parameters:
+- `usedLetOnly`: when true, `mkLambdaFVars`/`mkForallFVars`/`mkLetFVars` only abstract
+  over variables that are actually used in the body.
+- `skipConstInApp`: when true, constant heads in applications are not visited separately.
+- `skipInstances`: when true, instance arguments (determined via `getFunInfo`) are not visited.
+
+The `skipInstances` flag is used by `dsimp` to avoid rewriting instances.
+
+**Warnings:**
+- The cache is only valid when using the same `pre` and `post` functions.
+- Ensure there are no other references to `cache` to avoid unnecessary hash map copying.
 -/
 @[inline]
 partial def transformWithCache {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
@@ -93,6 +101,7 @@ partial def transformWithCache {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT
     (post  : Expr → m TransformStep := fun e => return .done e)
     (usedLetOnly := false)
     (skipConstInApp := false)
+    (skipInstances := false)
     : m (Expr × Std.HashMap ExprStructEq Expr) :=
   let _ : STWorld IO.RealWorld m := ⟨⟩
   let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := MetaM) (liftM (m := ST IO.RealWorld) x) }
@@ -123,10 +132,22 @@ partial def transformWithCache {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT
         | e => visitPost (← mkLetFVars (usedLetOnly := usedLetOnly) (generalizeNondepLet := false) fvars (← visit (e.instantiateRev fvars)))
       let visitApp (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
         e.withApp fun f args => do
-          if skipConstInApp && f.isConst then
-            visitPost (mkAppN f (← args.mapM visit))
-          else
-            visitPost (mkAppN (← visit f) (← args.mapM visit))
+        let f ← if skipConstInApp && f.isConst then pure f else visit f
+        if skipInstances then
+          let infos := (← getFunInfoNArgs f args.size).paramInfo
+          let mut args := args.toVector
+          for h : i in *...args.size do
+            let arg := args[i]
+            if h : i < infos.size then
+              let info := infos[i]
+              if skipInstances && info.isInstance then
+                continue
+              args := args.set i (← visit arg)
+            else
+              args := args.set i (← visit arg)
+          visitPost (mkAppN f args.toArray)
+        else
+          visitPost (mkAppN f (← args.mapM visit))
       match (← pre e) with
       | .done e  => pure e
       | .visit e => visit e
@@ -163,6 +184,10 @@ def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
   let (e, _) ← transformWithCache input {} pre post usedLetOnly skipConstInApp
   return e
 
+/--
+Replaces all free variables in `e` that have let-values with their values.
+The substitution is applied recursively to the values themselves.
+-/
 -- TODO: add options to distinguish zeta and zetaDelta reduction
 def zetaReduce (e : Expr) : MetaM Expr := do
   let pre (e : Expr) : MetaM TransformStep := do
@@ -173,7 +198,8 @@ def zetaReduce (e : Expr) : MetaM Expr := do
   transform e (pre := pre) (usedLetOnly := true)
 
 /--
-Zeta reduces only the provided fvars, beta reducing the substitutions.
+Zeta-reduces only the specified free variables, applying beta reduction after substitution.
+For example, if `x` has value `fun y => y + 1` and appears as `x 2`, the result is `2 + 1`.
 -/
 def zetaDeltaFVars (e : Expr) (fvars : Array FVarId) : MetaM Expr :=
   let unfold? (fvarId : FVarId) : MetaM (Option Expr) := do
@@ -207,10 +233,10 @@ def unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr := do
     Core.transform e (pre := pre)
 
 /--
-Unfolds theorems that are applied to a `f x₁ .. xₙ` where `f` is in the given array, and
-`n ≤ SectionVars`, i.e. an unsaturated application of `f`.
+Unfolds theorems that are applied to `f x₁ .. xₙ` where `f` is in `fnNames` and
+`n ≤ numSectionVars` (i.e., an unsaturated application of `f`).
 
-This is used tounfoldIfArgIsAppOf undo proof abstraction for termination checking, as otherwise the bare
+This is used to undo proof abstraction for termination checking, as otherwise the bare
 occurrence of the recursive function prevents termination checking from succeeding.
 
 Usually, the argument is just `f` (the constant), arising from `mkAuxTheorem` abstracting over the
@@ -249,9 +275,11 @@ def unfoldIfArgIsAppOf (fnNames : Array Name) (numSectionVars : Nat) (e : Expr)
       af.isConst && fnNames.any fun f => af.constName! == f && axs.size ≤ numSectionVars
 
 
+/-- Removes all `inaccessible` annotations from `e`. -/
 def eraseInaccessibleAnnotations (e : Expr) : CoreM Expr :=
   Core.transform e (post := fun e => return .done <| if let some e := inaccessible? e then e else e)
 
+/-- Removes all `patternWithRef` annotations from `e`. -/
 def erasePatternRefAnnotations (e : Expr) : CoreM Expr :=
   Core.transform e (post := fun e => return .done <| if let some (_, e) := patternWithRef? e then e else e)
 

tests/lean/run/12172_regression.lean

@@ -0,0 +1,63 @@
+/-
+Regression test for https://github.com/leanprover/lean4/pull/12172
+
+The pattern:
+1. A class `MeasurableSpace` is used as both a class and explicit argument (via @)
+2. `Measure.trim` takes a Prop proof `hm : m ≤ m0` and returns `@Measure α m`
+3. A typeclass `SigmaFinite` depends on `μ.trim hm`
+4. A function `myFun` has `hm` explicit and `[SigmaFinite (μ.trim hm)]` as instance
+5. A section variable makes `hm` implicit
+6. A lemma `myFun_eq` takes an explicit proof argument before the final arg
+
+When calling `simp only [myFun_eq μ hs]`:
+- Before #12172: `hm` is inferred, instance is found, works
+- After #12172: Instance synthesis happens before `hm` is inferred, fails with
+  "failed to synthesize instance SigmaFinite (μ.trim ?m.XX)"
+
+Workaround: `simp only [myFun_eq (hm := hm) μ hs]`
+
+This pattern is used in Mathlib's MeasureTheory.Function.ConditionalExpectation.CondexpL1
+-/
+
+set_option autoImplicit false
+set_option linter.unusedVariables false
+
+universe u
+
+class MeasurableSpace (α : Type u) where
+  dummy : Unit := ()
+
+instance {α : Type u} : LE (MeasurableSpace α) where
+  le _ _ := True
+
+structure Measure (α : Type u) [MeasurableSpace α] where
+  val : Nat
+
+def Measure.trim {α : Type u} {m m0 : MeasurableSpace α}
+    (μ : @Measure α m0) (_hm : m ≤ m0) : @Measure α m :=
+  @Measure.mk α m μ.val
+
+class SigmaFinite {α : Type u} {m0 : MeasurableSpace α} (_μ : @Measure α m0) : Prop where
+  sigma_finite : True
+
+def myFun {α : Type u} {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : @Measure α m0)
+    [SigmaFinite (μ.trim hm)] (n : Nat) : Nat := n
+
+section
+variable {α : Type u} {m m0 : MeasurableSpace α}
+variable (μ : @Measure α m0)
+variable {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {s : Nat}
+
+theorem myFun_eq (hs : s > 0) (n : Nat) : myFun hm μ n = n := rfl
+
+-- This should work (worked before #12172)
+theorem test_implicit_hm (hs : s > 0) (x y : Nat) :
+    myFun hm μ (x + y) = myFun hm μ x + myFun hm μ y := by
+  simp only [myFun_eq μ hs]
+
+-- Workaround with explicit hm also works
+theorem test_explicit_hm (hs : s > 0) (x y : Nat) :
+    myFun hm μ (x + y) = myFun hm μ x + myFun hm μ y := by
+  simp only [myFun_eq (hm := hm) μ hs]
+
+end

tests/lean/run/doLogicTests.lean

@@ -147,7 +147,7 @@ theorem throwing_loop_spec :
   ⦃post⟨fun _ _ => ⌜False⌝,
         fun e s => ⌜e = 42 ∧ s = 4⌝⟩⦄ := by
   mintro hs
-  dsimp only [throwing_loop, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift]
+  dsimp +instances only [throwing_loop, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift]
   mspec
   mspec
   mspec

tests/lean/run/dsimp_instances.lean

@@ -0,0 +1,33 @@
+set_option warn.sorry false
+
+def f [Add α] (a : α) := a + a
+abbrev id' (a : α) := a
+abbrev addNat : Add Nat := ⟨Nat.add⟩
+
+set_option pp.explicit true
+
+/--
+trace: a b : Nat
+⊢ @Eq Nat (@f Nat (@id' (Add Nat) addNat) a) b
+---
+trace: a b : Nat
+⊢ @Eq Nat (@f Nat addNat a) b
+-/
+#guard_msgs in
+example : @f _ (id' addNat) a = id b := by
+  dsimp [id']
+  trace_state -- `id'` was not unfolded because it is part of an instance
+  dsimp +instances [id']
+  trace_state
+  sorry
+
+/--
+trace: a b : Nat
+⊢ @Eq Nat (@f Nat addNat a) b
+-/
+#guard_msgs in
+set_option backward.dsimp.instances true in
+example : @f _ (id' addNat) a = id b := by
+  dsimp [id']
+  trace_state
+  sorry

tests/lean/run/grind_ematch_gen_pattern.lean

@@ -10,13 +10,13 @@ example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = som
 
 /--
 info: Try these:
-  [apply] grind only [= gen Option.pbind_some', f, #ebef]
+  [apply] grind only [= gen Option.pbind_some', f, #81d1]
   [apply] grind only [= gen Option.pbind_some', f]
   [apply] grind =>
     instantiate only [= gen Option.pbind_some']
     instantiate only [f]
     mbtc
-    cases #ebef
+    cases #81d1
 -/
 #guard_msgs (info) in
 example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by

tests/lean/run/grind_finish_trace.lean

@@ -2,8 +2,8 @@ open Lean Grind
 
 /--
 info: Try these:
-  [apply] cases #c4b6 <;> cases #4c68 <;> ring
-  [apply] finish only [#c4b6, #4c68]
+  [apply] cases #e4c4 <;> cases #3e9f <;> ring
+  [apply] finish only [#e4c4, #3e9f]
 -/
 #guard_msgs in
 example {α : Type} [CommRing α] (a b c d e : α) :
@@ -17,10 +17,10 @@ example {α : Type} [CommRing α] (a b c d e : α) :
 /--
 info: Try these:
   [apply] ⏎
-    cases #b0f4
-    · cases #50fc
-    · cases #50fc <;> lia
-  [apply] finish only [#b0f4, #50fc]
+    cases #6c8c
+    · cases #4228
+    · cases #4228 <;> lia
+  [apply] finish only [#6c8c, #4228]
 -/
 #guard_msgs in
 example (p : Nat → Prop) (x y z w : Int) :
@@ -69,8 +69,8 @@ example (p : Nat → Prop) (x y z w : Int) :
 
 /--
 info: Try these:
-  [apply] cases #5c4b <;> cases #896f <;> ac
-  [apply] finish only [#5c4b, #896f]
+  [apply] cases #5d93 <;> cases #11de <;> ac
+  [apply] finish only [#5d93, #11de]
 -/
 #guard_msgs in
 example {α : Type} (op : α → α → α) [Std.Associative op] [Std.Commutative op] (a b c d e : α) :
@@ -105,11 +105,11 @@ set_option warn.sorry false
 /--
 info: Try this:
   [apply] ⏎
-    cases #c4b6
-    · cases #8c9f
+    cases #e4c4
+    · cases #7fb4
       · ring
       · sorry
-    · cases #8c9f
+    · cases #7fb4
       · ring
       · sorry
 -/
@@ -124,7 +124,7 @@ example {α : Type} [CommRing α] (a b c d e : α) :
 info: Try this:
   [apply] ⏎
     instantiate only [= Nat.min_def]
-    cases #7640
+    cases #d485
     · sorry
     · lia
 -/
@@ -137,8 +137,8 @@ example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j
 info: Try these:
   [apply] ⏎
     instantiate only [= getMsbD_setWidth']
-    cases #aa9d
-  [apply] finish only [= getMsbD_setWidth', #aa9d]
+    cases #1f39
+  [apply] finish only [= getMsbD_setWidth', #1f39]
 -/
 #guard_msgs in
 open BitVec in
@@ -151,13 +151,13 @@ example (ge : m ≥ n) (x : BitVec n) (i : Nat) :
     getMsbD (setWidth' ge x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m)) := by
   grind =>
     instantiate only [= getMsbD_setWidth']
-    cases #aa9d
+    cases #c2c1
 
 /--
 info: Try these:
-  [apply] cases #9942 <;>
-      instantiate only [= BitVec.getElem_and] <;> instantiate only [= BitVec.getElem_or] <;> cases #cfbc
-  [apply] finish only [= BitVec.getElem_and, = BitVec.getElem_or, #9942, #cfbc]
+  [apply] cases #52a6 <;>
+      instantiate only [= BitVec.getElem_and] <;> instantiate only [= BitVec.getElem_or] <;> cases #de0f
+  [apply] finish only [= BitVec.getElem_and, = BitVec.getElem_or, #52a6, #de0f]
 -/
 #guard_msgs in
 example (x y : BitVec 64) : (x ||| y) &&& x = x := by
@@ -186,8 +186,8 @@ example (a : Array (BitVec 64)) (i : Nat) (v : BitVec 64)
 info: Try these:
   [apply] ⏎
     mbtc
-    cases #a6c8
-  [apply] finish only [#a6c8]
+    cases #aceb
+  [apply] finish only [#aceb]
 -/
 #guard_msgs in
 example (f : Nat → Nat) (x : Nat)
@@ -198,8 +198,8 @@ example (f : Nat → Nat) (x : Nat)
 info: Try these:
   [apply] ⏎
     mbtc
-    cases #beb4
-  [apply] finish only [#beb4]
+    cases #cb64
+  [apply] finish only [#cb64]
 -/
 #guard_msgs in
 example (f : Int → Int → Int) (x y : Int)
@@ -220,7 +220,7 @@ example (f : Int → Int) (x y : Int)
     : 0 ≤ x → x ≤ 2 → f 0 = y → f 1 = y → f 2 = y → f x = y := by
   grind =>
     mbtc
-    cases #23ad <;> mbtc <;> cases #beb4 <;> mbtc <;> cases #beed
+    cases #ae37 <;> mbtc <;> cases #cb64 <;> mbtc <;> cases #de9d
 
 example (f : Int → Int) (x y : Int)
     : 0 ≤ x → x ≤ 2 → f 0 = y → f 1 = y → f 2 = y → f x = y := by
@@ -238,9 +238,9 @@ example (f g : Int → Int) (x y z w : Int)
   set_option trace.grind.split true in
   grind =>
     mbtc
-    cases #23ad
+    cases #ae37
     mbtc
-    cases #beb4
+    cases #cb64
 
 /--
 trace: [grind.split] w = 0, generation: 0
@@ -269,7 +269,7 @@ example (f g : Int → Int) (x y z w : Int)
       g w ≠ z → f x = y := by
   fail_if_success grind [#23ad] -- not possible to solve using this set of anchors.
   set_option trace.grind.split true in
-  grind only [#23ad, #beb4] -- Only these two splits were performed.
+  grind only [#ae37, #cb64] -- Only these two splits were performed.
 
 /--
 trace: [grind.split] x = 0, generation: 0
@@ -282,7 +282,8 @@ example (f g : Int → Int) (x y z w : Int)
       f 0 = y → f 1 = y →
       g w ≠ z → f x = y := by
   set_option trace.grind.split true in
-  grind => finish only [#23ad, #beb4] -- Only these two splits were performed.
+  grind =>
+    finish only [#ae37, #cb64]
 
 /--
 trace: [grind.ematch.instance] h: f (f a) = f a
@@ -314,7 +315,7 @@ example (f g : Int → Int)
     (_ : g (g b) = b)
     : f (f (f a)) = f a := by
   set_option trace.grind.ematch.instance true in
-  grind only [#99cb]
+  grind only [#7a0d]
 
 /--
 trace: [grind.ematch.instance] x✝²: f (f a) = f a
@@ -329,4 +330,4 @@ example (f g : Int → Int)
     (_ : g (g b) = b)
     : f (f (f a)) = f a := by
   set_option trace.grind.ematch.instance true in
-  grind => finish only [#99cb]
+  grind => finish only [#7a0d]

tests/lean/run/grind_indexmap_getElem_indices_lt.lean

@@ -110,7 +110,7 @@ example {h : a ∈ m} : m.indices[a] < m.size := by
   have : m.indices[a]? = some m.indices[a] := by grind
   have := m.WF m.indices[a]
   grind =>
-    instantiate only [#41bd]
+    instantiate only [#bc4b]
     instantiate only [= getElem?_neg]
     instantiate only [= size_keys]
 
@@ -119,7 +119,7 @@ example {h : a ∈ m} : m.indices[a] < m.size := by
   have : m.indices[a]? = some m.indices[a] := by grind
   have := m.WF m.indices[a]
   grind =>
-    instantiate only [#41bd]
+    instantiate only [#bc4b]
     -- Display asserted facts
     show_asserted
     -- Display asserted facts with `generation > 0`

tests/lean/run/grind_indexmap_trace.lean

@@ -149,22 +149,22 @@ info: Try these:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
-    cases #4ed2
-    · cases #ffdf
+    cases #bd4f
+    · cases #54dd
       · instantiate only
       · instantiate only
         instantiate only [= HashMap.contains_insert]
-    · cases #10d8
-      · cases #2688
+    · cases #2eb4
+      · cases #cc2e
         · instantiate only
         · instantiate only
           instantiate only [= HashMap.contains_insert]
-      · cases #ffdf
+      · cases #54dd
         · instantiate only
         · instantiate only
           instantiate only [= HashMap.contains_insert]
   [apply] finish only [= mem_indices_of_mem, insert, =_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos,
-    = HashMap.contains_insert, #4ed2, #ffdf, #10d8, #2688]
+    = HashMap.contains_insert, #bd4f, #54dd, #2eb4, #cc2e]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) :
@@ -176,22 +176,22 @@ info: Try these:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
-    cases #4ed2
-    · cases #ffdf
+    cases #bd4f
+    · cases #54dd
       · instantiate only
       · instantiate only
         instantiate only [= HashMap.contains_insert]
-    · cases #10d8
-      · cases #2688
+    · cases #2eb4
+      · cases #cc2e
         · instantiate only
         · instantiate only
           instantiate only [= HashMap.contains_insert]
-      · cases #ffdf
+      · cases #54dd
         · instantiate only
         · instantiate only
           instantiate only [= HashMap.contains_insert]
   [apply] finish only [= mem_indices_of_mem, insert, =_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos,
-    = HashMap.contains_insert, #4ed2, #ffdf, #10d8, #2688]
+    = HashMap.contains_insert, #bd4f, #54dd, #2eb4, #cc2e]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) :
@@ -203,40 +203,33 @@ example (m : IndexMap α β) (a a' : α) (b : β) :
   grind =>
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
-    cases #4ed2
-    · cases #ffdf
+    cases #bd4f
+    · cases #54dd
       · instantiate only
       · instantiate only
         instantiate only [= HashMap.contains_insert]
-    · cases #10d8
-      · cases #2688 <;> finish only [= HashMap.contains_insert]
-      · cases #ffdf <;> finish only [= HashMap.contains_insert]
+    · cases #2eb4
+      · cases #cc2e <;> finish only [= HashMap.contains_insert]
+      · cases #54dd <;> finish only [= HashMap.contains_insert]
 
 example (m : IndexMap α β) (a a' : α) (b : β) :
     a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
   grind =>
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
-    cases #4ed2
-    next =>
-      cases #ffdf
-      next => instantiate only
-      next =>
-        instantiate only
+    cases #bd4f
+    · cases #54dd
+      · instantiate only
+      · instantiate only
         instantiate only [= HashMap.contains_insert]
-    next =>
-      cases #95a0
-      next =>
-        cases #2688
-        next => instantiate only
-        next =>
-          instantiate only
+    · cases #2eb4
+      · cases #cc2e
+        · instantiate only
+        · instantiate only
           instantiate only [= HashMap.contains_insert]
-      next =>
-        cases #ffdf
-        next => instantiate only
-        next =>
-          instantiate only
+      · cases #54dd
+        · instantiate only
+        · instantiate only
           instantiate only [= HashMap.contains_insert]
 
 /--
@@ -247,9 +240,9 @@ info: Try these:
     instantiate only [=_ WF]
     instantiate only [= getElem?_neg, = getElem?_pos, = WF]
     instantiate only [= getElem?_neg, = getElem?_pos, = size_keys]
-    cases #f590
+    cases #dbaf
     · instantiate only [size]
-      cases #ffdf
+      cases #54dd
       · instantiate only
         instantiate only [= Array.getElem_set]
       · instantiate only
@@ -257,14 +250,14 @@ info: Try these:
     · instantiate only [= mem_indices_of_mem, = getElem_def, size]
       instantiate only [usr getElem_indices_lt, =_ WF]
       instantiate only [= getElem?_pos]
-      cases #ffdf
+      cases #54dd
       · instantiate only [WF']
         instantiate only [= Array.getElem_set]
       · instantiate only
         instantiate only [= HashMap.getElem?_insert, = Array.getElem_push]
   [apply] finish only [= mem_indices_of_mem, insert, = getElem_def, usr getElem?_pos, = getElem?_neg, = getElem?_pos,
     =_ WF, = WF, = size_keys, size, = Array.getElem_set, = HashMap.getElem?_insert, = Array.getElem_push,
-    usr getElem_indices_lt, WF', #f590, #ffdf]
+    usr getElem_indices_lt, WF', #dbaf, #54dd]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
@@ -276,8 +269,8 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
   grind =>
     instantiate only [= mem_indices_of_mem, insert, = getElem_def]
     instantiate only [= getElem?_neg, = getElem?_pos]
-    cases #f590
-    · cases #ffdf
+    cases #dbaf
+    · cases #54dd
       · instantiate only
         instantiate only [= Array.getElem_set]
       · instantiate only
@@ -286,7 +279,7 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
     · instantiate only [= mem_indices_of_mem, = getElem_def]
       instantiate only [usr getElem_indices_lt]
       instantiate only [size]
-      cases #ffdf
+      cases #54dd
       · instantiate only [usr getElem_indices_lt, =_ WF]
         instantiate only [= mem_indices_of_mem, = getElem?_pos, = Array.size_set,
           = Array.getElem_set]
@@ -298,7 +291,7 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
 info: Try these:
   [apply] grind only [= mem_indices_of_mem, insert, = getElem_def, usr getElem?_pos, = getElem?_neg, = getElem?_pos,
     =_ WF, = WF, = size_keys, size, = Array.getElem_set, = HashMap.getElem?_insert, = Array.getElem_push,
-    usr getElem_indices_lt, WF', #f590, #ffdf]
+    usr getElem_indices_lt, WF', #dbaf, #54dd]
   [apply] grind only [= mem_indices_of_mem, insert, = getElem_def, usr getElem?_pos, = getElem?_neg, = getElem?_pos,
     =_ WF, = WF, = size_keys, size, = Array.getElem_set, = HashMap.getElem?_insert, = Array.getElem_push,
     usr getElem_indices_lt, WF']
@@ -308,9 +301,9 @@ info: Try these:
     instantiate only [=_ WF]
     instantiate only [= getElem?_neg, = getElem?_pos, = WF]
     instantiate only [= getElem?_neg, = getElem?_pos, = size_keys]
-    cases #f590
+    cases #dbaf
     · instantiate only [size]
-      cases #ffdf
+      cases #54dd
       · instantiate only
         instantiate only [= Array.getElem_set]
       · instantiate only
@@ -318,7 +311,7 @@ info: Try these:
     · instantiate only [= mem_indices_of_mem, = getElem_def, size]
       instantiate only [usr getElem_indices_lt, =_ WF]
       instantiate only [= getElem?_pos]
-      cases #ffdf
+      cases #54dd
       · instantiate only [WF']
         instantiate only [= Array.getElem_set]
       · instantiate only
@@ -334,8 +327,8 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
   grind =>
     instantiate only [= mem_indices_of_mem, insert, = getElem_def]
     instantiate only [= getElem?_neg, = getElem?_pos]
-    cases #f590
-    · cases #ffdf
+    cases #dbaf
+    · cases #54dd
       · instantiate only
         instantiate only [= Array.getElem_set]
       · instantiate only
@@ -344,7 +337,7 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
     · instantiate only [= mem_indices_of_mem, = getElem_def]
       instantiate only [usr getElem_indices_lt]
       instantiate only [size]
-      cases #ffdf
+      cases #54dd
       · instantiate only [usr getElem_indices_lt, =_ WF]
         instantiate only [= mem_indices_of_mem, = getElem?_pos, = Array.size_set,
           = Array.getElem_set]
@@ -356,7 +349,8 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
     (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
   grind only [= mem_indices_of_mem, insert, = getElem_def, = getElem?_neg, = getElem?_pos,
     = Array.getElem_set, size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push,
-    usr getElem_indices_lt, =_ WF, = Array.size_set, WF', #f590, #ffdf]
+    usr getElem_indices_lt, usr Array.eq_empty_of_size_eq_zero, =_ WF, = Array.size_set, WF', #dbaf,
+    #54dd]
 
 /--
 info: Try these:
@@ -366,12 +360,12 @@ info: Try these:
     instantiate only [=_ WF]
     instantiate only [= getElem?_neg]
     instantiate only [= size_keys]
-    cases #1bba
+    cases #ffde
     · instantiate only [findIdx]
     · instantiate only
       instantiate only [= HashMap.getElem?_insert]
   [apply] finish only [findIdx, insert, = mem_indices_of_mem, usr getElem?_pos, = getElem?_neg, = getElem?_pos, =_ WF,
-    = size_keys, = HashMap.getElem?_insert, #1bba]
+    = size_keys, = HashMap.getElem?_insert, #ffde]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a : α) (b : β) :
@@ -382,7 +376,7 @@ example (m : IndexMap α β) (a : α) (b : β) :
 info: Try these:
   [apply] grind
   [apply] grind only [findIdx, insert, = mem_indices_of_mem, usr getElem?_pos, = getElem?_neg, = getElem?_pos, =_ WF,
-    = size_keys, = HashMap.getElem?_insert, #1bba]
+    = size_keys, = HashMap.getElem?_insert, #ffde]
   [apply] grind only [findIdx, insert, = mem_indices_of_mem, usr getElem?_pos, = getElem?_neg, = getElem?_pos, =_ WF,
     = size_keys, = HashMap.getElem?_insert]
   [apply] grind =>
@@ -391,7 +385,7 @@ info: Try these:
     instantiate only [=_ WF]
     instantiate only [= getElem?_neg]
     instantiate only [= size_keys]
-    cases #1bba
+    cases #ffde
     · instantiate only [findIdx]
     · instantiate only
       instantiate only [= HashMap.getElem?_insert]
@@ -410,7 +404,7 @@ example (m : IndexMap α β) (a : α) (b : β) :
   grind =>
     instantiate only [findIdx, insert, = mem_indices_of_mem]
     instantiate only [= getElem?_neg, = getElem?_pos]
-    cases #1bba
+    cases #acc3
     · instantiate only [findIdx]
     · finish only [= HashMap.mem_insert, = HashMap.getElem_insert]
 
@@ -419,7 +413,7 @@ example (m : IndexMap α β) (a : α) (b : β) :
   grind =>
     instantiate only [findIdx, insert, = mem_indices_of_mem]
     instantiate only [= getElem?_neg, = getElem?_pos]
-    cases #1bba <;>
+    cases #acc3 <;>
       finish only [findIdx, = HashMap.mem_insert, = HashMap.getElem_insert]
 
 end IndexMap

tests/lean/run/grind_interactive.lean

@@ -217,11 +217,11 @@ def h (as : List Nat) :=
 
 /--
 trace: [splits] Case split candidates
-  [split] #829a := match bs with
+  [split] #8289 := match bs with
       | [] => 1
       | [head] => 2
       | head :: head_1 :: tail => 3
-  [split] #dce6 := match as with
+  [split] #bf4f := match as with
       | [] => 1
       | [head] => 2
       | head :: head_1 :: tail => 3
@@ -237,7 +237,7 @@ example : h bs = 1 → h as ≠ 0 := by
   grind [h.eq_def] =>
     instantiate
     show_cases
-    cases #dce6
+    cases #bf4f
     instantiate
     focus instantiate
     instantiate
@@ -263,7 +263,7 @@ example : h bs = 1 → h as ≠ 0 := by
 example : h bs = 1 → h as ≠ 0 := by
   grind [h.eq_def] =>
     instantiate | as
-    cases #dce6
+    cases #bf4f
     all_goals instantiate
 
 /--
@@ -309,12 +309,12 @@ example (r p q : Prop) : p ∨ r → p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p
 example : h bs = 1 → h as ≠ 0 := by
   grind [h.eq_def] =>
     instantiate
-    cases #dce6 <;> instantiate
+    cases #bf4f <;> instantiate
 
 example : h bs = 1 → h as ≠ 1 := by
   grind [h.eq_def] =>
     instantiate
-    cases #dce6
+    cases #8289
     any_goals instantiate
     sorry
 
@@ -330,7 +330,7 @@ h✝ : as = []
 example : h bs = 1 → h as ≠ 0 := by
   grind -verbose [h.eq_def] =>
     instantiate
-    cases #dce6
+    cases #bf4f
     next => skip
     all_goals sorry
 
@@ -343,7 +343,7 @@ def g (as : List Nat) :=
 example : g bs = 1 → g as ≠ 0 := by
   grind [g.eq_def] =>
     instantiate
-    cases #dce6
+    cases #bf4f
     next => instantiate
     next => finish
     tactic =>
@@ -542,7 +542,7 @@ example : (a : Point Nat) → p a → x ≠ y → False := by
     show_cases
     rename_i y w _ -- Must reset cached anchors
     show_cases
-    cases #e2a6
+    cases #dded
     all_goals sorry
 
 example : (a : Point Nat) → p a → x ≠ y → False := by
@@ -553,7 +553,7 @@ example : (a : Point Nat) → p a → x ≠ y → False := by
     show_cases
     next y w _ =>
     show_cases
-    cases #e2a6
+    cases #dded
     all_goals sorry
 
 example : (a : Point Nat) → p a → x ≠ y → False := by

tests/lean/run/grind_option.lean

@@ -38,11 +38,11 @@ example : Option.guard (· ≤ 7) 3 = some 3 := by grind?
 
 /--
 info: Try these:
-  [apply] grind only [= Option.mem_bind_iff, #99bb]
+  [apply] grind only [= Option.mem_bind_iff, #8b09]
   [apply] grind only [= Option.mem_bind_iff]
   [apply] grind =>
     instantiate only [= Option.mem_bind_iff]
-    instantiate only [#99bb]
+    instantiate only [#8b09]
 -/
 #guard_msgs in
 example {x : β} {o : Option α} {f : α → Option β} (h : a ∈ o) (h' : x ∈ f a) : x ∈ o.bind f := by grind?

tests/lean/run/grind_order_issue.lean

@@ -101,9 +101,9 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
     (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
   grind -ring -linarith -lia =>
     instantiate only [= getElem_def, insert]
-    cases #f590
+    cases #dbaf
     next =>
-      cases #ffdf
+      cases #54dd
       next => sorry
       next =>
         instantiate only
@@ -116,9 +116,9 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
     (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
   grind -ring -linarith -lia =>
     instantiate only [= getElem_def, insert]
-    cases #f590
+    cases #dbaf
     next =>
-      cases #ffdf
+      cases #54dd
       next => sorry
       next =>
         instantiate only

tests/lean/run/grind_reducible.lean

@@ -47,13 +47,13 @@ example :
 example :
     (Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂)
     = (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
-  grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun]
+  grind -reducible => cases #d592 <;> instantiate only [Equiv.congr_fun]
 
 /--
 info: Try these:
-  [apply] grind -reducible only [Equiv.congr_fun, #5103]
+  [apply] grind -reducible only [Equiv.congr_fun, #d592]
   [apply] grind -reducible only [Equiv.congr_fun]
-  [apply] grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun]
+  [apply] grind -reducible => cases #d592 <;> instantiate only [Equiv.congr_fun]
 -/
 #guard_msgs in
 example :

tests/lean/run/grind_trace.lean

@@ -42,20 +42,20 @@ attribute [grind ext] List.ext_getElem?
 info: Try these:
   [apply] grind only [= List.getElem?_replicate, = List.getElem?_map, = List.getElem?_eq_none,
     = List.getElem?_eq_getElem, = List.length_replicate, = List.getElem?_eq_some_iff, = Option.map_some,
-    = Option.map_none, #12fe, #986e, #0323]
+    = Option.map_none, #648a, #bb68, #a564]
   [apply] grind only [= List.getElem?_replicate, = List.getElem?_map, = List.getElem?_eq_none,
     = List.getElem?_eq_getElem, = List.length_replicate, = List.getElem?_eq_some_iff, = Option.map_some,
     = Option.map_none]
   [apply] grind =>
-    cases #12fe
+    cases #648a
     instantiate only [= List.getElem?_replicate, = List.getElem?_map, = List.getElem?_eq_none,
       = List.getElem?_eq_getElem]
     instantiate only [= List.getElem?_replicate, = List.getElem?_eq_none, = List.getElem?_eq_getElem,
       = List.length_replicate]
     instantiate only [= List.length_replicate]
-    cases #986e
+    cases #bb68
     · instantiate only [= List.getElem?_eq_some_iff]
-      cases #0323
+      cases #a564
       · instantiate only [= Option.map_some]
       · instantiate only [= Option.map_none]
     · instantiate only [= Option.map_some]
@@ -66,11 +66,11 @@ theorem map_replicate' : (List.replicate n a).map f = List.replicate n (f a) :=
 
 /--
 info: Try these:
-  [apply] grind only [= List.getLast?_eq_some_iff, ← List.mem_concat_self, #e8ab]
+  [apply] grind only [= List.getLast?_eq_some_iff, ← List.mem_concat_self, #1ecf]
   [apply] grind only [= List.getLast?_eq_some_iff, ← List.mem_concat_self]
   [apply] grind =>
     instantiate only [= List.getLast?_eq_some_iff]
-    cases #e8ab <;> instantiate only [← List.mem_concat_self]
+    cases #1ecf <;> instantiate only [← List.mem_concat_self]
 -/
 #guard_msgs (info) in
 theorem mem_of_getLast?_eq_some' {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs := by

tests/lean/run/grind_try_trace.lean

@@ -61,12 +61,12 @@ example : f (f 0) > 0 := by
 /--
 info: Try these:
   [apply] grind [= f.eq_def]
-  [apply] grind only [= f.eq_def, #bb96]
+  [apply] grind only [= f.eq_def, #6818]
   [apply] grind only [= f.eq_def]
   [apply] grind =>
     instantiate only [= f.eq_def]
     instantiate only
-    cases #bb96 <;> instantiate only
+    cases #6818 <;> instantiate only
 -/
 #guard_msgs (info) in
 example : f x > 0 := by

tests/lean/run/linearCategory_perf_issue.lean

@@ -362,12 +362,10 @@ instance functorCategoryPreadditive : Preadditive (C ⥤ D) where
         apply neg_add_cancel }
   add_comp := by
     intros
-    dsimp only [id_eq]
     ext
     apply add_comp
   comp_add := by
     intros
-    dsimp only [id_eq]
     ext
     apply comp_add
 

tests/lean/run/sym_simp_4.lean

@@ -52,7 +52,7 @@ example (α β : Type) (p q : Prop) : q → β → p → α → True := by
   sym_simp []
 
 /--
-trace: α✝ : Sort ?u.1893
+trace: α✝ : Sort ?u.1921
 x : α✝
 α : Type
 p : Prop