chore: fix tests

src/Init/Grind/Tactics.lean

@@ -15,12 +15,13 @@ Reset all `grind` attributes. This command is intended for testing purposes only
 syntax (name := resetGrindAttrs) "reset_grind_attrs%" : command
 
 namespace Attr
-syntax grindEq     := "= "
-syntax grindEqBoth := atomic("_" "=" "_ ")
-syntax grindEqRhs  := atomic("=" "_ ")
+syntax grindGen    := &"gen "
+syntax grindEq     := "= " (grindGen)?
+syntax grindEqBoth := atomic("_" "=" "_ ") (grindGen)?
+syntax grindEqRhs  := atomic("=" "_ ") (grindGen)?
 syntax grindEqBwd  := atomic("←" "= ") <|> atomic("<-" "= ")
-syntax grindBwd    := "← " <|> "-> "
-syntax grindFwd    := "→ " <|> "<- "
+syntax grindBwd    := ("← " <|> "<- ") (grindGen)?
+syntax grindFwd    := "→ " <|> "-> "
 syntax grindRL     := "⇐ " <|> "<= "
 syntax grindLR     := "⇒ " <|> "=> "
 syntax grindUsr    := &"usr "
@@ -28,7 +29,10 @@ syntax grindCases  := &"cases "
 syntax grindCasesEager := atomic(&"cases" &"eager ")
 syntax grindIntro  := &"intro "
 syntax grindExt    := &"ext "
-syntax grindMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager <|> grindCases <|> grindIntro <|> grindExt
+syntax grindMod :=
+    grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd
+    <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager
+    <|> grindCases <|> grindIntro <|> grindExt <|> grindGen
 syntax (name := grind) "grind" (grindMod)? : attr
 syntax (name := grind?) "grind?" (grindMod)? : attr
 end Attr

src/Lean/Elab/Tactic/Grind.lean

@@ -86,7 +86,7 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
       | .intro =>
         if let some info ← Grind.isCasesAttrPredicateCandidate? declName false then
           for ctor in info.ctors do
-            params ← withRef p <| addEMatchTheorem params ctor .default
+            params ← withRef p <| addEMatchTheorem params ctor (.default false)
         else
           throwError "invalid use of `intro` modifier, `{declName}` is not an inductive predicate"
       | .ext =>
@@ -98,9 +98,9 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
             -- If it is an inductive predicate,
             -- we also add the constructors (intro rules) as E-matching rules
             for ctor in info.ctors do
-              params ← withRef p <| addEMatchTheorem params ctor .default
+              params ← withRef p <| addEMatchTheorem params ctor (.default false)
         else
-          params ← withRef p <| addEMatchTheorem params declName .default
+          params ← withRef p <| addEMatchTheorem params declName (.default false)
     | _ => throwError "unexpected `grind` parameter{indentD p}"
   return params
 where
@@ -108,15 +108,16 @@ where
     let info ← getConstInfo declName
     match info with
     | .thmInfo _ | .axiomInfo _ | .ctorInfo _ =>
-      if kind == .eqBoth then
-        let params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqLhs) }
-        return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqRhs) }
-      else
+      match kind with
+      | .eqBoth gen =>
+        let params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen)) }
+        return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen)) }
+      | _ =>
         return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName kind) }
     | .defnInfo _ =>
       if (← isReducible declName) then
         throwError "`{declName}` is a reducible definition, `grind` automatically unfolds them"
-      if kind != .eqLhs && kind != .default then
+      if !kind.isEqLhs && !kind.isDefault then
         throwError "invalid `grind` parameter, `{declName}` is a definition, the only acceptable (and redundant) modifier is '='"
       let some thms ← Grind.mkEMatchEqTheoremsForDef? declName
         | throwError "failed to generate equation theorems for `{declName}`"
@@ -223,16 +224,21 @@ def mkGrindOnly
       else
         let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
         let param ← match kind with
-          | .eqLhs     => `(Parser.Tactic.grindParam| = $decl)
-          | .eqRhs     => `(Parser.Tactic.grindParam| =_ $decl)
-          | .eqBoth    => `(Parser.Tactic.grindParam| _=_ $decl)
-          | .eqBwd     => `(Parser.Tactic.grindParam| ←= $decl)
-          | .bwd       => `(Parser.Tactic.grindParam| ← $decl)
-          | .fwd       => `(Parser.Tactic.grindParam| → $decl)
-          | .leftRight => `(Parser.Tactic.grindParam| => $decl)
-          | .rightLeft => `(Parser.Tactic.grindParam| <= $decl)
-          | .user      => `(Parser.Tactic.grindParam| usr $decl)
-          | .default   => `(Parser.Tactic.grindParam| $decl:ident)
+          | .eqLhs false   => `(Parser.Tactic.grindParam| = $decl:ident)
+          | .eqLhs true    => `(Parser.Tactic.grindParam| = gen $decl:ident)
+          | .eqRhs false   => `(Parser.Tactic.grindParam| =_ $decl:ident)
+          | .eqRhs true    => `(Parser.Tactic.grindParam| =_ gen $decl:ident)
+          | .eqBoth false  => `(Parser.Tactic.grindParam| _=_ $decl:ident)
+          | .eqBoth true   => `(Parser.Tactic.grindParam| _=_ gen $decl:ident)
+          | .eqBwd         => `(Parser.Tactic.grindParam| ←= $decl:ident)
+          | .bwd false     => `(Parser.Tactic.grindParam| ← $decl:ident)
+          | .bwd true      => `(Parser.Tactic.grindParam| ← gen $decl:ident)
+          | .fwd           => `(Parser.Tactic.grindParam| → $decl:ident)
+          | .leftRight     => `(Parser.Tactic.grindParam| => $decl:ident)
+          | .rightLeft     => `(Parser.Tactic.grindParam| <= $decl:ident)
+          | .user          => `(Parser.Tactic.grindParam| usr $decl:ident)
+          | .default false => `(Parser.Tactic.grindParam| $decl:ident)
+          | .default true  => `(Parser.Tactic.grindParam| gen $decl:ident)
         params := params.push param
   for declName in trace.eagerCases.toList do
     unless Grind.isBuiltinEagerCases declName do

src/Lean/Elab/Tactic/Try.lean

@@ -610,7 +610,7 @@ private def setGrindParams (tac : TSyntax `tactic) (params : Array (TSyntax ``Pa
 /-- Given a set of declaration names, returns `grind` parameters of the form `= <declName>` -/
 private def mkGrindEqnParams (declNames : Array Name) : MetaM (Array (TSyntax ``Parser.Tactic.grindParam)) := do
   declNames.mapM fun declName => do
-    `(Parser.Tactic.grindParam| = $(← toIdent declName))
+    `(Parser.Tactic.grindParam| = $(← toIdent declName):ident)
 
 private def mkGrindStx (info : Try.Info) : MetaM (TSyntax `tactic) := do
   let grind ← `(tactic| grind?)

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

@@ -20,19 +20,24 @@ inductive AttrKind where
 /-- Return theorem kind for `stx` of the form `Attr.grindThmMod` -/
 def getAttrKindCore (stx : Syntax) : CoreM AttrKind := do
   match stx with
-  | `(Parser.Attr.grindMod| =) => return .ematch .eqLhs
+  | `(Parser.Attr.grindMod| =) => return .ematch (.eqLhs false)
+  | `(Parser.Attr.grindMod| = gen) => return .ematch (.eqLhs true)
   | `(Parser.Attr.grindMod| →)
   | `(Parser.Attr.grindMod| ->) => return .ematch .fwd
   | `(Parser.Attr.grindMod| ←)
-  | `(Parser.Attr.grindMod| <-) => return .ematch .bwd
-  | `(Parser.Attr.grindMod| =_) => return .ematch .eqRhs
-  | `(Parser.Attr.grindMod| _=_) => return .ematch .eqBoth
+  | `(Parser.Attr.grindMod| <-) => return .ematch (.bwd false)
+  | `(Parser.Attr.grindMod| <- gen) => return .ematch (.bwd true)
+  | `(Parser.Attr.grindMod| =_) => return .ematch (.eqRhs false)
+  | `(Parser.Attr.grindMod| =_ gen) => return .ematch (.eqRhs true)
+  | `(Parser.Attr.grindMod| _=_) => return .ematch (.eqBoth false)
+  | `(Parser.Attr.grindMod| _=_ gen) => return .ematch (.eqBoth true)
   | `(Parser.Attr.grindMod| ←=) => return .ematch .eqBwd
   | `(Parser.Attr.grindMod| ⇒)
   | `(Parser.Attr.grindMod| =>) => return .ematch .leftRight
   | `(Parser.Attr.grindMod| ⇐)
   | `(Parser.Attr.grindMod| <=) => return .ematch .rightLeft
   | `(Parser.Attr.grindMod| usr) => return .ematch .user
+  | `(Parser.Attr.grindMod| gen) => return .ematch (.default true)
   | `(Parser.Attr.grindMod| cases) => return .cases false
   | `(Parser.Attr.grindMod| cases eager) => return .cases true
   | `(Parser.Attr.grindMod| intro) => return .intro
@@ -87,7 +92,7 @@ private def registerGrindAttr (showInfo : Bool) : IO Unit :=
       | .intro =>
         if let some info ← isCasesAttrPredicateCandidate? declName false then
           for ctor in info.ctors do
-            addEMatchAttr ctor attrKind .default (showInfo := showInfo)
+            addEMatchAttr ctor attrKind (.default false) (showInfo := showInfo)
         else
           throwError "invalid `[grind intro]`, `{declName}` is not an inductive predicate"
       | .ext => addExtAttr declName attrKind
@@ -98,9 +103,9 @@ private def registerGrindAttr (showInfo : Bool) : IO Unit :=
             -- If it is an inductive predicate,
             -- we also add the constructors (intro rules) as E-matching rules
             for ctor in info.ctors do
-              addEMatchAttr ctor attrKind .default (showInfo := showInfo)
+              addEMatchAttr ctor attrKind (.default false) (showInfo := showInfo)
         else
-          addEMatchAttr declName attrKind .default (showInfo := showInfo)
+          addEMatchAttr declName attrKind (.default false) (showInfo := showInfo)
     erase := fun declName => MetaM.run' do
       if showInfo then
         throwError "`[grind?]` is a helper attribute for displaying inferred patterns, if you want to remove the attribute, consider using `[grind]` instead"

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

@@ -148,18 +148,61 @@ private def preprocessMatchCongrEqType (type : Expr) : MetaM Expr := do
     let resultType := mkAppN resultTypeFn (resultArgs.set! 1 lhsNew)
     mkForallFVars hs resultType
 
+/--
+A heuristic procedure for detecting generalized patterns.
+For example, given the theorem
+```
+theorem Option.pbind_some' {α β} {x : Option α} {a : α} {f : (a : α) → x = some a → Option β}
+  (h : x = some a) : pbind x f = f a h
+```
+In the current implementation, we support only occurrences in the resulting type.
+Thus, the following resulting type is generated for the example above:
+```
+pbind (Grind.genPattern h x (some a)) f = f a h
+```
+-/
+private def detectGeneralizedPatterns? (type : Expr) : MetaM Expr := do
+  forallTelescopeReducing type fun hs resultType => do
+    let isTarget? (lhs : Expr) (rhs : Expr) (s : FVarSubst) : Option (FVarId × Expr) := Id.run do
+      let .fvar fvarId := lhs | return none
+      if !hs.contains lhs then
+        return none -- It is a foreign free variable
+      if rhs.containsFVar fvarId then
+        return none -- It is not a generalization if `rhs` contains it
+      if s.contains fvarId then
+        return none -- Remark: may want to abort instead, it is probably not a generalization
+      let rhs := s.apply rhs
+      return some (fvarId, rhs)
+    let mut s : FVarSubst := {}
+    for h in hs do
+      match_expr (← inferType h) with
+      | f@Eq α lhs rhs =>
+        let some (fvarId, rhs) := isTarget? lhs rhs s | pure ()
+        s := s.insert fvarId <| mkGenPattern f.constLevels! α h lhs rhs
+      | f@HEq α lhs β rhs =>
+        let some (fvarId, rhs) := isTarget? lhs rhs s | pure ()
+        s := s.insert fvarId <| mkGenHEqPattern f.constLevels! α β h lhs rhs
+      | _ => pure ()
+    if s.isEmpty then
+      return type
+    let resultType' := s.apply resultType
+    if resultType' == resultType then
+      return type
+    mkForallFVars hs resultType'
+
 /--
 Given the proof for a proposition to be used as an E-matching theorem,
 infers its type, and preprocess it to identify generalized patterns.
 Recall that we infer these generalized patterns automatically for
 `match` congruence equations.
 -/
-private def inferEMatchProofType (proof : Expr) : MetaM Expr := do
+private def inferEMatchProofType (proof : Expr) (gen : Bool) : MetaM Expr := do
   let type ← inferType proof
   if (← isMatchCongrEqConst proof) then
     preprocessMatchCongrEqType type
+  else if gen then
+    detectGeneralizedPatterns? type
   else
-    -- TODO: implement support for to be implemented annotations
     return type
 
 -- Configuration for the `grind` normalizer. We want both `zetaDelta` and `zeta`
@@ -210,31 +253,53 @@ instance : Hashable Origin where
   hash a := hash a.key
 
 inductive EMatchTheoremKind where
-  | eqLhs | eqRhs | eqBoth | eqBwd | fwd | bwd | leftRight | rightLeft | default | user /- pattern specified using `grind_pattern` command -/
+  | eqLhs (gen : Bool)
+  | eqRhs (gen : Bool)
+  | eqBoth (gen : Bool)
+  | eqBwd
+  | fwd
+  | bwd (gen : Bool)
+  | leftRight
+  | rightLeft
+  | default (gen : Bool)
+  | user /- pattern specified using `grind_pattern` command -/
   deriving Inhabited, BEq, Repr, Hashable
 
+def EMatchTheoremKind.isEqLhs : EMatchTheoremKind → Bool
+  | .eqLhs _ => true
+  | _ => false
+
+def EMatchTheoremKind.isDefault : EMatchTheoremKind → Bool
+  | .default _ => true
+  | _ => false
+
 private def EMatchTheoremKind.toAttribute : EMatchTheoremKind → String
-  | .eqLhs     => "[grind =]"
-  | .eqRhs     => "[grind =_]"
-  | .eqBoth    => "[grind _=_]"
-  | .eqBwd     => "[grind ←=]"
-  | .fwd       => "[grind →]"
-  | .bwd       => "[grind ←]"
-  | .leftRight => "[grind =>]"
-  | .rightLeft => "[grind <=]"
-  | .default   => "[grind]"
-  | .user      => "[grind]"
+  | .eqLhs true     => "[grind = gen]"
+  | .eqLhs false    => "[grind =]"
+  | .eqRhs true     => "[grind =_ gen]"
+  | .eqRhs false    => "[grind =_]"
+  | .eqBoth false   => "[grind _=_]"
+  | .eqBoth true    => "[grind _=_ gen]"
+  | .eqBwd          => "[grind ←=]"
+  | .fwd            => "[grind →]"
+  | .bwd false      => "[grind ←]"
+  | .bwd true       => "[grind ← gen]"
+  | .leftRight      => "[grind =>]"
+  | .rightLeft      => "[grind <=]"
+  | .default false  => "[grind]"
+  | .default true   => "[grind gen]"
+  | .user           => "[grind]"
 
 private def EMatchTheoremKind.explainFailure : EMatchTheoremKind → String
-  | .eqLhs     => "failed to find pattern in the left-hand side of the theorem's conclusion"
-  | .eqRhs     => "failed to find pattern in the right-hand side of the theorem's conclusion"
-  | .eqBoth    => unreachable! -- eqBoth is a macro
+  | .eqLhs _   => "failed to find pattern in the left-hand side of the theorem's conclusion"
+  | .eqRhs _   => "failed to find pattern in the right-hand side of the theorem's conclusion"
+  | .eqBoth _  => unreachable! -- eqBoth is a macro
   | .eqBwd     => "failed to use theorem's conclusion as a pattern"
   | .fwd       => "failed to find patterns in the antecedents of the theorem"
-  | .bwd       => "failed to find patterns in the theorem's conclusion"
+  | .bwd _     => "failed to find patterns in the theorem's conclusion"
   | .leftRight => "failed to find patterns searching from left to right"
   | .rightLeft => "failed to find patterns searching from right to left"
-  | .default   => "failed to find patterns"
+  | .default _ => "failed to find patterns"
   | .user      => unreachable!
 
 /-- A theorem for heuristic instantiation based on E-matching. -/
@@ -747,8 +812,8 @@ Given a theorem with proof `proof` and type of the form `∀ (a_1 ... a_n), lhs
 creates an E-matching pattern for it using `addEMatchTheorem n [lhs]`
 If `normalizePattern` is true, it applies the `grind` simplification theorems and simprocs to the pattern.
 -/
-def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (normalizePattern : Bool) (useLhs : Bool) (showInfo := false) : MetaM EMatchTheorem := do
-  let (numParams, patterns) ← forallTelescopeReducing (← inferEMatchProofType proof) fun xs type => do
+def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (normalizePattern : Bool) (useLhs : Bool) (gen : Bool) (showInfo := false) : MetaM EMatchTheorem := do
+  let (numParams, patterns) ← forallTelescopeReducing (← inferEMatchProofType proof gen) fun xs type => do
     let (lhs, rhs) ← match_expr type with
       | Eq _ lhs rhs => pure (lhs, rhs)
       | Iff lhs rhs => pure (lhs, rhs)
@@ -760,10 +825,10 @@ def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof :
     trace[grind.debug.ematch.pattern] "mkEMatchEqTheoremCore: after preprocessing: {pat}, {← normalize pat normConfig}"
     let pats := splitWhileForbidden (pat.abstract xs)
     return (xs.size, pats)
-  mkEMatchTheoremCore origin levelParams numParams proof patterns (if useLhs then .eqLhs else .eqRhs) (showInfo := showInfo)
+  mkEMatchTheoremCore origin levelParams numParams proof patterns (if useLhs then .eqLhs gen else .eqRhs gen) (showInfo := showInfo)
 
 def mkEMatchEqBwdTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (showInfo := false) : MetaM EMatchTheorem := do
-  let (numParams, patterns) ← forallTelescopeReducing (← inferEMatchProofType proof) fun xs type => do
+  let (numParams, patterns) ← forallTelescopeReducing (← inferEMatchProofType proof (gen := false)) fun xs type => do
     let_expr f@Eq α lhs rhs := type
       | throwError "invalid E-matching `←=` theorem, conclusion must be an equality{indentExpr type}"
     let pat ← preprocessPattern (mkEqBwdPattern f.constLevels! α lhs rhs)
@@ -777,8 +842,8 @@ creates an E-matching pattern for it using `addEMatchTheorem n [lhs]`
 If `normalizePattern` is true, it applies the `grind` simplification theorems and simprocs to the
 pattern.
 -/
-def mkEMatchEqTheorem (declName : Name) (normalizePattern := true) (useLhs : Bool := true) (showInfo := false) : MetaM EMatchTheorem := do
-  mkEMatchEqTheoremCore (.decl declName) #[] (← getProofFor declName) normalizePattern useLhs (showInfo := showInfo)
+def mkEMatchEqTheorem (declName : Name) (normalizePattern := true) (useLhs : Bool := true) (gen : Bool := false) (showInfo := false) : MetaM EMatchTheorem := do
+  mkEMatchEqTheoremCore (.decl declName) #[] (← getProofFor declName) normalizePattern useLhs gen (showInfo := showInfo)
 
 /--
 Adds an E-matching theorem to the environment.
@@ -956,6 +1021,15 @@ where
         return none
     | _ => return none
 
+def EMatchTheoremKind.gen : EMatchTheoremKind → Bool
+  | .eqLhs gen => gen
+  | .eqRhs gen => gen
+  | .eqBoth gen => gen
+  | .default gen => gen
+  | .bwd gen => gen
+  | .eqBwd | .fwd | .rightLeft
+  | .leftRight | .user => false
+
 /--
 Creates an E-match theorem using the given proof and kind.
 If `groundPatterns` is `true`, it accepts patterns without pattern variables. This is useful for
@@ -965,13 +1039,16 @@ since the theorem is already in the `grind` state and there is nothing to be ins
 def mkEMatchTheoremWithKind?
       (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind)
       (groundPatterns := true) (showInfo := false) : MetaM (Option EMatchTheorem) := do
-  if kind == .eqLhs then
-    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true) (showInfo := showInfo))
-  else if kind == .eqRhs then
-    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := false) (showInfo := showInfo))
-  else if kind == .eqBwd then
+  match kind with
+  | .eqLhs gen =>
+    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true) (gen := gen) (showInfo := showInfo))
+  | .eqRhs gen =>
+    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := false) (gen := gen) (showInfo := showInfo))
+  | .eqBwd =>
     return (← mkEMatchEqBwdTheoremCore origin levelParams proof (showInfo := showInfo))
-  let type ← inferEMatchProofType proof
+  | _ =>
+    pure ()
+  let type ← inferEMatchProofType proof kind.gen
   /-
   Remark: we should not use `forallTelescopeReducing` (with default reducibility) here
   because it may unfold a definition/abstraction, and then select a suboptimal pattern.
@@ -996,10 +1073,10 @@ def mkEMatchTheoremWithKind?
         if ps.isEmpty then
           throwError "invalid `grind` forward theorem, theorem `{← origin.pp}` does not have propositional hypotheses"
         pure ps
-      | .bwd => pure #[type]
+      | .bwd _ => pure #[type]
       | .leftRight => pure <| (← getPropTypes xs).push type
       | .rightLeft => pure <| #[type] ++ (← getPropTypes xs).reverse
-      | .default => pure <| #[type] ++ (← getPropTypes xs)
+      | .default _ => pure <| #[type] ++ (← getPropTypes xs)
       | _ => unreachable!
     go xs searchPlaces
 where
@@ -1057,14 +1134,15 @@ def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMat
     return s.erase <| .decl declName
 
 def addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (showInfo := false) : MetaM Unit := do
-  if thmKind == .eqLhs then
+  match thmKind with
+  | .eqLhs _ =>
     addGrindEqAttr declName attrKind thmKind (useLhs := true) (showInfo := showInfo)
