-- 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
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 (move₂ (fun x => false) aux stack (trNormal fs (trCont k).cons₂)), var := none,
      stk :=
        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) }
    s'

Tactic:
refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_

Result:
case cons₁.intro.intro.refine_2.refine_5.refine_1
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'
⊢ 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) rev =
    []

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'

Proof state:
case halt
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepRet Cont.halt v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont Cont.halt)), var := s, stk := elim (trList v) [] [] (trContStack Cont.halt) } b₂

Tactic:
exact ⟨_, rfl, TransGen.single rfl⟩

Result:
no goals

Proof state:
case cons₁.intro.intro.refine_1
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'
⊢ elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k)) rev = []

Tactic:
rfl

Result:
no goals

Proof state:
case pos.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 = true ∧ (trList v).tail = trList v.tail
c : Cfg'
h₁ : TrCfg (stepRet k v.tail) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (Λ'.ret (trCont k)), var := (trList v).head?, stk := elim (trList v.tail) [] [] (trContStack k) } c
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux (tr (Λ'.ret (trCont (Cont.fix f k)))) s (elim (trList v) [] [] (trContStack (Cont.fix f k)))) c

Tactic:
rw [trCont, tr]

Result:
case pos.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 = true ∧ (trList v).tail = trList v.tail
c : Cfg'
h₁ : TrCfg (stepRet k v.tail) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (Λ'.ret (trCont k)), var := (trList v).head?, stk := elim (trList v.tail) [] [] (trContStack k) } c
⊢ 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))))
    c

Proof state:
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 ∧
      trList v.tail = [])
    (fun a =>
      natEnd a = true ∧
        update (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail main =
          (trNat v.headI).tail ++ a :: trList v.tail)
    (some Γ'.cons)

Tactic:
exact ⟨rfl, this.2⟩

Result:
no goals