mathlib-initiative/mathlib-tactics huggingface dataset:
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 v ←
      (fun v ↦ do
            let n ← f.eval v
            let ns ← fs.eval v
            pure (n.headI :: ns))
          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 ℕ
⊢ (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let v ←
      (fun v ↦ do
            let n ← f.eval v
            let ns ← fs.eval v
            pure (n.headI :: ns))
          v
    eval step (Cfg.ret k v)
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.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)
i : I
⊢ Disjoint (Z' i) U

Tactic:
exact Disjoint.mono_left (subset_iUnion_of_subset i fun _ h ↦ h) (by grind)

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.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 Γ'
a' : Γ'
Sk : List Γ'
e :
  (bif p a' then ([], some a', Sk)
    else
      match splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
e₁ : S k₁ = a' :: Sk
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k₁ (a' :: Sk).tail }
    else
      { l := some (Λ'.move p k₁ k₂ q), var := (a' :: Sk).head?,
        stk :=
          update (update S k₁ (a' :: Sk).tail) k₂ ((a' :: Sk).head?.getD default :: update S k₁ (a' :: Sk).tail k₂) })
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }

Tactic:
]

Goal state after:
case cons.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 Γ'
a' : Γ'
Sk : List Γ'
e :
  (bif p a' then ([], some a', Sk)
    else
      match splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
e₁ : S k₁ = a' :: Sk
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k₁ (a' :: Sk).tail }
    else
      { l := some (Λ'.move p k₁ k₂ q), var := (a' :: Sk).head?,
        stk :=
          update (update S k₁ (a' :: Sk).tail) k₂ ((a' :: Sk).head?.getD default :: update S k₁ (a' :: Sk).tail k₂) })
    { 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 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 comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal g (Cont.comp f k) v) 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 ((fun k v ↦ stepNormal g (Cont.comp f k) v) 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 v ← (fun v ↦ g.eval v >>= f.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 ℕ
⊢ (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v)) =
    do
    let v ← (fun v ↦ g.eval v >>= f.eval) v
    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 e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ (do
      let v ← f.eval v
      eval step (Cfg.ret k v)) =
    do
    let v ← f.eval v
    eval step (Cfg.ret k v)

Tactic:
]

Goal state after:
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 ((fun k v ↦ Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) v.headI) 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 ((fun k v ↦ Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) v.headI) 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 ((fun k v ↦ stepNormal f (Cont.fix f k) v) 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 ((fun k v ↦ stepNormal f (Cont.fix f k) v) 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 fix
f : Code
IHf : f.Ok
k : Cont
v : List ℕ
⊢ (do
      let v ← f.fix.eval v
      eval step (Cfg.ret k v)) =
    do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)

Tactic:
]

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case zero'
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ Cfg.ret k (0 :: v)) 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 ((fun k v ↦ Cfg.ret k (0 :: v)) 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 ((fun k v ↦ Cfg.ret k [v.headI.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 ((fun k v ↦ Cfg.ret k [v.headI.succ]) k v) = do
    let v ← Code.succ.eval v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case tail
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ Cfg.ret k v.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 ((fun k v ↦ Cfg.ret k v.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)) =
    Cfg.halt <$>
      (fun v ↦ do
          let ns ← fs.eval as
          k.eval (v.headI :: ns))
        v

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)) =
    Cfg.halt <$>
      (fun v ↦ do
          let ns ← fs.eval as
          k.eval (v.headI :: ns))
        v
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
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case refine_3
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
p✝ : σ → Bool
q₁✝ 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')
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 (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝, x ∈ trSupp M S
IH₁₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₁✝)
IH₁₂ : ∀ l' ∈ trStmts₁ q₁✝, TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₂✝)
IH₂₂ : ∀ l' ∈ trStmts₁ q₂✝, TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)

Tactic:
]

Goal state after:
case refine_3
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
p✝ : σ → Bool
q₁✝ 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')
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 (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝, x ∈ trSupp M S
IH₁₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₁✝)
IH₁₂ : ∀ l' ∈ trStmts₁ q₁✝, TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₂✝)
IH₂₂ : ∀ l' ∈ trStmts₁ q₂✝, TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
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 ℕ
⊢ Cfg.halt <$> k.eval (v.headI :: v') = Cfg.halt <$> k.eval (v.headI :: v')

Tactic:
]

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons₂
ns : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet k (ns.headI :: v)) = Cfg.halt <$> (fun v ↦ k.eval (ns.headI :: v)) v

Tactic:
]

Goal state after:
case cons₂
ns : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet k (ns.headI :: v)) = Cfg.halt <$> (fun v ↦ k.eval (ns.headI :: v)) v
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.cons.false
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 Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
e₂ : p a' = false
fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e : (a' :: (fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) = (a :: L₁, o, L₂)
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k₁ (a' :: Sk).tail }
    else
      { l := some (Λ'.move p k₁ k₂ q), var := (a' :: Sk).head?,
        stk :=
          update (update S k₁ (a' :: Sk).tail) k₂ ((a' :: Sk).head?.getD default :: update S k₁ (a' :: Sk).tail k₂) })
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }

Tactic:
]

Goal state after:
case cons.cons.false
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 Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
e₂ : p a' = false
fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e : (a' :: (fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) = (a :: L₁, o, L₂)
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k₁ (a' :: Sk).tail }
    else
      { l := some (Λ'.move p k₁ k₂ q), var := (a' :: Sk).head?,
        stk :=
          update (update S k₁ (a' :: Sk).tail) k₂ ((a' :: Sk).head?.getD default :: update S k₁ (a' :: Sk).tail k₂) })
    { 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 comp
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (do
      let v ← f.eval v
      eval step (Cfg.ret k v)) =
    Cfg.halt <$> (fun v ↦ f.eval v >>= k.eval) v

Tactic:
]

Goal state after:
case comp
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (do
      let v ← f.eval v
      eval step (Cfg.ret k v)) =
    Cfg.halt <$> (fun v ↦ f.eval v >>= k.eval) v
Module: Mathlib.Computability.TuringMachine.Config

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

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

pp: f : Code
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
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step ?m.167 = do
    let a ← k.eval v'
    pure (Cfg.halt a)

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

f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ Cfg.halt <$> k.eval v' = Cfg.halt <$> k.eval v'

Tactic:
]

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case fix
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) =
    Cfg.halt <$> (fun v ↦ if v.headI = 0 then k.eval v.tail else f.fix.eval v.tail >>= k.eval) v

Tactic:
]

Goal state after:
case fix
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) =
    Cfg.halt <$> (fun v ↦ if v.headI = 0 then k.eval v.tail else f.fix.eval v.tail >>= k.eval) v
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case pos
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h✝ : v.headI = 0
⊢ eval step (stepRet k v.tail) = Cfg.halt <$> k.eval v.tail

pp: case neg
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h✝ : ¬v.headI = 0
⊢ eval step (stepNormal f (Cont.fix f k) v.tail) = Cfg.halt <$> (f.fix.eval v.tail >>= k.eval)

Tactic:
· exact IH

Goal state after:
case neg
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h✝ : ¬v.headI = 0
⊢ eval step (stepNormal f (Cont.fix f k) v.tail) = Cfg.halt <$> (f.fix.eval v.tail >>= k.eval)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h✝ : ¬v.headI = 0
x✝ : List ℕ
⊢ eval step (Cfg.ret k x✝) = eval step (stepRet k x✝)

Tactic:
]

Goal state after:
case e_a
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h✝ : ¬v.headI = 0
x✝ : List ℕ
⊢ eval step (Cfg.ret k x✝) = eval step (stepRet k x✝)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ExtremallyDisconnected X
e : X ≃ₜ Y
U : Set Y
hU : IsOpen U
⊢ IsOpen (closure (⇑e.symm '' U))

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ExtremallyDisconnected X
e : X ≃ₜ Y
U : Set Y
hU : IsOpen U
⊢ IsOpen (closure (⇑e.symm '' U))
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ExtremallyDisconnected X
e : X ≃ₜ Y
U : Set Y
hU : IsOpen U
⊢ IsOpen (closure U)

Tactic:
rw [e.symm.isInducing.closure_eq_preimage_closure_image, Homeomorph.isOpen_preimage]
    exact ExtremallyDisconnected.open_closure _ (e.symm.isOpen_image.mpr hU)

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ¬∀ (o : Set X), IsOpen o → y ∈ o → (o ∩ U).Nonempty

Tactic:
]

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ¬∀ (o : Set X), IsOpen o → y ∈ o → (o ∩ U).Nonempty
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ Disjoint U V

Tactic:
]

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ Disjoint U V
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
⊢ False

Tactic:
let Z := of (ULift.{u} <| Fin 2)

Goal state after:
case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift.{u, 0} (Fin 2))
⊢ False