lean file

leanprover-community · Dec 6, 2023 · 3e8df60 · 3e8df60
1 parent 5dcf4e7
commit 3e8df60
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/test/Mathlib/test/H20231206.lean b/test/Mathlib/test/H20231206.lean
@@ -0,0 +1,16 @@
+import Mathlib
+import Mathlib.Tactic.GoalNormalization.NormalizeHyps
+
+/--
+info: theorem extracted_1 (h0 : ZMod (11 ^ 2)) (h1 : h0 = 24⁻¹) : ∃ k, h0 = k := sorry
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+theorem problem
+    (b :  ZMod (11^2))
+    (h₀ : b = 24⁻¹) :
+    ∃ (k : ZMod (11^2)), b = k := by
+  normalize_hyps
+  extract_goal
+  sorry