From e648a3489e8e24cca3f72037f231c2ec6753ae9c Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Sun, 13 Oct 2024 10:49:18 +0800
Subject: [PATCH] typo

---
 GoldbachTm/Tm31/Prime.lean | 11 +++--------
 1 file changed, 3 insertions(+), 8 deletions(-)

diff --git a/GoldbachTm/Tm31/Prime.lean b/GoldbachTm/Tm31/Prime.lean
index a12b5a1..0902866 100644
--- a/GoldbachTm/Tm31/Prime.lean
+++ b/GoldbachTm/Tm31/Prime.lean
@@ -99,18 +99,13 @@ induction rb with intros i la lb ra l r g hm
               obtain ⟨j, la', lb', g, h₁, h₂⟩ := g
               apply induction_step at g
               rw [← h₂] at g
-              have h : ra + 1 + 2 = ra + 3 := by omega
-              rw [h] at g
+              ring_nf at *
               specialize g h₁
               obtain ⟨k, la'', lb'', g, h₃, h₄⟩ := g
               use! (j+k), la'', lb''
+              ring_nf at *
               repeat any_goals constructor
-              any_goals tauto
-              . rw [← Nat.add_assoc i, g]
-                repeat any_goals first | omega | rfl | apply congr
-              . have h : ra + (rb + 1) +2 = ra + 1 + rb + 2:= by omega
-                rw [h]
-                assumption
+              all_goals tauto
 
 --    l 0 1 0  [lb 11]    0  0  [(rb+1) 1] 0 r
 --          c1            ^  c2