mathlib-initiative/mathlib-tactics huggingface dataset:
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.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)) =
    do
    let x ← f.eval v
    let a ← k.eval x
    pure (Cfg.halt a)

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)) =
    do
    let x ← f.eval v
    let a ← k.eval x
    pure (Cfg.halt a)
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 ℕ
⊢ (fun v ↦ eval step (Cfg.ret k v)) = fun x ↦ do
    let a ← k.eval x
    pure (Cfg.halt a)

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 ℕ
⊢ (fun v ↦ eval step (Cfg.ret k v)) = fun x ↦ do
    let a ← k.eval x
    pure (Cfg.halt a)
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.StackTuringMachine

Goal state before:
pp: case refine_4
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
l✝ : σ → Λ
ss' : TM2.SupportsStmt S (TM2.Stmt.goto l✝)
x✝ : ∀ x ∈ trStmts₁ (TM2.Stmt.goto l✝), x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l✝)) ∧
    ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
;

Goal state after:
case refine_4
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
l✝ : σ → Λ
ss' : TM2.SupportsStmt S (TM2.Stmt.goto l✝)
x✝ : ∀ x ∈ trStmts₁ (TM2.Stmt.goto l✝), x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l✝)) ∧
    ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp M S) (tr M l')
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:
;

Goal state after:
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

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
⊢ (fun v ↦ eval step (Cfg.ret k v)) = fun x ↦ do
    let a ← k.eval x
    pure (Cfg.halt a)

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
⊢ (fun v ↦ eval step (Cfg.ret k v)) = fun x ↦ do
    let a ← k.eval x
    pure (Cfg.halt a)
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✝) = do
    let a ← k.eval x✝
    pure (Cfg.halt a)

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✝) = do
    let a ← k.eval x✝
    pure (Cfg.halt a)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = ([], o, L₂)
⊢ ReflTransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux (pop' k (branch (fun s ↦ s.elim true p) (goto fun x ↦ q) (goto fun x ↦ Λ'.clear p k q))) s S)
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
;

