grind and coercions

Stream: mathlib4

[Yuval Filmus]

The grind tactic seems easily confused by coercions, for example:

example {n m : ℕ} (h : (n : WithBot ℕ) < m) : n < m := by grind
example {n m : ℕ} (h : (n : WithBot ℕ) < m) : n < m := by grind [WithBot.coe_lt_coe]
example {n m : ℕ} (h : (n : WithBot ℕ) < m) : n < m := WithBot.coe_lt_coe.mp h

example {n m : ℕ} (h : m ≤ n) : m * π / n ≤ π := by grind
example {n m : ℕ} (h : m ≤ n) : m * π / n ≤ π := by
  by_cases! n = 0
  case pos hn => rw [hn, Nat.cast_zero, div_zero]; positivity
  case neg hn => trans n * π / n; { gcongr }; aesop

All grind invocations fail.
This is a bit annoying.
Is there an easy fix?

[Damiano Testa]

The first three work with

attribute [grind =] Nat.cast_lt

[Yuval Filmus]

There are scores, perhaps hundreds of casting lemmas.
Should we just add appropriate grind attributes to all of them?

[Damiano Testa]

I do not know what the plans for grind and coercions are, but here is a slightly different approach to the final proof that also pushes grind a little further by extra tagging. In this case, I do not know whether grind is even expected to close the goal with no further hints, though.

import Mathlib

attribute [grind =] Nat.cast_le
attribute [grind ·] Real.pi_nonneg

open Real

example {n m : ℕ} (h : m ≤ n) : m * π / n ≤ π := by
  obtain rfl | hn := eq_or_ne n 0
  · grind
  · field_simp
    grind

[Jovan Gerbscheid]

The last example doesn't count as linear arithmetic (since π is counted as a variable), so it is not yet supported by grind.