From 5e411e95418501c98a3348b020eb64f18173e45e Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 7 Dec 2023 04:16:04 +1100
Subject: [PATCH] what

---
 test/Mathlib/test/H20231206.in | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test/Mathlib/test/H20231206.in

diff --git a/test/Mathlib/test/H20231206.in b/test/Mathlib/test/H20231206.in
new file mode 100644
index 0000000..38f78d2
--- /dev/null
+++ b/test/Mathlib/test/H20231206.in
@@ -0,0 +1,4 @@
+{"cmd": "import Mathlib\nimport Mathlib.Tactic.GoalNormalization.NormalizeHyps"}
+
+{"cmd": "theorem problem\n    (b :  ZMod (11^2))\n    (h₀ : b = 24⁻¹) :\n    ∃ (k : ZMod (11^2)), b = k := by\n  normalize_hyps\n  extract_goal\n  sorry",
+  "env": 0 }