-- Mathlib/Computability/TMConfig.lean
theorem cont_eval_fix {f k v} (fok : Code.Ok f) :
    Turing.eval step (stepNormal f (Cont.fix f k) v) =
      f.fix.eval v >>= fun v => Turing.eval step (Cfg.ret k v)

Proof state:
case mp.halt
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
this : Cfg.halt v' ∈ eval step (stepNormal f Cont.halt v)
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
rw [fok, Part.bind_eq_bind, Part.mem_bind_iff] at this

Result:
case mp.halt
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
this : ∃ a ∈ f.eval v, Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt a)
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)

Proof state:
case mp.halt
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
this : ∃ a ∈ f.eval v, Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt a)
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
obtain ⟨v'', h₁, h₂⟩ := this

Result:
case mp.halt.intro.intro
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
v'' : List ℕ
h₁ : v'' ∈ f.eval v
h₂ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v'')
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)

Proof state:
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
⊢ Reaches step (stepNormal f Cont.halt v'.tail) (stepRet k₀ v₀)

Tactic:
apply ReflTransGen.single

Result:
case hab
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
⊢ stepRet k₀ v₀ ∈ step (stepNormal f Cont.halt v'.tail)

Proof state:
case neg.intro.intro.intro.intro.intro.intro
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v'.tail
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
⊢ Sum.inl v₂ ∈ Part.map (fun v => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v'.tail) ∨
    ∃ a',
      Sum.inr a' ∈ Part.map (fun v => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v'.tail) ∧
        v₂ ∈
          PFun.fix (fun v => Part.map (fun v => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) a'

Tactic:
simp only [Part.eq_some_iff.2 hv₁, Part.map_some, Part.mem_some_iff]

Result:
case neg.intro.intro.intro.intro.intro.intro
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v'.tail
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
⊢ (Sum.inl v₂ = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
    ∃ a',
      (Sum.inr a' = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∧
        v₂ ∈
          PFun.fix (fun v => Part.map (fun v => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) a'