grind funCC の使い方

Here's a situation where grind fails to solve a goal involving function equalities.

def Φ : (Nat → Nat) → (Nat → Nat) := id

example (f g : Nat → Nat) (h : Φ f = Φ g) (a : Nat) : Φ f a = Φ g a := by
  grind -- fails

example (f g : Nat → Nat) (h : Φ f = Φ g) (a : Nat) : Φ f a = Φ g a := by
  grind [Φ] -- fails

example (f g : Nat → Nat) (h : Φ f = Φ g) (a : Nat) : Φ f a = Φ g a := by
  rw [h] -- succeeds
  -- apply congrFun ‹_› -- also succeeds

example (f g : Nat → Nat) (h : Φ f = Φ g) (a : Nat) : Φ f a = Φ g a := by
  grind only [funext_iff (f := Φ f) (g := Φ g)] -- succeeds

example (f g : Nat → Nat) (h : f = g) (a : Nat) : Φ f a = Φ g a := by
  grind only -- succeeds

こういうのを証明できるようになる

Start by reproducing the two failing grind examples in the issue, then compare them with the succeeding rw, congrFun, and funext_iff examples. Trace how grind handles equalities between functions and determine what is needed so the first two examples are provable; done means those examples succeed without the explicit workaround.