fix: panic at reducePow

closes #4947

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

@@ -55,8 +55,9 @@ builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : Nat)) := reduceBin ``HDiv.hDi
 builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Nat)) := reduceBin ``HMod.hMod 6 (· % ·)
 
 builtin_dsimproc [simp, seval] reducePow ((_ ^ _ : Nat)) := fun e => do
-  let some n ← fromExpr? e.appFn!.appArg! | return .continue
-  let some m ← fromExpr? e.appArg! | return .continue
+  let_expr HPow.hPow _ _ _ _ n m := e | return .continue
+  let some n ← fromExpr? n | return .continue
+  let some m ← fromExpr? m | return .continue
   unless (← checkExponent m) do return .continue
   return .done <| toExpr (n ^ m)
 

tests/lean/run/4947.lean

@@ -0,0 +1,6 @@
+universe u
+class G (A : outParam Nat) where Z : Type u
+export G (Z)
+abbrev f (a : Nat) : Nat := 2 ^ a
+variable [G (f 0)]
+example {s : Z} : s = s := by simp only [Nat.reducePow]