fix: use isClass? instead of binder annotation to identify instance parameters (#12172)

This PR fixes how we determine whether a function parameter is an
instance.
Previously, we relied on binder annotations (e.g., `[Ring A]` vs `{_ :
Ring A}`)
to make this determination. This is unreliable because users
legitimately use
`{..}` binders for class types when the instance is already available
from
context. For example:
```lean
structure OrdSet (α : Type) [Hashable α] [BEq α] where
  ...

def OrdSet.insert {_ : Hashable α} {_ : BEq α} (s : OrdSet α) (a : α) : OrdSet α :=
  ...
```

Here, `Hashable` and `BEq` are classes, but the `{..}` binder is
intentional, the
instances come from `OrdSet`'s parameters, so type class resolution is
unnecessary.

The fix checks the parameter's *type* using `isClass?` rather than its
syntax, and
caches this information in `FunInfo`. This affects several subsystems:

- **Discrimination trees**: instance parameters should not be indexed
even if marked with `{..}`
- **Congruence lemma generation**: instances require special treatment
- **`grind` canonicalizer**: must ensure canonical instances

**Potential regressions**: automation may now behave differently in
cases where it
previously misidentified instance parameters. For example, a rewrite
rule in `simp` that was
not firing due to incorrect indexing may now fire.

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Claude <noreply@anthropic.com>

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/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/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

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/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/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