feat: grind simple strategy

[leodemoura]

This PR adds a simple strategy to the (WIP) grind tactic. It just keeps internalizing new theorem instances found by E-matching. The simple strategy can solve examples such as:

grind_pattern Array.size_set => Array.set a i v h
grind_pattern Array.get_set_eq  => a.set i v h
grind_pattern Array.get_set_ne => (a.set i v hi)[j]

example (as bs : Array α) (v : α)
        (i : Nat)
        (h₁ : i < as.size)
        (h₂ : bs = as.set i v)
        : as.size = bs.size := by
  grind

example (as bs cs : Array α) (v : α)
        (i : Nat)
        (h₁ : i < as.size)
        (h₂ : bs = as.set i v)
        (h₃ : cs = bs)
        (h₄ : i ≠ j)
        (h₅ : j < cs.size)
        (h₆ : j < as.size)
        : cs[j] = as[j] := by
  grind


opaque R : Nat → Nat → Prop
theorem Rtrans (a b c : Nat) : R a b → R b c → R a c := sorry

grind_pattern Rtrans => R a b, R b c

example : R a b → R b c → R c d → R d e → R a d := by
  grind

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a08379ce2ee540a8733aec0e7b747a0a2608bccf --onto 2c87905d77b707c3283c1de759fd63269ac386a1. (2025-01-02 05:39:40)