Goal state after:
case nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = ([], o, L₂)
⊢ ReflTransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux (pop' k (branch (fun s ↦ s.elim true p) (goto fun x ↦ q) (goto fun x ↦ Λ'.clear p k q))) s S)
    { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
⊢ splitAtPred p (S k) = ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif
          match (S k).head?, true, p with
          | some x, x_1, f => f x
          | none, y, x => y then
        { l := some q, var := (S k).head?, stk := update S k (S k).tail }
      else { l := some (Λ'.clear p k q), var := (S k).head?, stk := update S k (S k).tail })
      { l := some q, var := o, stk := update S k L₂ }

Tactic:
;

Goal state after:
case nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
⊢ splitAtPred p (S k) = ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif
          match (S k).head?, true, p with
          | some x, x_1, f => f x
          | none, y, x => y then
        { l := some q, var := (S k).head?, stk := update S k (S k).tail }
      else { l := some (Λ'.clear p k q), var := (S k).head?, stk := update S k (S k).tail })
      { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Topology.Category.CompHaus.Projective

Goal state before:
pp: case h
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := ⋯
h : Ultrafilter X → ↑Y.toTop := ⋯
hh : Continuous h
⊢ ⇑(ConcreteCategory.hom (CompHausLike.ofHom (fun x ↦ True) { toFun := h, continuous_toFun := hh } ≫ g)) =
    ⇑(ConcreteCategory.hom f)

Tactic:
have : g.hom ∘ g' = id := hg'.comp_eq_id

Goal state after:
case h
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
this : ⇑(ConcreteCategory.hom g.hom) ∘ g' = id
⊢ ⇑(ConcreteCategory.hom (CompHausLike.ofHom (fun x ↦ True) { toFun := h, continuous_toFun := hh } ≫ g)) =
    ⇑(ConcreteCategory.hom f)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case nil.cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
⊢ (bif p a then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
      ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif p a then { l := some q, var := some a, stk := update S k Sk }
      else { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk })
      { l := some q, var := o, stk := update S k L₂ }

Tactic:
;

Goal state after:
case nil.cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
⊢ (bif p a then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
      ([], o, L₂) →
    ReflTransGen
      (fun a b ↦
        (match a with
          | { l := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
          some b)
      (bif p a then { l := some q, var := some a, stk := update S k Sk }
      else { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk })
      { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
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) (goto fun x ↦ Λ'.clear p k q))) s S)
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
;

Goal state after:
case cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
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) (goto fun x ↦ Λ'.clear p k q))) s S)
    { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
X₁ : ↑D → A := Prod.fst ∘ Subtype.val
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : X₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X₁ '' E₀ ≠ univ
ρ : ↑E → A := E.domRestrict X₁
ρ_cont : Continuous ρ
d : ↑D
hd : d ∈ E
⊢ ∃ a, ρ a = X₁ d

Tactic:
;

Goal state after:
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
X₁ : ↑D → A := Prod.fst ∘ Subtype.val
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : X₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X₁ '' E₀ ≠ univ
ρ : ↑E → A := E.domRestrict X₁
ρ_cont : Continuous ρ
d : ↑D
hd : d ∈ E
⊢ ∃ a, ρ a = X₁ d
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case e'_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ elim (trNat L.headI ++ [Γ'.cons]) [] c d =
    update
      (update (update (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [])
        rev [])
      main
      ((update (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main []
            rev).reverseAux
        (update (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [] main))

Tactic:
;

Goal state after:
case e'_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ elim (trNat L.headI ++ [Γ'.cons]) [] c d =
    update
      (update (update (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [])
        rev [])
      main
      ((update (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main []
            rev).reverseAux
        (update (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [] main))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pos.bit0
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih✝ :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ : List Γ'
⊢ { l := some (unrev q), var := some Γ'.bit0, stk := elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d } ∈
    some (TM2.stepAux (tr q.succ) s (elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d))

Tactic:
;

Goal state after:
case pos.bit0
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih✝ :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ : List Γ'
⊢ { l := some (unrev q), var := some Γ'.bit0, stk := elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d } ∈
    some (TM2.stepAux (tr q.succ) s (elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux
      (pop' main
        (branch (fun s ↦ decide (s = some Γ'.bit0)) (push rev (fun x ↦ Γ'.bit1) (goto fun x ↦ q₁.pred q₂))
          (branch (fun s ↦ natEnd (s.getD default)) (goto fun x ↦ q₁)
            (peek' main
              (branch (fun s ↦ natEnd (s.getD default)) (goto fun x ↦ unrev q₂)
                (push rev (fun x ↦ Γ'.bit0) (goto fun x ↦ unrev q₂)))))))
      s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }

Tactic:
;

Goal state after:
case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux
      (pop' main
        (branch (fun s ↦ decide (s = some Γ'.bit0)) (push rev (fun x ↦ Γ'.bit1) (goto fun x ↦ q₁.pred q₂))
          (branch (fun s ↦ natEnd (s.getD default)) (goto fun x ↦ q₁)
            (peek' main
              (branch (fun s ↦ natEnd (s.getD default)) (goto fun x ↦ unrev q₂)
                (push rev (fun x ↦ Γ'.bit0) (goto fun x ↦ unrev q₂)))))))
      s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case zero'
k : Cont
v : List ℕ
s : Option Γ'
⊢ { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList (0 :: v)) [] [] (trContStack k) } ∈
    TM2.step tr { l := some (trNormal Code.zero' (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }

Tactic:
;

Goal state after:
case zero'
k : Cont
v : List ℕ
s : Option Γ'
⊢ { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList (0 :: v)) [] [] (trContStack k) } ∈
    TM2.step tr { l := some (trNormal Code.zero' (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepNormal Code.succ k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal Code.succ (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
refine ⟨_, ⟨none, rfl⟩, head_main_ok.trans succ_ok⟩

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

Goal state before:
pp: case tail
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x_1 ↦ some Γ'.cons
⊢ Reaches₁ (TM2.step tr)
    { l := some (trNormal Code.tail (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
    { l := some (Λ'.ret (trCont k)), var := o, stk := elim (trList v.tail) [] [] (trContStack k) }

Tactic:
;

Goal state after:
case tail
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x_1 ↦ some Γ'.cons
⊢ Reaches₁ (TM2.step tr)
    { l := some (trNormal Code.tail (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
    { l := some (Λ'.ret (trCont k)), var := o, stk := elim (trList v.tail) [] [] (trContStack k) }
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: case mk.mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
a✝² : Quotient ⊤.toSetoid
a✝¹ : X
b✝ : Quotient ⊤.toSetoid
a✝ : X
⊢ Quot.mk (⇑⊤.toSetoid) a✝¹ = Quot.mk (⇑⊤.toSetoid) a✝

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
a✝² : Quotient ⊤.toSetoid
a✝¹ : X
b✝ : Quotient ⊤.toSetoid
a✝ : X
⊢ Quot.mk (⇑⊤.toSetoid) a✝¹ = Quot.mk (⇑⊤.toSetoid) a✝
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case e'_4.e'_7
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x_1 ↦ some Γ'.cons
⊢ elim (trList v.tail) [] [] (trContStack k) = elim ?tail.convert_7 [] [] (trContStack k)

Tactic:
;

Goal state after:
case e'_4.e'_7
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x_1 ↦ some Γ'.cons
⊢ elim (trList v.tail) [] [] (trContStack k) = elim ?tail.convert_7 [] [] (trContStack k)
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: case mk
X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (ContinuousMap.id X) ⋯ (Quot.mk (⇑A.toSetoid) a✝) = id (Quot.mk (⇑A.toSetoid) a✝)

Tactic:
;

Goal state after:
case mk
X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (ContinuousMap.id X) ⋯ (Quot.mk (⇑A.toSetoid) a✝) = id (Quot.mk (⇑A.toSetoid) a✝)
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
⊢ x ∈ connectedComponent y

Tactic:
connectedComponent_eq_iInter_isClopen,

Goal state after:
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
⊢ x ∈ ⋂ s, ↑s
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝² : Set X
x✝¹ : ∃ y, x✝² = {x | d.toSetoid x y}
y : X
h : x✝² = {x | d.toSetoid x y}
x✝ : X
⊢ x✝ ∈ d.proj ⁻¹' {d.proj y} ↔ x✝ ∈ x✝²

Tactic:
;

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝² : Set X
x✝¹ : ∃ y, x✝² = {x | d.toSetoid x y}
y : X
h : x✝² = {x | d.toSetoid x y}
x✝ : X
⊢ x✝ ∈ d.proj ⁻¹' {d.proj y} ↔ x✝ ∈ x✝²