mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: 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)

Tactic:
;

Goal state after:
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)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: 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 (Cfg.ret k₀ v₀)

Tactic:
;

Goal state after:
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 (Cfg.ret k₀ v₀)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case pos
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'✝)
hr : x ∈ eval step (stepRet k v'✝)
v : List ℕ
he✝ : v'✝ ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
he : Sum.inl v'✝ ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he₂ : Sum.inl v'.tail = Sum.inl v'✝
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)

Tactic:
;

Goal state after:
case pos
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'✝)
hr : x ∈ eval step (stepRet k v'✝)
v : List ℕ
he✝ : v'✝ ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
he : Sum.inl v'✝ ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he₂ : Sum.inl v'.tail = Sum.inl v'✝
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case neg
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')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v'' : List ℕ
he₁' : Sum.inr v'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
right✝ :
  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)) v''
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
he₂ : Sum.inr v₁.tail = Sum.inr v''
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)

Tactic:
;

Goal state after:
case neg
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')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v'' : List ℕ
he₁' : Sum.inr v'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
right✝ :
  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)) v''
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
he₂ : Sum.inr v₁.tail = Sum.inr v''
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct K Γ σ k✝
q✝ : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt S q✝ →
    (∀ x ∈ trStmts₁ q✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧ ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ ∀ (a : Γ' K Γ) (v : σ), go k✝ s q✝ ∈ trSupp M S

Tactic:
;

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct K Γ σ k✝
q✝ : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt S q✝ →
    (∀ x ∈ trStmts₁ q✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧ ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ ∀ (a : Γ' K Γ) (v : σ), go k✝ s q✝ ∈ trSupp M S
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct K Γ σ k✝
q✝ : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt S q✝ →
    (∀ x ∈ trStmts₁ q✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧ ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : Γ' K Γ
v✝ : σ
⊢ go k✝ s q✝ ∈ trSupp M S

Tactic:
;

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct K Γ σ k✝
q✝ : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt S q✝ →
    (∀ x ∈ trStmts₁ q✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧ ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : Γ' K Γ
v✝ : σ
⊢ go k✝ s q✝ ∈ trSupp M S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux (pop' k₁ (branch (fun s ↦ s.elim true p) (goto fun x ↦ q) (push' k₂ (goto fun x ↦ Λ'.move p k₁ k₂ q))))
      s S)
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }

Tactic:
;

Goal state after:
case cons
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux (pop' k₁ (branch (fun s ↦ s.elim true p) (goto fun x ↦ q) (push' k₂ (goto fun x ↦ Λ'.move p k₁ k₂ q))))
      s S)
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ eval step (stepNormal (f.cons fs) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)

Tactic:
;

Goal state after:
case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ eval step (stepNormal (f.cons fs) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let x ← f.eval v
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))

Tactic:
;

Goal state after:
case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let x ← f.eval v
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (fun v_1 ↦ eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) = fun x ↦ do
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))

Tactic:
;

Goal state after:
case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (fun v_1 ↦ eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) = fun x ↦ do
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.61 = do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

pp: case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₁ fs v✝ k) v) ?m.61

pp: f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg

Tactic:
;

Goal state after:
case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.61 = do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₁ fs v✝ k) v) ?m.61

f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ (do
      let v_1 ← fs.eval v✝
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

Tactic:
;

Goal state after:
case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ (do
      let v_1 ← fs.eval v✝
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ (fun v_1 ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_1)) = fun x ↦ eval step (Cfg.ret k (v.headI :: x))

Tactic:
;

Goal state after:
case e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ (fun v_1 ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_1)) = fun x ↦ eval step (Cfg.ret k (v.headI :: x))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step (stepNormal (f.comp g) k v) = do
    let v ← (f.comp g).eval v
    eval step (Cfg.ret k v)

Tactic:
;

Goal state after:
case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step (stepNormal (f.comp g) k v) = do
    let v ← (f.comp g).eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v)) =
    do
    let x ← g.eval v
    let v ← f.eval x
    eval step (Cfg.ret k v)

Tactic:
;

Goal state after:
case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v)) =
    do
    let x ← g.eval v
    let v ← f.eval x
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (fun v ↦ eval step (Cfg.ret (Cont.comp f k) v)) = fun x ↦ do
    let v ← f.eval x
    eval step (Cfg.ret k v)

Tactic:
;

Goal state after:
case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (fun v ↦ eval step (Cfg.ret (Cont.comp f k) v)) = fun x ↦ do
    let v ← f.eval x
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.171 = do
    let v ← f.eval v
    eval step (Cfg.ret k v)

pp: case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.comp f k) v) ?m.171

pp: f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg

Tactic:
;

Goal state after:
case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.171 = do
    let v ← f.eval v
    eval step (Cfg.ret k v)

case e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.comp f k) v) ?m.171

f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case case
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step (stepNormal (f.case g) k v) = do
    let v ← (f.case g).eval v
    eval step (Cfg.ret k v)

Tactic:
;

Goal state after:
case case
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step (stepNormal (f.case g) k v) = do
    let v ← (f.case g).eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case fix
f : Code
IHf : f.Ok
k : Cont
v : List ℕ
⊢ eval step (stepNormal f.fix k v) = do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)

Tactic:
;

Goal state after:
case fix
f : Code
IHf : f.Ok
k : Cont
v : List ℕ
⊢ eval step (stepNormal f.fix k v) = do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case zero'
k : Cont
v : List ℕ
⊢ eval step (stepNormal Code.zero' k v) = do
    let v ← Code.zero'.eval v
    eval step (Cfg.ret k v)

Tactic:
;

Goal state after:
case zero'
k : Cont
v : List ℕ
⊢ eval step (stepNormal Code.zero' k v) = do
    let v ← Code.zero'.eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case succ
k : Cont
v : List ℕ
⊢ eval step (stepNormal Code.succ k v) = do
    let v ← Code.succ.eval v
    eval step (Cfg.ret k v)

Tactic:
;

Goal state after:
case succ
k : Cont
v : List ℕ
⊢ eval step (stepNormal Code.succ k v) = do
    let v ← Code.succ.eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this : IsClopen C0
⊢ ∀ (i : I), Disjoint V (C' i)

Tactic:
;

Goal state after:
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this : IsClopen C0
⊢ ∀ (i : I), Disjoint V (C' i)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case tail
k : Cont
v : List ℕ
⊢ eval step (stepNormal Code.tail k v) = do
    let v ← Code.tail.eval v
    eval step (Cfg.ret k v)

Tactic:
;

Goal state after:
case tail
k : Cont
v : List ℕ
⊢ eval step (stepNormal Code.tail k v) = do
    let v ← Code.tail.eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons₁
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (do
      let v_1 ← fs.eval as
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    do
    let x ← fs.eval as
    let a ← k.eval (v.headI :: x)
    pure (Cfg.halt a)

Tactic:
;

Goal state after:
case cons₁
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (do
      let v_1 ← fs.eval as
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    do
    let x ← fs.eval as
    let a ← k.eval (v.headI :: x)
    pure (Cfg.halt a)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (fun v_1 ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_1)) = fun x ↦ do
    let a ← k.eval (v.headI :: x)
    pure (Cfg.halt a)

Tactic:
;

Goal state after:
case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (fun v_1 ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_1)) = fun x ↦ do
    let a ← k.eval (v.headI :: x)
    pure (Cfg.halt a)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step ?m.89 = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)

pp: case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₂ v k) v') ?m.89

pp: fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg

Tactic:
;

Goal state after:
case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step ?m.89 = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)

case e_a
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₂ v k) v') ?m.89

fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg