simpler proof

GoldbachTm/Tm31/Transition.lean

@@ -2,26 +2,20 @@ import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Tm31.Search0
 
 theorem lemma_12_to_13 (i : ℕ) (r1: ℕ) (l r : List Γ)
-(g :
+(h :
 nth_cfg i = some ⟨⟨12, by omega⟩, ⟨Γ.zero,
   Turing.ListBlank.mk l,
   Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩) :
 
 ∃ j, nth_cfg (i + j) = some ⟨⟨13, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩
 := by
-have h : nth_cfg (i + 1) = nth_cfg (i + 1) := rfl
-nth_rewrite 2 [nth_cfg] at h
-simp [g, step, Option.map, machine, Turing.Tape.write, Turing.Tape.move] at h
-clear g
+forward h h i
 
 cases r1 with
 | zero => use 1
           rw [h]
           rfl
-| succ r1 => have g := rec13 r1 (i+1) (List.cons Γ.zero l) r
+| succ r1 => apply rec13 at h
              use (r1 + 2)
-             have h1 : i + 1 + r1 + 1 = i + (r1 + 2) := by omega
-             rw [h1] at g
-             apply g
-             rw [h]
-             constructor
+             have g : i + (r1 + 2) = i + 1 + r1 + 1 := by omega
+             rw [g, h]