-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : 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₂_1 : 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₂)
pos :
  v₁.headI = 0 →
    ∀ (hv₂ : Membership.mem (γ := Part (List ℕ)) (pure v₁.tail) v₂),
      Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v₂) (Sum.inl v₁.tail) ∨
        ∃ (a' : List ℕ),
          False ∧
            Membership.mem (γ := Part (List ℕ))
              (PFun.fix
                (fun (v : List ℕ) ↦
                  Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
                a')
              v₂
neg :
  ¬v₁.headI = 0 →
    ∀ (hv₂ : v₂ ∈ f.fix.eval v₁.tail),
      False ∨
        ∃ (a' : List ℕ),
          Eq (α := List ℕ ⊕ List ℕ) (Sum.inr a') (Sum.inr v₁.tail) ∧
            Membership.mem (γ := Part (List ℕ))
              (PFun.fix
                (fun (v : List ℕ) ↦
                  Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
                a')
              v₂
pos₁ :
  v₁.headI = 0 →
    ∀ (hv₂ : Membership.mem (γ := Part (List ℕ)) (pure v₁.tail) v₂),
      Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v₂) (Sum.inl v₁.tail) ∨
        ∃ (a' : List ℕ),
          False ∧
            Membership.mem (γ := Part (List ℕ))
              (PFun.fix
                (fun (v : List ℕ) ↦
                  Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
                a')
              v₂
neg₁ :
  ¬v₁.headI = 0 →
    ∀ (hv₂ : v₂ ∈ f.fix.eval v₁.tail),
      False ∨
        ∃ (a' : List ℕ),
          Eq (α := List ℕ ⊕ List ℕ) (Sum.inr a') (Sum.inr v₁.tail) ∧
            Membership.mem (γ := Part (List ℕ))
              (PFun.fix
                (fun (v : List ℕ) ↦
                  Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
                a')
              v₂
⊢ (Sum.inl v₂ = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
    ∃ (a' : List ℕ),
      (Sum.inr a' = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∧
        Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
            a')
          v₂

Tactic:
split_ifs at hv₂ ⊢ <;> [exact Or.inl (congr_arg Sum.inl (Part.mem_some_iff.1 hv₂));
          exact Or.inr ⟨_, rfl, hv₂⟩]

Premises used: Part.mem_some_iff, Sum.inl, congr_arg, Iff.mp, Or.inl, Or.inr