what

leanprover-community · Dec 6, 2023 · 5e411e9 · 5e411e9
1 parent 1a3826e
commit 5e411e9
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/test/Mathlib/test/H20231206.in 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 }