From b084c1ac02b7e9afaf5f9688e59052e6ba592667 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Sun, 17 Nov 2024 09:15:17 +0800
Subject: [PATCH] fix tm 31

---
 GoldbachTm/Tm31/Content.lean         | 1 +
 GoldbachTm/Tm31/Prime.lean           | 1 +
 GoldbachTm/Tm31/TuringMachine31.lean | 2 +-
 3 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/GoldbachTm/Tm31/Content.lean b/GoldbachTm/Tm31/Content.lean
index 2e674ae..a9cb35c 100644
--- 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
index 6bd6fbf..fccc23a 100644
--- 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
index 6ccb8c4..61c529a 100644
--- 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