fix: PANIC at Fin.isValue

closes #4983

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean

@@ -64,8 +64,9 @@ builtin_dsimproc [simp, seval] reduceBNe  (( _ : Fin _) != _)  := reduceBoolPred
 
 /-- Simplification procedure for ensuring `Fin` literals are normalized. -/
 builtin_dsimproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
+  let_expr OfNat.ofNat _ m _ ← e | return .continue
   let some ⟨n, v⟩ ← getFinValue? e | return .continue
-  let some m ← getNatValue? e.appFn!.appArg! | return .continue
+  let some m ← getNatValue? m | return .continue
   if n == m then
     -- Design decision: should we return `.continue` instead of `.done` when simplifying.
     -- In the symbolic evaluator, we must return `.done`, otherwise it will unfold the `OfNat.ofNat`

tests/lean/run/4983.lean

@@ -0,0 +1 @@
+example : (@& (1 : Fin 2)) = 1 := by simp only [Fin.isValue]