awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
he₂ : (if v'.headI = 0 then Sum.inl v'.tail else Sum.inr v'.tail) = Sum.inl v'_1
⊢ v'.headI = 0

Tactic:
split_ifs at he₂ with h
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
he₂ : (if v'.headI = 0 then Sum.inl v'.tail else Sum.inr v'.tail) = Sum.inl v'_1
h : v'.headI = 0
⊢ Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v'.tail) (Sum.inl v'_1)

Tactic:
split_ifs at he₂ with h
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v'.tail) (Sum.inl v'_1)
⊢ v'.tail ∈ f.fix.eval v_1

Tactic:
cases he₂
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v'.tail) (Sum.inl v'_1)
he₃ : v'.tail ∈ f.fix.eval v_1
⊢ x ∈ eval step (Cfg.ret k v'.tail)

Tactic:
cases he₂
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v'.tail) (Sum.inl v'_1)
he₃ : v'.tail ∈ f.fix.eval v_1
hr₁ : x ∈ eval step (Cfg.ret k v'.tail)
⊢ x ∈ eval step (stepRet k v'.tail)

Tactic:
cases he₂
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v'.tail) (Sum.inl v'_1)
he₃ : v'.tail ∈ f.fix.eval v_1
hr₁ : x ∈ eval step (Cfg.ret k v'.tail)
hr₂ : x ∈ eval step (stepRet k v'.tail)
⊢ v'.tail ∈ f.fix.eval v

Tactic:
cases he₂
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v'.tail) (Sum.inl v'_1)
he₃ : v'.tail ∈ f.fix.eval v_1
hr₁ : x ∈ eval step (Cfg.ret k v'.tail)
hr₂ : x ∈ eval step (stepRet k v'.tail)
he₄ : v'.tail ∈ f.fix.eval 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)) (Sum.inl v'.tail)

Tactic:
cases he₂
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
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'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he_1 : v'.tail ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he_2 : v'.tail ∈ f.fix.eval v
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'.tail)
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)

Tactic:
⟨_, he₁, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
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'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he_1 : v'.tail ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he_2 : v'.tail ∈ f.fix.eval v
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'.tail)
pos : x ∈ eval step (Cfg.ret (Cont.fix f k) v')
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)

Tactic:
refine ⟨_, he₁, ?_⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
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'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he_1 : v'.tail ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he_2 : v'.tail ∈ f.fix.eval v
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'.tail)
pos : x ∈ eval step (stepRet (Cont.fix f k) v')
pos₁ : Reaches step (Cfg.ret (Cont.fix f k) v') (stepRet (Cont.fix f k) v')
rw : Cfg
⊢ x ∈ eval step (Cfg.ret (Cont.fix f k) v')

Tactic:
rw [reaches_eval]

Premises used: StateTransition.reaches_eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
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'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he_1 : v'.tail ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he_2 : v'.tail ∈ f.fix.eval v
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'.tail)
⊢ Reaches step (Cfg.ret (Cont.fix f k) v') (stepRet (Cont.fix f 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_1 : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
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'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he_1 : v'.tail ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he_2 : v'.tail ∈ f.fix.eval v
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'.tail)
⊢ Reaches step (Cfg.ret (Cont.fix f k) v') (stepRet (Cont.fix f k) 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 : Cfg
v : List ℕ
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'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he_1 : v'.tail ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he_2 : v'.tail ∈ f.fix.eval v
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'.tail)
pos : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)
pos₁ pos₂ pos₃ pos₄ : x ∈ eval step (stepRet k v'.tail)
⊢ x ∈ eval step (stepRet (Cont.fix f k) v')

Tactic:
rwa [stepRet, if_pos h]

Premises used: if_pos, Turing.ToPartrec.stepRet
-- 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'')
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'')
right :
  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'
mpr :
  ∀ (v₁ : List ℕ) (he₁ : v₁ ∈ f.eval v)
    (he₂ : (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) = Sum.inr 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
-- 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'')
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'')
right :
  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'
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
he₂ : (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) = Sum.inr v''
⊢ ¬v₁.headI = 0

Tactic:
split_ifs at he₂ with h
-- 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'')
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'')
right :
  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'
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
he₂ : (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) = Sum.inr v''
h : ¬v₁.headI = 0
⊢ Eq (α := List ℕ ⊕ List ℕ) (Sum.inr v₁.tail) (Sum.inr v'')

Tactic:
split_ifs at he₂ with h
-- 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'')
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'')
right :
  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'
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inr v₁.tail) (Sum.inr 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)) (Sum.inr v₁.tail)

Tactic:
cases he₂
-- 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'')
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'')
right :
  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'
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inr v₁.tail) (Sum.inr v'')
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₁.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))
      v₁.tail)
    v'

Tactic:
cases he₂
-- 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'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right :
  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₁.tail)
    v'
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)

Tactic:
⟨_, he₁, ?_⟩

Premises used: And.intro, Exists.intro
-- 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'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right :
  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₁.tail)
    v'
neg : x ∈ eval step (Cfg.ret (Cont.fix f k) v₁)
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)

Tactic:
refine ⟨_, he₁, ?_⟩
-- 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'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right :
  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₁.tail)
    v'
neg : x ∈ eval step (stepRet (Cont.fix f k) v₁)
neg₁ : Reaches step (Cfg.ret (Cont.fix f k) v₁) (stepRet (Cont.fix f k) v₁)
rw : Cfg
⊢ x ∈ eval step (Cfg.ret (Cont.fix f k) v₁)

Tactic:
rw [reaches_eval]

Premises used: StateTransition.reaches_eval
-- 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'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right :
  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₁.tail)
    v'
⊢ Reaches step (Cfg.ret (Cont.fix f k) v₁) (stepRet (Cont.fix f 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_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'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right :
  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₁.tail)
    v'
⊢ Reaches step (Cfg.ret (Cont.fix f k) v₁) (stepRet (Cont.fix f k) 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 : 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'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right :
  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₁.tail)
    v'
neg : x ∈ eval step (stepNormal f (Cont.fix f k) v₁.tail)
⊢ x ∈ eval step (stepRet (Cont.fix f k) v₁)

Tactic:
rw [stepRet, if_neg h]

Premises used: if_neg, Turing.ToPartrec.stepRet