awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h_1 : v₁.headI = 0
hv₂ : Membership.mem (γ := Part (List ℕ)) (pure v₁.tail) v₂
⊢ Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl v₁.tail)) (Sum.inl v₁.tail) ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl 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₁.tail

Tactic:
Or.inl (Part.mem_some _)

Premises used: Part.mem_some, Or.inl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h_1 : v₁.headI = 0
hv₂ : Membership.mem (γ := Part (List ℕ)) (pure v₁.tail) v₂
⊢ Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl v₁.tail)) (Sum.inl v₁.tail) ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl 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₁.tail

Tactic:
exact Or.inl (Part.mem_some _)

Premises used: Part.mem_some, Or.inl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h_1 : ¬v₁.headI = 0
hv₂ : v₂ ∈ f.fix.eval v₁.tail
⊢ Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inr v₁.tail)) (Sum.inl v₂) ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inr 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:
Or.inr ⟨_, Part.mem_some _, hv₂⟩

Premises used: Part.mem_some, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h_1 : ¬v₁.headI = 0
hv₂ : v₂ ∈ f.fix.eval v₁.tail
⊢ Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inr v₁.tail)) (Sum.inl v₂) ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inr 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:
exact Or.inr ⟨_, Part.mem_some _, hv₂⟩

Premises used: Or.inr
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
mp :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) → ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)

Tactic:
suffices ∀ c, x ∈ eval step c → ∀ v c', c = Cfg.then c' (Cont.fix f k) →
      Reaches step (stepNormal f Cont.halt v) c' →
        ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if List.headI v₁ = 0 then pure v₁.tail else f.fix.eval v₁.tail,
          x ∈ eval step (Cfg.ret k v₂) by
      intro h
      obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
        this _ h _ _ (stepNormal_then _ Cont.halt _ _) ReflTransGen.refl
      refine ⟨v₂, PFun.mem_fix_iff.2 ?_, h₃⟩
      simp only [Part.eq_some_iff.2 hv₁, Part.map_some]
      split_ifs at hv₂ ⊢
      · rw [Part.mem_some_iff.1 hv₂]
        exact Or.inl (Part.mem_some _)
      · exact Or.inr ⟨_, Part.mem_some _, hv₂⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
⊢ ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)

Tactic:
fun c he => evalInduction he fun y h IH => ?_

Premises used: StateTransition.evalInduction
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
mp :
  ∀ (c : Cfg) (he : x ∈ eval step c) (y : Cfg) (h : x ∈ eval step y)
    (IH :
      ∀ (a' : Cfg),
        step y = 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₂))
    (v : List ℕ) (c' : Cfg),
    y = 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₂)
⊢ ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)

