awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀
hab : stepRet k₀ v₀ ∈ step (Cfg.ret k₀ v₀)
⊢ stepRet k₀ v₀ ∈ step (stepNormal f Cont.halt v'.tail)

Tactic:
rw [e₀]
-- 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₀
⊢ stepRet k₀ v₀ ∈ step (Cfg.ret k₀ v₀)

Tactic:
rfl
-- 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₀
neg :
  ∀ (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₂)),
    ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)
⊢ ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
          IH (stepRet (k₀.then (Cont.fix f k)) v₀) (by rw [stepRet, if_neg he, e₁]; rfl)
            v'.tail _ stepRet_then (by apply ReflTransGen.single; rw [e₀]; rfl)

Premises used: Turing.ToPartrec.stepRet_then, Turing.ToPartrec.Cont.fix, List.tail, Turing.ToPartrec.stepRet, Turing.ToPartrec.Cont.then
-- 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₂)
⊢ ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
⟨_, PFun.mem_fix_iff.2 ?_, h₃⟩

Premises used: Iff.mpr, And.intro, Exists.intro, PFun.mem_fix_iff
-- 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₂)
neg :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
      (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v'.tail))
      (Sum.inl v₂) ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
          (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v'.tail))
          (Sum.inr a') ∧
        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₂
⊢ ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
refine ⟨_, PFun.mem_fix_iff.2 ?_, h₃⟩
-- 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₂)
neg :
  (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₂
⊢ Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
      (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v'.tail))
      (Sum.inl v₂) ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
          (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v'.tail))
          (Sum.inr a') ∧
        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:
simp only [Part.eq_some_iff.2 hv₁, Part.map_some, Part.mem_some_iff]

Premises used: Iff.mpr, Part.eq_some_iff, Part.mem_some_iff, Part.map_some
-- 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₂
⊢ (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₂ ⊢
-- 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 ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h_1 : 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₂

Tactic:
Or.inl (congr_arg Sum.inl (Part.mem_some_iff.1 hv₂))

Premises used: Part.mem_some_iff, Sum.inl, congr_arg, Iff.mp, Or.inl
-- 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 ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h_1 : 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₂

Tactic:
exact Or.inl (congr_arg Sum.inl (Part.mem_some_iff.1 hv₂))

Premises used: Part.mem_some_iff, Sum.inl, congr_arg, Iff.mp, Or.inl
-- 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 ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h_1 : ¬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₂

Tactic:
Or.inr ⟨_, rfl, hv₂⟩

Premises used: And.intro, Exists.intro, Or.inr, rfl
-- 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 ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h_1 : ¬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₂

Tactic:
exact Or.inr ⟨_, rfl, hv₂⟩

Premises used: Or.inr
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v : List ℕ
k' : Cont
v' : List ℕ
h : x ∈ eval step (Cfg.ret (k'.then (Cont.fix f k)) v')
IH :
  ∀ (a' : Cfg),
    step (Cfg.ret (k'.then (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.ret k' 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:
IH _ rfl _ _ stepRet_then (ReflTransGen.tail hr rfl)

Premises used: Turing.ToPartrec.stepRet_then, Relation.ReflTransGen.tail, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v : List ℕ
k' : Cont
v' : List ℕ
h : x ∈ eval step (Cfg.ret (k'.then (Cont.fix f k)) v')
IH :
  ∀ (a' : Cfg),
    step (Cfg.ret (k'.then (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.ret k' 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:
exact IH _ rfl _ _ stepRet_then (ReflTransGen.tail hr rfl)

Premises used: Turing.ToPartrec.stepRet_then, Relation.ReflTransGen.tail, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr : x ∈ eval step (Cfg.ret k v')
mpr : ∀ (hr : x ∈ eval step (stepRet k v')), x ∈ eval step (stepNormal f (Cont.fix f k) v)
mpr₁ : Reaches step (Cfg.ret k v') (stepRet k v')
rw : Cfg
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)

Tactic:
rw [reaches_eval] at hr

Premises used: StateTransition.reaches_eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr : x ∈ eval step (Cfg.ret k v')
⊢ Reaches step (Cfg.ret k v') (stepRet k v')

Tactic:
ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, rfl, StateTransition.Reaches
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr : x ∈ eval step (Cfg.ret k v')
⊢ Reaches step (Cfg.ret k v') (stepRet k v')

Tactic:
exact ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)

Tactic:
PFun.fixInduction he fun v (he : v' ∈ f.fix.eval v) IH => ?_

Premises used: PFun.fixInduction
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
mpr :
  ∀ (v : List ℕ) (he : v' ∈ f.fix.eval v)
    (IH :
      ∀ (a'' : List ℕ),
        Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
            (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
            (Sum.inr a'') →
          x ∈ eval step (stepNormal f (Cont.fix f k) a'')),
    x ∈ eval step (stepNormal f (Cont.fix f k) v)
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)

Tactic:
refine PFun.fixInduction he fun v (he : v' ∈ f.fix.eval v) IH => ?_
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
mpr : ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)

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

Premises used: Part.mem_bind_iff, Part.bind_eq_bind
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
mpr :
  ∀
    (he :
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inl v')),
    ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
mpr₁ :
  ∀ (v'' : List ℕ)
    (he₁' :
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr v'')),
    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))
          v'')
        v' →
      ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)

Tactic:
obtain he | ⟨v'', he₁', _⟩ := PFun.mem_fix_iff.1 he

Premises used: Iff.mp, PFun.mem_fix_iff
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he_2 : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
he :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inl v')
mpr :
  ∀ (v'_1 : List ℕ) (he₁ : v'_1 ∈ f.eval v)
    (he₂ : (if v'_1.headI = 0 then Sum.inl v'_1.tail else Sum.inr v'_1.tail) = Sum.inl v'),
    ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)

Tactic:
obtain ⟨v', he₁, he₂⟩ := (Part.mem_map_iff _).1 he

Premises used: Iff.mp, Part.mem_map_iff