-- 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 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 Γ'
⊢ (bif decide ((trPosNum m.bit0 ++ [Γ'.cons]).head? = some Γ'.bit1) then
      { l := some q.succ, var := (trPosNum m.bit0 ++ [Γ'.cons]).head?,
        stk := elim (trPosNum m.bit0 ++ [Γ'.cons]).tail (Γ'.bit0 :: l₁) c d }
    else
      bif decide ((trPosNum m.bit0 ++ [Γ'.cons]).head? = some Γ'.cons) then
        { l := some (unrev q), var := (trPosNum m.bit0 ++ [Γ'.cons]).head?,
          stk := elim (Γ'.bit1 :: Γ'.cons :: (trPosNum m.bit0 ++ [Γ'.cons]).tail) l₁ c d }
      else
        { l := some (unrev q), var := (trPosNum m.bit0 ++ [Γ'.cons]).head?,
          stk := elim (Γ'.bit1 :: (trPosNum m.bit0 ++ [Γ'.cons]).tail) l₁ c d }) =
    { l := some (unrev q), var := some Γ'.bit0, stk := elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d }

Tactic:
rfl

Result:
no goals

Proof state:
case pos.bit1.intro.intro.intro.intro
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₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr)
    { l := some q.succ, var := ?m.108487, stk := elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d }
    { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
⊢ ∃ 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 }

Tactic:
refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩

Result:
case pos.bit1.intro.intro.intro.intro
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₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr)
    { l := some q.succ, var := ?m.108487, stk := elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d }
    { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
⊢ { l := some q.succ, var := ?m.108487, stk := elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d } ∈
    TM2.step tr { l := some q.succ, var := s, stk := elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d }

Proof state:
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 }
⊢ 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:
obtain ⟨l₁', l₂', s', e, h⟩ := this []

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

Proof state:
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 }

Tactic:
refine ⟨Γ'.bit0 :: l₁, [Γ'.bit1], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩

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

Proof state:
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 := some (unrev q), var := some Γ'.bit0, stk := elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d } ∈
    some (TM2.stepAux (tr q.succ) s (elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d))

Tactic:
rw [tr]

Result:
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 := some (unrev q), var := some Γ'.bit0, stk := elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d } ∈
    some
      (TM2.stepAux
        (pop' main
          (branch (fun s => decide (s = some Γ'.bit1)) (push rev (fun x => Γ'.bit0) (goto fun x => q.succ))
            (branch (fun s => decide (s = some Γ'.cons))
              (push main (fun x => Γ'.cons) (push main (fun x => Γ'.bit1) (goto fun x => unrev q)))
              (push main (fun x => Γ'.bit1) (goto fun x => unrev q)))))
        s (elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d))

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

Tactic:
rcases (n : Num) with - | a

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

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 }