-- Mathlib/Computability/TMToPartrec.lean
theorem trNormal_respects (c k v s) :
    ∃ b₂,
      TrCfg (stepNormal c k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          ⟨some (trNormal c (trCont k)), s, K'.elim (trList v) [] [] (trContStack k)⟩ b₂

Proof state:
case case
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepNormal (f.case g) k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
rw [stepNormal]

Result:
case case
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg ((fun k v => Nat.rec (stepNormal f k v.tail) (fun y x => stepNormal g k (y :: v.tail)) v.headI) k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Proof state:
case zero'
k : Cont
v : List ℕ
s : Option Γ'
⊢ { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList (0 :: v)) [] [] (trContStack k) } ∈
    TM2.step tr { l := some (trNormal Code.zero' (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }

Tactic:
simp

Result:
no goals

Proof state:
case case.intro.succ.intro.intro
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s s' : Option Γ'
n : ℕ
h :
  Reaches₁ (TM2.step tr)
    { l := some ((trNormal f (trCont k)).pred (trNormal g (trCont k))), var := s,
      stk := elim (trList v) [] [] (trContStack k) }
    (Nat.rec { l := some (trNormal f (trCont k)), var := s', stk := elim (trList v.tail) [] [] (trContStack k) }
      (fun n x =>
        { l := some (trNormal g (trCont k)), var := s', stk := elim (trList (n :: v.tail)) [] [] (trContStack k) })
      (n + 1))
c : Cfg'
h₁ : TrCfg (stepNormal g k ?m.139777) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal g (trCont k)), var := s', stk := elim (trList ?m.139777) [] [] (trContStack k) } c
⊢ ∃ b₂,
    TrCfg (Nat.rec (stepNormal f k v.tail) (fun y x => stepNormal g k (y :: v.tail)) (n + 1)) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
exact ⟨_, h₁, h.trans h₂⟩

Result:
no goals

Proof state:
case case.intro.zero
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s s' : Option Γ'
h :
  Reaches₁ (TM2.step tr)
    { l := some (Λ'.pred ?m.139559 ?m.139560), var := s, stk := elim (trList v) [] ?m.139561 ?m.139562 }
    (Nat.rec { l := some ?m.139559, var := s', stk := elim (trList v.tail) [] ?m.139561 ?m.139562 }
      (fun n x => { l := some ?m.139560, var := s', stk := elim (trList (n :: v.tail)) [] ?m.139561 ?m.139562 }) 0)
⊢ ∃ b₂,
    TrCfg (Nat.rec (stepNormal f k v.tail) (fun y x => stepNormal g k (y :: v.tail)) 0) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
obtain ⟨c, h₁, h₂⟩ := IHf k _ s'

Result:
case case.intro.zero.intro.intro
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s s' : Option Γ'
h :
  Reaches₁ (TM2.step tr)
    { l := some (Λ'.pred ?m.139559 ?m.139560), var := s, stk := elim (trList v) [] ?m.139561 ?m.139562 }
    (Nat.rec { l := some ?m.139559, var := s', stk := elim (trList v.tail) [] ?m.139561 ?m.139562 }
      (fun n x => { l := some ?m.139560, var := s', stk := elim (trList (n :: v.tail)) [] ?m.139561 ?m.139562 }) 0)
c : Cfg'
h₁ : TrCfg (stepNormal f k ?m.139654) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont k)), var := s', stk := elim (trList ?m.139654) [] [] (trContStack k) } c
⊢ ∃ b₂,
    TrCfg (Nat.rec (stepNormal f k v.tail) (fun y x => stepNormal g k (y :: v.tail)) 0) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Proof state:
case h.e'_4.h.e'_7
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x => some Γ'.cons
⊢ elim (trList v.tail) [] [] (trContStack k) = update (elim (trList v) [] [] (trContStack k)) main ?tail.convert_7

Tactic:
simp

Result:
case h.e'_4.h.e'_7
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x => some Γ'.cons
⊢ elim (trList v.tail) [] [] (trContStack k) = elim ?tail.convert_7 [] [] (trContStack k)