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

Proof state:
case cons
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
s : Option Γ'
n : ℕ
tail✝ : List ℕ
⊢ if (n :: tail✝).headI = 0 then
    natEnd (trList (n :: tail✝)).head?.iget = true ∧ (trList (n :: tail✝)).tail = trList (n :: tail✝).tail
  else
    natEnd (trList (n :: tail✝)).head?.iget = false ∧
      (trList (n :: tail✝)).tail = (trNat (n :: tail✝).headI).tail ++ Γ'.cons :: trList (n :: tail✝).tail

Tactic:
rcases n with - | n

Result:
case cons.zero
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
s : Option Γ'
tail✝ : List ℕ
⊢ if (0 :: tail✝).headI = 0 then
    natEnd (trList (0 :: tail✝)).head?.iget = true ∧ (trList (0 :: tail✝)).tail = trList (0 :: tail✝).tail
  else
    natEnd (trList (0 :: tail✝)).head?.iget = false ∧
      (trList (0 :: tail✝)).tail = (trNat (0 :: tail✝).headI).tail ++ Γ'.cons :: trList (0 :: tail✝).tail

case cons.succ
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if ((n + 1) :: tail✝).headI = 0 then
    natEnd (trList ((n + 1) :: tail✝)).head?.iget = true ∧
      (trList ((n + 1) :: tail✝)).tail = trList ((n + 1) :: tail✝).tail
  else
    natEnd (trList ((n + 1) :: tail✝)).head?.iget = false ∧
      (trList ((n + 1) :: tail✝)).tail =
        (trNat ((n + 1) :: tail✝).headI).tail ++ Γ'.cons :: trList ((n + 1) :: tail✝).tail

Proof state:
case h.e'_2.h.e'_7
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this : natEnd (trList v).head?.iget = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.fix f k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
    s'
⊢ elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) =
    update (update (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail) main
      ?neg.intro.intro.convert_6✝

Tactic:
simp

Result:
case h.e'_2.h.e'_7
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this : natEnd (trList v).head?.iget = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.fix f k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
    s'
⊢ elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) =
    elim ?neg.intro.intro.convert_6✝ [] [] (trContStack (Cont.fix f k))

Proof state:
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
⊢ if v.headI = 0 then natEnd (trList v).head?.iget = true ∧ (trList v).tail = trList v.tail
  else natEnd (trList v).head?.iget = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail

Tactic:
obtain - | n := v

Result:
case nil
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
s : Option Γ'
⊢ if [].headI = 0 then natEnd (trList []).head?.iget = true ∧ (trList []).tail = trList [].tail
  else natEnd (trList []).head?.iget = false ∧ (trList []).tail = (trNat [].headI).tail ++ Γ'.cons :: trList [].tail

case cons
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
s : Option Γ'
n : ℕ
tail✝ : List ℕ
⊢ if (n :: tail✝).headI = 0 then
    natEnd (trList (n :: tail✝)).head?.iget = true ∧ (trList (n :: tail✝)).tail = trList (n :: tail✝).tail
  else
    natEnd (trList (n :: tail✝)).head?.iget = false ∧
      (trList (n :: tail✝)).tail = (trNat (n :: tail✝).headI).tail ++ Γ'.cons :: trList (n :: tail✝).tail

Proof state:
case neg.intro.intro
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this : natEnd (trList v).head?.iget = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.fix f k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
    s'
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux
      (pop' main
        (goto fun s =>
          bif natEnd s.iget then Λ'.ret (trCont k) else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      s (elim (trList v) [] [] (trContStack (Cont.fix f k))))
    { l := some (trNormal f (Cont'.fix f (trCont k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }

Tactic:
simp only [pop', TM2.stepAux, elim_main, this.1]

Result:
case neg.intro.intro
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this : natEnd (trList v).head?.iget = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.fix f k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
    s'
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    { l := some (bif false then Λ'.ret (trCont k) else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))),
      var := (trList v).head?, stk := update (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail }
    { l := some (trNormal f (Cont'.fix f (trCont k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }