fix: simp support for OfNat instances that are functions

closes #4462

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -34,7 +34,7 @@ def Config.updateArith (c : Config) : CoreM Config := do
 
 /-- Return true if `e` is of the form `ofNat n` where `n` is a kernel Nat literal -/
 def isOfNatNatLit (e : Expr) : Bool :=
-  e.isAppOfArity ``OfNat.ofNat 3 && e.appFn!.appArg!.isRawNatLit
+  e.isAppOf ``OfNat.ofNat && e.getAppNumArgs >= 3 && (e.getArg! 1).isRawNatLit
 
 /--
 If `e` is a raw Nat literal and `OfNat.ofNat` is not in the list of declarations to unfold,

tests/lean/run/4462.lean

@@ -0,0 +1,26 @@
+def Matrix (α β R : Type) := α → β → R
+
+instance [DecidableEq α] : OfNat (Matrix α α Nat) 1 where
+  ofNat x y := if x = y then 1 else 0
+
+example [DecidableEq α] (x y : α) (h : x ≠ y) :
+    (1 : Matrix α α Nat) x y = 0 := by
+  guard_target =ₛ (1 : Matrix ..) x y = 0
+  fail_if_success simp
+  guard_target =ₛ (1 : Matrix ..) x y = 0
+  sorry
+
+example [DecidableEq α] (x y : α) (h : x ≠ y) :
+    (1 : Matrix α α Nat) x y = 0 := by
+  guard_target =ₛ (1 : Matrix ..) x y = 0
+  fail_if_success dsimp
+  guard_target =ₛ (1 : Matrix ..) x y = 0
+  sorry
+
+theorem one_eq [DecidableEq α] : (1 : Matrix α α Nat) x x = 1 := by
+  simp [OfNat.ofNat]
+
+example [DecidableEq α] (x y : α) (h : x ≠ y) :
+    (1 : Matrix α α Nat) x y = 0 := by
+  guard_target =ₛ (1 : Matrix ..) x y = 0
+  simp [OfNat.ofNat, h]