fix tm 31

lengyijun · Nov 17, 2024 · b084c1a · b084c1a
1 parent 1b08d8e
commit b084c1a
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 1 deletion.
diff --git a/GoldbachTm/Tm31/Content.lean b/GoldbachTm/Tm31/Content.lean
@@ -20,6 +20,7 @@ refine (?_ ∘ g) ?_
   use (1+k)
   ring_nf at *
   simp [h]
+  omega
 . obtain ⟨x, y, _, hx, hy⟩ := hpp
   by_cases x ≤ y
   . use! x, y

diff --git a/GoldbachTm/Tm31/Prime.lean b/GoldbachTm/Tm31/Prime.lean
@@ -4,6 +4,7 @@ import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Tm31.Transition
 import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.Data.Nat.ModEq
+import Mathlib.Data.Nat.Prime.Basic
 
 namespace Tm31
 

diff --git a/GoldbachTm/Tm31/TuringMachine31.lean b/GoldbachTm/Tm31/TuringMachine31.lean
@@ -1,6 +1,6 @@
 -- inspired by https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Computability/TuringMachine.lean
 import Mathlib.Computability.TuringMachine
-import Mathlib.Data.Real.Sqrt
+import Mathlib.Tactic.Ring.RingNF
 import GoldbachTm.Basic
 import GoldbachTm.Format
 import GoldbachTm.ListBlank