-- 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 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 }

Tactic:
refine ⟨Γ'.bit0 :: l₁, _, some a, rfl, TransGen.single ?_⟩

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 := some (unrev q₂), var := some a, stk := elim (trPosNum m ++ Γ'.cons :: trList v) (Γ'.bit0 :: l₁) c d } ∈
    TM2.step tr { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.bit0.succ ++ Γ'.cons :: trList v) l₁ c d }

Proof state:
case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum Num.zero.succ' ++ Γ'.cons :: trList v) [] c d }
    { l := some q₂, var := none,
      stk :=
        elim
          ((match Num.zero with
            | Num.zero => []
            | Num.pos n => trPosNum n) ++
            Γ'.cons :: trList v)
          [] c d }

Tactic:
simp only [trPosNum, Num.succ', List.singleton_append, List.nil_append]

Result:
case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ Reaches₁ (TM2.step tr) { l := some (q₁.pred q₂), var := s, stk := elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d }
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }

Proof state:
case h.e'_2.h.e'_7
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ elim (Γ'.cons :: trList v) [] c d =
    update
      (update
        (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)).stk
        rev [])
      main
      (((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)).stk
            rev).reverseAux
        ((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)).stk
          main))

Tactic:
simp

Result:
no goals