-- Mathlib/Computability/TMToPartrec.lean
theorem pred_ok (q₁ q₂ s v) (c d : List Γ') : ∃ s',
    Reaches₁ (TM2.step tr) ⟨some (Λ'.pred q₁ q₂), s, K'.elim (trList v) [] c d⟩
      (v.headI.rec ⟨some q₁, s', K'.elim (trList v.tail) [] c d⟩ fun n _ =>
        ⟨some q₂, s', K'.elim (trList (n::v.tail)) [] c d⟩)

Proof state:
case h.e'_2.h.e'_7
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d }
    { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ elim (trPosNum a ++ Γ'.cons :: trList v) [] c d =
    update (update (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d) rev []) main
      ((elim (l₂' ++ Γ'.cons :: trList v) l₁' c d rev).reverseAux (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d main))

Tactic:
simp [e, List.reverseAux_eq]

Result:
no goals

Proof state:
case cons.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
⊢ Nat.rec { l := some q₁, var := some Γ'.cons, stk := elim (trList (0 :: v).tail) [] c d }
      (fun n x => { l := some q₂, var := some Γ'.cons, stk := elim (trList (n :: (0 :: v).tail)) [] c d })
      (0 :: v).headI ∈
    TM2.step tr { l := some (q₁.pred q₂), var := s, stk := elim (trList (0 :: v)) [] c d }

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux (tr (q₁.pred q₂)) s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }

Tactic:
rw [tr]

Result:
case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux
      (pop' main
        (branch (fun s => decide (s = some Γ'.bit0)) (push rev (fun x => Γ'.bit1) (goto fun x => q₁.pred q₂))
          (branch (fun s => natEnd s.iget) (goto fun x => q₁)
            (peek' main
              (branch (fun s => natEnd s.iget) (goto fun x => unrev q₂)
                (push rev (fun x => Γ'.bit0) (goto fun x => unrev q₂)))))))
      s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }

Proof state:
case cons.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
⊢ ∃ s',
    Reaches₁ (TM2.step tr) { l := some (q₁.pred q₂), var := s, stk := elim (trList (0 :: v)) [] c d }
      (Nat.rec { l := some q₁, var := s', stk := elim (trList (0 :: v).tail) [] c d }
        (fun n x => { l := some q₂, var := s', stk := elim (trList (n :: (0 :: v).tail)) [] c d }) (0 :: v).headI)

Tactic:
refine ⟨some Γ'.cons, TransGen.single ?_⟩

Result:
case cons.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
⊢ Nat.rec { l := some q₁, var := some Γ'.cons, stk := elim (trList (0 :: v).tail) [] c d }
      (fun n x => { l := some q₂, var := some Γ'.cons, stk := elim (trList (n :: (0 :: v).tail)) [] c d })
      (0 :: v).headI ∈
    TM2.step tr { l := some (q₁.pred q₂), var := s, stk := elim (trList (0 :: v)) [] c d }

Proof state:
case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux
      (pop' main
        (branch (fun s => decide (s = some Γ'.bit0)) (push rev (fun x => Γ'.bit1) (goto fun x => q₁.pred q₂))
          (branch (fun s => natEnd s.iget) (goto fun x => q₁)
            (peek' main
              (branch (fun s => natEnd s.iget) (goto fun x => unrev q₂)
                (push rev (fun x => Γ'.bit0) (goto fun x => unrev q₂)))))))
      s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }

Tactic:
simp only [pop', TM2.stepAux, cond_false]

Result:
case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
      { l := some (q₁.pred q₂), var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
        stk :=
          update
            (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
              (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
            rev
            (Γ'.bit1 ::
              update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail rev) }
    else
      bif natEnd (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?.iget then
        { l := some q₁, var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
          stk :=
            update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
              (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail }
      else
        TM2.stepAux
          (peek' main
            (branch (fun s => natEnd s.iget) (goto fun x => unrev q₂)
              (push rev (fun x => Γ'.bit0) (goto fun x => unrev q₂))))
          (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
          (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
            (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail))
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }

Proof state:
case cons.succ.pos.bit0
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
s : Option Γ'
l₁ : List Γ'
⊢ ∃ l₁' l₂' s',
    l₁.reverseAux (trPosNum m.bit0) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step tr)
        { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.bit0.succ ++ Γ'.cons :: trList v) l₁ c d }
        { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }

Tactic:
obtain ⟨a, l, e, h⟩ : ∃ a l, (trPosNum m = a::l) ∧ natEnd a = false := by
  cases m <;> refine ⟨_, _, rfl, rfl⟩

Result:
case cons.succ.pos.bit0.intro.intro.intro
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
s : Option Γ'
l₁ : List Γ'
a : Γ'
l : List Γ'
e : trPosNum m = a :: l
h : natEnd a = false
⊢ ∃ l₁' l₂' s',
    l₁.reverseAux (trPosNum m.bit0) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step tr)
        { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.bit0.succ ++ Γ'.cons :: trList v) l₁ c d }
        { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }