mathlib-initiative/mathlib-tactics huggingface dataset:
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
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ (bif ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L))).head.1 then
      TM1.stepAux q (f v none) ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))
    else
      TM1.stepAux q
        (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
        (Tape.write
          ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.1,
            update (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k
              none)
          (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))))) =
    TM1.stepAux q (f v (hd :: tl).head?)
      ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom ?m.569)))

Tactic:
by

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

Goal state before:
pp: n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
n : ℕ
hn : f (n ::ᵥ v) = 0
hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0
⊢ Sum.inl (n.succ :: ↑v) ∈
    (cf.eval (n :: ↑v)).bind fun y ↦
      Part.some
        (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
        else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
e : (a : α) → X a ⟶ B
⊢ Continuous fun x ↦
    match x with
    | ⟨a, x⟩ => (ConcreteCategory.hom (e a)) x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
⊢ Function.Injective ⇑(ConcreteCategory.hom (ι X a))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
π : (a : α) → X a ⟶ B
a : α
⊢ ∀ (x : (fun X ↦ ↑X.toTop) (X a)),
    (ConcreteCategory.hom (desc X π)) ((ConcreteCategory.hom (ι X a)) x) = (ConcreteCategory.hom (π a)) x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝² : Finite α
X : α → CompHausLike P
inst✝¹ : HasExplicitFiniteCoproduct X
inst✝ : HasExplicitFiniteCoproducts P
n : ℕ
⊢ HasColimitsOfShape (Discrete (Fin n)) (CompHausLike P)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (Sigma.ι X a))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P✝¹ : TopCat → Prop
α : Type w
inst✝³ : Finite α
X : α → CompHausLike P✝¹
inst✝² : HasExplicitFiniteCoproduct X
P✝ : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P✝
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
⊢ PreservesFiniteCoproducts (compHausLikeToTop P)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P✝ : TopCat → Prop
α : Type w
inst✝² : Finite α
X : α → CompHausLike P✝
inst✝¹ : HasExplicitFiniteCoproduct X
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
P' : TopCat → Prop
h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop
⊢ PreservesFiniteCoproducts (toCompHausLike h)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
⊢ fst f g ≫ f = snd f g ≫ g

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Nat.Partrec' f
⊢ ∃ c, ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
z : ↑Z.toTop
⊢ ((ConcreteCategory.hom a) z, (ConcreteCategory.hom b) z) ∈
    {xy | (ConcreteCategory.hom f) xy.1 = (ConcreteCategory.hom g) xy.2}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a : Z ⟶ X
b : Z ⟶ Y
w : a ≫ f = b ≫ g
⊢ Continuous fun z ↦ ⟨((ConcreteCategory.hom a) z, (ConcreteCategory.hom b) z), ⋯⟩

Tactic:
by

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

Goal state before:
pp: case halt
k' : Cont
v : List ℕ
⊢ (halt.then k').eval v = halt.eval v >>= k'.eval

Tactic:
| halt =>

Goal state after:
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
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
⊢ let v' := stVar v (S k) o;
  let Sk' := stWrite v (S k) o;
  let S' := update S k Sk';
  ∃ L',
    (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S' k)).reverse) ∧
      TM1.stepAux (trStAct q o) v ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))) =
        TM1.stepAux q v' ((Tape.move Dir.right)^[(S' k).length] (Tape.mk' ∅ (addBottom L')))

Tactic:
by

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

Goal state before:
pp: k k' : Cont
v : List ℕ
⊢ (k.then k').eval v = k.eval v >>= k'.eval

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
⊢ cospan f.hom g.hom ≅
    cospan ((cospan f g ⋙ compHausLikeToTop P).map WalkingCospan.Hom.inl)
      ((cospan f g ⋙ compHausLikeToTop P).map WalkingCospan.Hom.inr)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
P' : TopCat → Prop
h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop
⊢ PreservesLimit (cospan f g) (toCompHausLike h)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
⊢ ∀ {X Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), HasExplicitPullback coprod.inl f

Tactic:
by

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

Goal state before:
pp: c : Code
k k' : Cont
v : List ℕ
⊢ stepNormal c (k.then k') v = (stepNormal c k v).then k'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P
inst✝ : HasExplicitPullbacksOfInclusions P
⊢ ∀ {X Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), PreservesLimit (cospan coprod.inl f) (compHausLikeToTop P)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
B X : CompHausLike P
π : X ⟶ B
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
W✝ : CompHausLike P
e : X ⟶ W✝
h : ∀ {Z : CompHausLike P} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
a b : (fun X ↦ ↑X.toTop) X
hab : (ConcreteCategory.hom π) a = (ConcreteCategory.hom π) b
⊢ ofHom P { toFun := fun x ↦ a, continuous_toFun := ⋯ } ≫ π = ofHom P { toFun := fun x ↦ b, continuous_toFun := ⋯ } ≫ π

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
B X : CompHausLike P
π : X ⟶ B
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
W✝ : CompHausLike P
e : X ⟶ W✝
h : ∀ {Z : CompHausLike P} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
a b : (fun X ↦ ↑X.toTop) X
hab : (ConcreteCategory.hom π) a = (ConcreteCategory.hom π) b
⊢ ofHom P { toFun := fun x ↦ a, continuous_toFun := ⋯ } ≫ π = ofHom P { toFun := fun x ↦ b, continuous_toFun := ⋯ } ≫ π

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
B X : CompHausLike P
π : X ⟶ B
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
W✝ : CompHausLike P
e : X ⟶ W✝
h : ∀ {Z : CompHausLike P} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
this : g = ofHom P (⋯.liftEquiv ⟨TopCat.Hom.hom e.hom, ⋯⟩)
⊢ g = ofHom P (⋯.lift (TopCat.Hom.hom e.hom) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
B X : CompHausLike P
π : X ⟶ B
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
W✝ : CompHausLike P
e : X ⟶ W✝
h : ∀ {Z : CompHausLike P} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
⊢ g = ofHom P (⋯.lift (TopCat.Hom.hom e.hom) ⋯)

Tactic:
by

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

Goal state before:
pp: k k' : Cont
v : List ℕ
⊢ stepRet (k.then k') v = (stepRet k v).then k'

Tactic:
by

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

Goal state before:
pp: c : Code
h : c.Ok
v : List ℕ
⊢ StateTransition.eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ ∀ {X Y Z : CompHausLike P} (f : X ⟶ Y) (g : Z ⟶ Y) [EffectiveEpi g], ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ g = h ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
inst✝¹ : HasExplicitPullbacks P
inst✝ : HasExplicitFiniteCoproducts P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ Precoherent (CompHausLike P)

Tactic:
by

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

Goal state before:
pp: case case
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v',
    (fun k v ↦ Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) v.headI) k v = Cfg.ret k' v'

Tactic:
simp only

Goal state after:
case case
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) v.headI = Cfg.ret k' v'
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: B X : CompHaus
π : X ⟶ B
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
x✝ : Epi (Sigma.desc π)
⊢ EffectiveEpiFamily X π

Tactic:
by

Goal state after:
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 Γ Λ σ
k : K
o : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
v : σ
S : List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
n : ℕ
H : n ≤ S.length
⊢ Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
    { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }

Tactic:
by

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

Goal state before:
pp: case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ some (TM1.stepAux (tr M (ret q)) v ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))) =
    some { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }

Tactic:
Option.some_inj,

Goal state after:
case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ TM1.stepAux (tr M (ret q)) v ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: c : Code
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal c k v = Cfg.ret k' v'

Tactic:
by

Goal state after:
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 Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
x✝ : ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b
e : ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b := x✝
⊢ Epi (Sigma.desc π)

Tactic:
by

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

Goal state before:
pp: f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) → ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)

Tactic:
by

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

Goal state before:
pp: f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) → ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)

Tactic:
by
      intro h
      obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
        this _ h _ _ (stepNormal_then _ Cont.halt _ _) ReflTransGen.refl
      refine ⟨v₂, PFun.mem_fix_iff.2 ?_, h₃⟩
      simp only [Part.eq_some_iff.2 hv₁, Part.map_some]
      split_ifs at hv₂ ⊢
      · rw [Part.mem_some_iff.1 hv₂]
        exact Or.inl (Part.mem_some _)
      · exact Or.inr ⟨_, Part.mem_some _, hv₂⟩

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

