fix: spurious warning message in grind

This PR fixes a spurious warning message in `grind`.

Closes #10670

src/Lean/Elab/Tactic/Grind/Main.lean

@@ -185,7 +185,8 @@ where
           -- 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 id ctor (.default false) minIndexable
+            -- **Note**: We should not warn if `declName` is an inductive
+            params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable (warn := False)
       else
         params ← withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true)
     | .symbol prio =>
@@ -195,7 +196,7 @@ where
 
   addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Name)
       (kind : Grind.EMatchTheoremKind)
-      (minIndexable : Bool) (suggest : Bool := false) : MetaM Grind.Params := do
+      (minIndexable : Bool) (suggest : Bool := false) (warn := true) : MetaM Grind.Params := do
     let info ← getAsyncConstInfo declName
     match info.kind with
     | .thm | .axiom | .ctor =>
@@ -204,7 +205,8 @@ where
         ensureNoMinIndexable minIndexable
         let thm₁ ← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios
         let thm₂ ← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios
-        if params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns &&
+        if warn &&
+           params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns &&
            params.ematch.containsWithSamePatterns thm₂.origin thm₂.patterns then
           warnRedundantEMatchArg params.ematch declName
         return { params with extra := params.extra.push thm₁ |>.push thm₂ }
@@ -215,7 +217,7 @@ where
           Grind.mkEMatchTheoremAndSuggest id declName params.symPrios minIndexable (isParam := true)
         else
           Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable)
-        if params.ematch.containsWithSamePatterns thm.origin thm.patterns then
+        if warn && params.ematch.containsWithSamePatterns thm.origin thm.patterns then
           warnRedundantEMatchArg params.ematch declName
         return { params with extra := params.extra.push thm }
     | .defn =>

tests/lean/run/grind_10670.lean

@@ -0,0 +1,11 @@
+inductive Foo : Nat → Prop
+  | one : Foo 1
+  | two : Foo 2
+
+attribute [grind ·] Foo.one
+
+#guard_msgs in
+example {l : Nat} (hl : Foo l) : Foo (3 - l) := by
+  induction hl with
+  | one => grind [Foo]
+  | two => grind