possible grind regression?

Stream: lean4

[Damiano Testa]

I do not know if this has been reported before, but the following is a minimised example of something that used to work.

example (a b : Nat) (f g : Nat → Nat)
    -- This superfluous hypothesis trips up `grind`
    (hf : (∀ i ≤ a, f i ≤ f (i + 1)) ∧ f 0 = 0)
    (hg : (∀ i ≤ b, g i ≤ g (i + 1)) ∧ g 0 = 0 ∧ g b = 0) :
    g (a + b - a) = 0 := by
  try grind
  simp_all -- used to be `grind`

If you use "Latest Mathlib" in the online server, try grind does nothing and simp_all solves the goal, but with "Mathlib v.24", grind solves the goal.

[Jireh Loreaux]

Indeed, there's another one here: #mathlib4 > `simp only` + `grind` failure

[Damiano Testa]

Yes, also your example looks like it sends grind on a case-split chase and then it gives up.