Goal state before:
pp: p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih✝ : (b : Λ') → Decidable (q = b)
p' : Γ' → Bool
k₁' k₂' : K'
q' : Λ'
⊢ move p k₁ k₂ q = move p' k₁' k₂' q' ↔ p = p' ∧ k₁ = k₁' ∧ k₂ = k₂' ∧ q = q'

Tactic:
by

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

Goal state before:
pp: p : Γ' → Bool
k : K'
q : Λ'
q_ih✝ : (b : Λ') → Decidable (q = b)
p' : Γ' → Bool
k' : K'
q' : Λ'
⊢ clear p k q = clear p' k' q' ↔ p = p' ∧ k = k' ∧ q = q'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
this✝ : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
this : i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
⊢ (ConcreteCategory.hom (π q.fst)) q.snd =
    (ConcreteCategory.hom (i.inv ≫ Sigma.desc π)) ((ConcreteCategory.hom i.hom) t)

Tactic:
by

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

Goal state before:
pp: q : Λ'
q_ih✝ : (b : Λ') → Decidable (q = b)
q' : Λ'
⊢ q.copy = q'.copy ↔ q = q'

Tactic:
by

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

Goal state before:
pp: k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih✝ : (b : Λ') → Decidable (q = b)
k' : K'
s' : Option Γ' → Option Γ'
q' : Λ'
⊢ push k s q = push k' s' q' ↔ k = k' ∧ s = s' ∧ q = q'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Epi (Sigma.desc π) := x✝
⊢ ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
⊢ [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b].TFAE

Tactic:
by

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

Goal state before:
pp: f : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
f' : Option Γ' → Λ'
⊢ read f = read f' ↔ ∀ (a : Option Γ'), f a = f' a

Tactic:
by

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

Goal state before:
pp: q : Λ'
q_ih✝ : (b : Λ') → Decidable (q = b)
q' : Λ'
⊢ q.succ = q'.succ ↔ q = q'

Tactic:
by

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

Goal state before:
pp: q₁ q₂ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂ = b)
q₁' q₂' : Λ'
⊢ q₁.pred q₂ = q₁'.pred q₂' ↔ q₁ = q₁' ∧ q₂ = q₂'

Tactic:
by

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

Goal state before:
pp: k k' : Cont'
⊢ ret k = ret k' ↔ k = k'

Tactic:
by

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

Goal state before:
pp: p✝¹ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ ¬move p✝¹ k₁✝ k₂✝ q✝¹ = clear p✝ k✝ q✝

Tactic:
by

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

Goal state before:
pp: p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ ¬move p✝ k₁✝ k₂✝ q✝¹ = q✝.copy

Tactic:
by

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

Goal state before:
pp: p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ ¬move p✝ k₁✝ k₂✝ q✝¹ = push k✝ s✝ q✝

Tactic:
by

Goal state after:
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 Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K), ListBlank.map (proj k) T = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q) v (Tape.mk' ∅ (addBottom T))) b
⊢ ∃ b,
    TrCfg (TM2.stepAux (stRun o q) v S) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal (stRun o q)) v (Tape.mk' ∅ (addBottom T))) b

Tactic:
simp only [trNormal_run, step_run]
  have hgo := tr_respects_aux₁ M o q v (hT k) _ le_rfl
  obtain ⟨T', hT', hrun⟩ := tr_respects_aux₂ (Λ := Λ) hT o
  have := hgo.tail' rfl
  rw [tr, TM1.stepAux, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_snd,
    stk_nth_val _ (hT k), List.getElem?_eq_none (le_of_eq List.length_reverse),
    Option.isNone, cond, hrun, TM1.stepAux] at this
  obtain ⟨c, gc, rc⟩ := IH hT'
  refine ⟨c, gc, (this.to₀.trans (tr_respects_aux₃ M _) c (TransGen.head' rfl ?_)).to_reflTransGen⟩
  rw [tr, TM1.stepAux, Tape.mk'_head, addBottom_head_fst]
  exact rc

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

Goal state before:
pp: p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ ¬move p✝ k₁✝ k₂✝ q✝ = read f✝

Tactic:
by

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

Goal state before:
pp: p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ ¬move p✝ k₁✝ k₂✝ q✝¹ = q✝.succ

Tactic:
by

Goal state after: