-- Mathlib/Computability/TMToPartrec.lean
theorem succ_ok {q s n} {c d : List Γ'} :
    Reaches₁ (TM2.step tr) ⟨some (Λ'.succ q), s, K'.elim (trList [n]) [] c d⟩
      ⟨some q, none, K'.elim (trList [n.succ]) [] c d⟩

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

Tactic:
convert unrev_ok using 1

Result:
case h.e'_2
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ { l := some q, var := none, stk := elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d } =
    { l := some q, var := none,
      stk :=
        update
          (update
            (update
              (update
                (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                  (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                main
                ((fun x => Γ'.cons) ((fun x v => v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
              main
              ((fun x => Γ'.bit1) ((fun x v => v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update
                  (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                  main
                  ((fun x => Γ'.cons) ((fun x v => v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                    update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                  main))
            rev [])
          main
          ((update
                (update
                  (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                  main
                  ((fun x => Γ'.cons) ((fun x v => v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                    update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
                main
                ((fun x => Γ'.bit1) ((fun x v => v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update
                    (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                    main
                    ((fun x => Γ'.cons) ((fun x v => v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                      update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                        (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                    main)
                rev).reverseAux
            (update
              (update
                (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                  (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                main
                ((fun x => Γ'.cons) ((fun x v => v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
              main
              ((fun x => Γ'.bit1) ((fun x v => v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update
                  (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                  main
                  ((fun x => Γ'.cons) ((fun x v => v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                    update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                  main)
              main)) }

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

Tactic:
simp [e, List.reverseAux_eq]

Result:
no goals

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

Tactic:
induction' a with m IH m _ generalizing s <;> intro l₁

Result:
case pos.one
q : Λ'
n : ℕ
c d : List Γ'
s : Option Γ'
l₁ : List Γ'
⊢ ∃ l₁' l₂' s',
    l₁.reverseAux (trPosNum PosNum.one.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum PosNum.one ++ [Γ'.cons]) l₁ c d }
        { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }

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

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