grind: cannot teach grind that (¬(x = none)) -> (∃ y, x = some y)

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

grind cannot prove (¬(x = none)) -> (∃ y, x = some y). Moreover, it is impossible to teach grind this reasoning principle, such that it can use it in bigger proofs.

I have some big theorem I want to prove (I don't share it, but I can share it if you want), and this big theorem requires to prove (¬(x = none)) -> (∃ y, x = some y) as one of its steps. I hoped that grind will be able to prove whole theorem, but, unfortunately, because of this step grind was unable to prove the theorem, and thus I had to resort to big proof with many steps.

Let me describe this issue in more details: grind cannot prove (¬(f x = none)) -> (∃ y, f x = some y) (note f x here) and this is impossible to teach grind principle (¬(x = none)) -> (∃ y, x = some y) (note lack of f x here) in such way that grind can use it to prove (¬(f x = none)) -> (∃ y, f x = some y).

Here are some my attempts. In all these attempts I try to teach grind (¬(x = none)) -> (∃ y, x = some y) and use this to prove (¬(f x = none)) -> (∃ y, f x = some y) using grind.

theorem final_theorem (a : Type) (b : Type) (f : a -> Option b) (x : a) : (f x ≠ none) -> (∃ y, f x = some y) := by grind
-- error: "`grind` failed"

-- Now let's try to teach grind this helper and use it in final theorem:
theorem helper (a : Type) (x : Option a) : (x ≠ none) -> (∃ y, x = some y) := by cases x with grind

theorem final_theorem (a : Type) (b : Type) (f : a -> Option b) (x : a) : (f x ≠ none) -> (∃ y, f x = some y) := by grind [helper]
-- error: "invalid `grind` theorem, failed to find an usable pattern using different modifiers"

@[grind]
theorem helper (a : Type) (x : Option a) : (x ≠ none) -> (∃ y, x = some y) := by cases x with grind
-- error: "invalid `grind` theorem, failed to find an usable pattern using different modifiers"

theorem final_theorem (a : Type) (b : Type) (f : a -> Option b) (x : a) : (f x ≠ none) -> (∃ y, f x = some y) := by grind

@[grind gen]
theorem helper (a : Type) (x : Option a) : (x ≠ none) -> (∃ y, x = some y) := by cases x with grind
-- error: "`@[grind . gen] theorem helper` failed to find patterns, consider using different options or the `grind_pattern` command"

theorem final_theorem (a : Type) (b : Type) (f : a -> Option b) (x : a) : (f x ≠ none) -> (∃ y, f x = some y) := by grind

Similarly nearly all other @[grind] forms (on helper) failed with errors pointing at @[grind] line. They are:

-- @[grind =]
-- @[grind = _]
-- @[grind _ = _]
-- @[grind <- =]
-- @[grind <-]
-- @[grind ->]
-- @[grind =>]
-- @[grind <=]
-- @[grind .]
-- @[grind usr]
-- @[grind cases]
-- @[grind cases eager]
-- @[grind intro]
-- @[grind ext]
-- @[grind inj]
-- @[grind unfold]

The only grind attributes I was able to put on helper are funCC and norm. But I still were unable to prove final_theorem:

@[grind funCC]
theorem helper (a : Type) (x : Option a) : (x ≠ none) -> (∃ y, x = some y) := by cases x with grind

theorem final_theorem (a : Type) (b : Type) (f : a -> Option b) (x : a) : (f x ≠ none) -> (∃ y, f x = some y) := by grind
-- error: "`grind` failed"

@[grind norm]
theorem helper (a : Type) (x : Option a) : (x ≠ none) -> (∃ y, x = some y) := by cases x with grind

theorem final_theorem (a : Type) (b : Type) (f : a -> Option b) (x : a) : (f x ≠ none) -> (∃ y, f x = some y) := by grind
-- error: "`grind` failed"

I also tried this:

attribute [grind cases] Option

theorem final_theorem (a : Type) (b : Type) (f : a -> Option b) (x : a) : (f x ≠ none) -> (∃ y, f x = some y) := by grind
-- error: "`grind` failed"

attribute [grind cases eager] Option

theorem final_theorem (a : Type) (b : Type) (f : a -> Option b) (x : a) : (f x ≠ none) -> (∃ y, f x = some y) := by grind
-- error: "`grind` failed"

You may say: "Just use by cases (f x)". Well, by cases (f x) indeed works. But, as I said previously, in fact I need to prove one big theorem (I can share it if you want), and for this grind needs to prove this ∃-statement somewhere in the middle. And so I want to teach grind to use this ∃-principle, so that I can prove whole theorem by grind.

All this was observed on nightly (4.28.0-nightly-2026-01-04).

(some time passes.)

Okay, while writing this bug report I noticed that this works:

theorem final_theorem (a : Type) (b : Type) (f : a -> Option b) (x : a) : (f x ≠ none) -> (∃ y, f x = some y) := by grind (config := { extAll := true })

So, it seems some theorem misses @[grind ext] attribute. How to debug this?

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal Option example and compare the default grind behavior with config := { extAll := true }. Investigate the grind extensional reasoning path and determine why the helper theorem cannot be registered; done means the default theorem is accepted or the missing rule is precisely identified and covered by a regression test.