-- 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 intro.intro.intro.intro
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 Γ'
e : [].reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂'
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 }
⊢ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) [] c d }
    { l := some q, var := none, stk := elim (trPosNum a.succ ++ [Γ'.cons]) [] c d }

Tactic:
simp only [List.reverseAux, List.reverseAux_eq] at e

Result:
case intro.intro.intro.intro
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₂'
⊢ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) [] c d }
    { l := some q, var := none, stk := elim (trPosNum a.succ ++ [Γ'.cons]) [] c d }

Proof state:
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 := elim (Γ'.bit1 :: Γ'.cons :: (trNum Num.zero ++ [Γ'.cons]).tail) [] c d }

Tactic:
rfl

Result:
no goals

Proof state:
case pos.one
q : Λ'
n : ℕ
c d : List Γ'
s : Option Γ'
l₁ : List Γ'
⊢ { l := some (unrev q), var := some Γ'.cons, stk := elim ([Γ'.bit1] ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d } ∈
    TM2.step tr (TM2.stepAux (tr q.succ) s (elim (trPosNum PosNum.one ++ [Γ'.cons]) l₁ c d))

Tactic:
simp [trPosNum]

Result:
no goals

Proof state:
case zero
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ TransGen (fun a b => b ∈ TM2.step tr a) (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:
simp only [Option.mem_def, TM2.stepAux, elim_main, decide_false, elim_update_main, ne_eq,
  Function.update_of_ne, elim_rev, elim_update_rev, decide_true, Function.update_self,
  cond_true, cond_false]

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

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

Tactic:
simp only [trNum, Num.succ, Num.succ']

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

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

Tactic:
suffices ∀ l₁, ∃ l₁' l₂' s',
    List.reverseAux l₁ (trPosNum a.succ) = List.reverseAux l₁' l₂' ∧
      Reaches₁ (TM2.step tr) ⟨some q.succ, s, K'.elim (trPosNum a ++ [Γ'.cons]) l₁ c d⟩
        ⟨some (unrev q), s', K'.elim (l₂' ++ [Γ'.cons]) l₁' c d⟩ by
  obtain ⟨l₁', l₂', s', e, h⟩ := this []
  simp? [List.reverseAux] at e says simp only [List.reverseAux, List.reverseAux_eq] at e
  refine h.trans ?_
  convert unrev_ok using 2
  simp [e, List.reverseAux_eq]

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