Tactic:
refine fun c he => evalInduction he fun y h IH => ?_
-- 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 v' : List ℕ
h : x ∈ eval step ((Cfg.halt v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.halt v').then (Cont.fix f k)) = 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')
⊢ x ∈ eval step ((fun (k' : Cont) ↦ stepRet k' v') (Cont.fix f k))

Tactic:
rw [Cfg.then] at h IH

Premises used: Turing.ToPartrec.Cfg.then
-- 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 v' : List ℕ
h : x ∈ eval step ((Cfg.halt v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.halt v').then (Cont.fix f k)) = 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₁ : x ∈ eval step ((fun (k' : Cont) ↦ stepRet k' v') (Cont.fix f k))
⊢ ∀ (a' : Cfg),
    step ((fun (k' : Cont) ↦ stepRet k' v') (Cont.fix f k)) = 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₂)

Tactic:
rw [Cfg.then] at h IH

Premises used: Turing.ToPartrec.Cfg.then
-- 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 v' : List ℕ
h : x ∈ eval step ((Cfg.halt v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.halt v').then (Cont.fix f k)) = 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₁ : x ∈ eval step ((fun (k' : Cont) ↦ stepRet k' v') (Cont.fix f k))
IH₁ :
  ∀ (a' : Cfg),
    step ((fun (k' : Cont) ↦ stepRet k' v') (Cont.fix f k)) = 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₂)
⊢ Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')

Tactic:
rw [Cfg.then] at h IH

Premises used: Turing.ToPartrec.Cfg.then
-- 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' v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.ret k' v').then (Cont.fix f k)) = 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')
⊢ x ∈ eval step ((fun (k'_1 : Cont) ↦ Cfg.ret (k'.then k'_1) v') (Cont.fix f k))

Tactic:
rw [Cfg.then] at h IH

Premises used: Turing.ToPartrec.Cfg.then
-- 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' v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.ret k' v').then (Cont.fix f k)) = 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')
h₁ : x ∈ eval step ((fun (k'_1 : Cont) ↦ Cfg.ret (k'.then k'_1) v') (Cont.fix f k))
⊢ ∀ (a' : Cfg),
    step ((fun (k'_1 : Cont) ↦ Cfg.ret (k'.then k'_1) v') (Cont.fix f k)) = 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₂)

Tactic:
rw [Cfg.then] at h IH

Premises used: Turing.ToPartrec.Cfg.then
-- 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' v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.ret k' v').then (Cont.fix f k)) = 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')
h₁ : x ∈ eval step ((fun (k'_1 : Cont) ↦ Cfg.ret (k'.then k'_1) v') (Cont.fix f k))
IH₁ :
  ∀ (a' : Cfg),
    step ((fun (k'_1 : Cont) ↦ Cfg.ret (k'.then k'_1) v') (Cont.fix f k)) = 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₂)
⊢ Reaches step (stepNormal f Cont.halt v) (Cfg.ret k' v')

Tactic:
rw [Cfg.then] at h IH

Premises used: Turing.ToPartrec.Cfg.then
-- 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 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')
⊢ Cfg.halt v' ∈ eval step (stepNormal f Cont.halt v)

Tactic:
have := mem_eval.2 ⟨hr, 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 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)
⊢ ∃ a ∈ f.eval v, Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt a)

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

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 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)
mp :
  ∀ (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₂)
⊢ ∃ 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
-- 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 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'')
mp :
  ∀ (h₂ : Cfg.halt v' ∈ eval step (stepRet 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₂)
mp₁ : Reaches step (Cfg.ret Cont.halt v'') (stepRet Cont.halt v'')
rw : Cfg
⊢ ∃ 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 [reaches_eval] at h₂

Premises used: StateTransition.reaches_eval
-- 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 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'')
⊢ Reaches step (Cfg.ret Cont.halt v'') (stepRet Cont.halt v'')

Tactic:
ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, rfl, StateTransition.Reaches
-- 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 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'')
⊢ Reaches step (Cfg.ret Cont.halt v'') (stepRet Cont.halt v'')

Tactic:
exact ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, 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 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₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v'')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v'')
⊢ v' ∈ f.eval v

Tactic:
cases Part.mem_unique h₂ (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)

Premises used: Iff.mpr, Relation.ReflTransGen.refl, StateTransition.mem_eval, And.intro, rfl, Part.mem_unique
-- 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 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₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v'')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v'')
h₃ : v' ∈ f.eval v
⊢ Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')

Tactic:
cases Part.mem_unique h₂ (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)

Premises used: Iff.mpr, Relation.ReflTransGen.refl, StateTransition.mem_eval, And.intro, rfl, Part.mem_unique
-- 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 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₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v'')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v'')
h₃ : v' ∈ f.eval v
h₄ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
⊢ Cfg.halt v' ∈ eval step (stepRet Cont.halt v')

Tactic:
cases Part.mem_unique h₂ (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)

Premises used: Iff.mpr, Relation.ReflTransGen.refl, StateTransition.mem_eval, And.intro, rfl, Part.mem_unique
-- 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 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')
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')
⊢ ∃ 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:
⟨v', h₁, ?_⟩

Premises used: And.intro, Exists.intro
-- 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 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')
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')
mp : ∃ v₂ ∈ if v'.headI = 0 then pure v'.tail else f.fix.eval v'.tail, x ∈ eval step (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:
refine ⟨v', h₁, ?_⟩
-- 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 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')
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')
⊢ x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)

Tactic:
rw [stepRet] at h

Premises used: Turing.ToPartrec.stepRet