-  else if thmKind == .eqRhs then
+  | .eqRhs _ =>
     addGrindEqAttr declName attrKind thmKind (useLhs := false) (showInfo := showInfo)
-  else if thmKind == .eqBoth then
+  | .eqBoth _ =>
     addGrindEqAttr declName attrKind thmKind (useLhs := true) (showInfo := showInfo)
     addGrindEqAttr declName attrKind thmKind (useLhs := false) (showInfo := showInfo)
-  else
+  | _ =>
     let info ← getConstInfo declName
     if !wasOriginallyTheorem (← getEnv) declName && !info.isCtor && !info.isAxiom then
       addGrindEqAttr declName attrKind thmKind (showInfo := showInfo)

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

@@ -78,7 +78,7 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
   if let some thm ← mkEMatchTheoremWithKind'? origin proof .rightLeft then
     activateTheorem thm gen
   if (← get).ematch.newThms.size == size then
-    if let some thm ← mkEMatchTheoremWithKind'? origin proof .default then
+    if let some thm ← mkEMatchTheoremWithKind'? origin proof (.default false) then
       activateTheorem thm gen
   if (← get).ematch.newThms.size == size then
     reportIssue! "failed to create E-match local theorem for{indentExpr e}"

src/Lean/Meta/Tactic/Try/Collect.lean

@@ -111,7 +111,7 @@ def saveLibSearchCandidates (e : Expr) : M Unit := do
     for (declName, declMod) in (← libSearchFindDecls e) do
       unless (← Grind.isEMatchTheorem declName) do
         let kind := match declMod with
-          | .none => .default
+          | .none => (.default false)
           | .mp => .leftRight
           | .mpr => .rightLeft
         modify fun s => { s with libSearchResults := s.libSearchResults.insert (declName, kind) }