wip

GoldbachTm/Tm31/Prime.lean

@@ -178,10 +178,41 @@ cases lb' with (simp! [*, -nth_cfg] at g; simp_all)
               rw [List.replicate_add] at g
               simp! [*, -nth_cfg] at g
               apply rec7 at g
-              forward g g (16 + m + k + i + j + rb + lb' * 2 + la'+ (2 + lb' + la' - 1) + 1)
-              forward g g (18 + m + k + i + j + rb + lb' * 2 + la'+ (2 + lb' + la' - 1))
-              forward g g (19 + m + k + i + j + rb + lb' * 2 + la'+ (2 + lb' + la' - 1))
-              all_goals sorry
+              have h : 2+lb'+la'-1=1+lb'+la' := by omega
+              rw [h] at g
+              forward g g (16 + m + k + i + j + rb + lb' * 2 + la'+ (1 + lb' + la') + 1)
+              forward g g (19 + m + k + i + j + rb + lb' * 3 + la'*2)
+              rw [List.replicate_add] at g
+              rw [List.replicate_add] at g
+              simp! [*, -nth_cfg] at g
+              apply rec9 at g
+              forward g g (20 + m + k + i + j + rb + lb' * 3 + la' * 2 + (1 + lb' + la' - 1) + 1)
+              rw [ List.append_cons ] at g
+              rw [← List.replicate_succ'] at g
+              apply lemma_11_to_12 at g
+              obtain ⟨n, g⟩ := g
+              use (n + (22 + m + k + j + rb + lb' * 3 + la' * 2 + (1 + lb' + la' - 1)))
+              ring_nf at *
+              rw [g]
+              any_goals apply congr
+              any_goals rfl
+              any_goals apply congr
+              any_goals rfl
+              any_goals apply congr
+              any_goals rfl
+              any_goals apply congr
+              any_goals rfl
+              any_goals apply congr
+              any_goals rfl
+              any_goals apply congr
+              any_goals rfl
+              any_goals apply congr
+              any_goals rfl
+              any_goals apply congr
+              any_goals rfl
+              any_goals apply congr
+              any_goals rfl
+              omega
 
 -- r1 : count of 1 on the right
 theorem lemma_23 : ∀ (i r1: ℕ) (l r : List Γ),