-- 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₁.intro.intro.refine_2.refine_5.refine_2
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    { l := some (trNormal fs (trCont k).cons₂), var := none,
      stk :=
        update
          (update
            (update
              (update (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
                ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
              main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main))
            aux (none.elim id List.cons []))
          stack
          (update
              (update (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
                ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
              main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) aux ++
            update
              (update (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
                ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
              main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) stack) }
    s'

Tactic:
simp only [TM2.step, Option.mem_def, Option.elim, elim_update_stack, elim_main,
  List.append_nil, elim_update_main,  id_eq, elim_update_aux, ne_eq, Function.update_of_ne,
  elim_aux, elim_stack]

Result:
case cons₁.intro.intro.refine_2.refine_5.refine_2
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ TransGen
    (fun a b =>
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some (trNormal fs (trCont k).cons₂), var := none,
      stk := elim (trList as) [] [] (trList v ++ Γ'.consₗ :: trLList (contStack k)) }
    s'

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)
    { 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)) }

Tactic:
convert clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _) using 2

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)) =
    update (update (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail) main
      ?neg.intro.intro.convert_6✝

case neg.intro.intro.convert_6
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'
⊢ List Γ'

case neg.intro.intro.convert_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'
⊢ ∀ x ∈ (trNat v.headI).tail, natEnd x = false

case neg.intro.intro.convert_8
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'
⊢ Option.elim'
    (update (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail main = (trNat v.headI).tail ∧
      ?neg.intro.intro.convert_6✝ = [])
    (fun a =>
      natEnd a = true ∧
        update (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail main =
          (trNat v.headI).tail ++ a :: ?neg.intro.intro.convert_6✝)
    (some Γ'.cons)