From 7d7447563d4197a02c85462d984f67a56093f65d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 12 Aug 2024 02:20:29 +0200
Subject: [PATCH] fix: panic at `reducePow` (#4988)

closes #4947
---
 src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean | 5 +++--
 tests/lean/run/4947.lean                           | 6 ++++++
 2 files changed, 9 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/4947.lean

diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
index f71e70228345..fe9bd495aadc 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
+++ b/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)
 
diff --git a/tests/lean/run/4947.lean b/tests/lean/run/4947.lean
new file mode 100644
index 000000000000..9ac85f4205a7
--- /dev/null
+++ b/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]