typo

lengyijun · Oct 13, 2024 · 9177965 · 9177965
1 parent 8798556
commit 9177965
Showing 1 changed file with 11 additions and 8 deletions.
diff --git a/GoldbachTm/Tm31/Transition.lean b/GoldbachTm/Tm31/Transition.lean
@@ -16,8 +16,8 @@ cases r1 with
           simp [h]
 | succ r1 => apply rec13 at h
              use (r1 + 2)
-             have g : r1 + 2+i = 1 + i + r1 + 1 := by omega
-             rw [g, h]
+             rw [← h]
+             ring_nf
 
 theorem lemma_8_to_9 (i : ℕ) (l1: ℕ) (l r : List Γ)
 (h :
@@ -37,9 +37,10 @@ cases l1 with
           simp [h]
 | succ l1 => apply rec9 at h
              use (l1 + 2)
-             have g : l1 + 2+i = 1+i +l1 + 1 := by omega
-             simp [g, h]
+             ring_nf at *
+             simp [h]
              rw [List.append_cons, ← List.replicate_succ']
+             ring_nf
 
 theorem lemma_11_to_12 (i : ℕ) (r1: ℕ) (l r : List Γ)
 (h :
@@ -59,8 +60,8 @@ cases r1 with
 | succ r1 =>  simp! [*, -nth_cfg] at h
               apply rec12 at h
               use (r1+2)
-              have g : r1 + 2+i = 1+i +r1 + 1 := by omega
-              simp [g, h]
+              ring_nf at *
+              simp [h]
 
 theorem lemma_17_to_20 (i : ℕ) (l1: ℕ) (l r : List Γ)
 (h :
@@ -79,5 +80,7 @@ cases l1 with simp! [*, -nth_cfg] at h
           simp [h]
 | succ r1 =>  apply rec20 at h
               use (r1+2)
-              have g : r1 + 2+i = 1+i +r1 + 1 := by omega
-              simp [g, h, List.replicate_succ' (r1+1)]
+              ring_nf at *
+              simp [h]
+              rw [List.append_cons, ← List.replicate_succ']
+              ring_nf