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

Goal state before:
pp: case rfind.mp
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)]
v' : List ℕ
⊢ ∀ (v₁ : List ℕ),
    v' ∈
        PFun.fix
          (fun v ↦
            (cf.eval v).bind fun y ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          v₁ →
      ∀ (n_1 : ℕ),
        v₁ = n_1 :: ↑v →
          (∀ m < n_1, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
intro v₀ h1

Goal state after:
case rfind.mp
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)]
v' v₀ : List ℕ
h1 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      v₀
⊢ ∀ (n_1 : ℕ),
    v₀ = n_1 :: ↑v →
      (∀ m < n_1, ¬f (m ::ᵥ v) = 0) →
        ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case right.e_a.e_a.cons
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) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[(head✝ :: tail✝).length] (Tape.mk' ∅ (addBottom L)))).head.2 k =
    (head✝ :: tail✝).head?

Tactic:
rw [List.length_cons, iterate_succ', Function.comp, Tape.move_right_left,
      Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_snd, stk_nth_val _ (hL k), e,
      List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length]

Goal state after:
case right.e_a.e_a.cons
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) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ some head✝ = (head✝ :: tail✝).head?
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:
refine IsOpenEmbedding.of_comp _ (homeoOfIso ((colimit.isColimit _).coconePointUniqueUpToIso
    (finiteCoproduct.isColimit X))).isOpenEmbedding ?_
  convert! finiteCoproduct.isOpenEmbedding_ι X a
  ext x
  change (Sigma.ι X a ≫ _) x = _
  simp

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

Goal state before:
pp: case cons
k' : Cont
c c' : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal (c.cons c') (k.then k') v = (stepNormal (c.cons c') k v).then k'

Tactic:
simp only [stepNormal, *]

Goal state after:
case cons
k' : Cont
c c' : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
k' : Cont
c c' : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal (c.comp c') (k.then k') v = (stepNormal (c.comp c') k v).then k'

Tactic:
simp only [stepNormal, *]

Goal state after:
case comp
k' : Cont
c c' : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case case
k' : Cont
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), stepNormal a✝¹ (k.then k') v = (stepNormal a✝¹ k v).then k'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal a✝ (k.then k') v = (stepNormal a✝ k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal (a✝¹.case a✝) (k.then k') v = (stepNormal (a✝¹.case a✝) k v).then k'

Tactic:
simp only [stepNormal, *]

Goal state after:
case case
k' : Cont
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), stepNormal a✝¹ (k.then k') v = (stepNormal a✝¹ k v).then k'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal a✝ (k.then k') v = (stepNormal a✝ k v).then k'
k : Cont
v : List ℕ
⊢ Nat.rec ((stepNormal a✝¹ k v.tail).then k') (fun y x ↦ (stepNormal a✝ k (y :: v.tail)).then k') v.headI =
    (Nat.rec (stepNormal a✝¹ k v.tail) (fun y x ↦ stepNormal a✝ k (y :: v.tail)) v.headI).then k'
Module: Mathlib.Computability.TuringMachine.Config

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

Tactic:
simp only [stepNormal, *]

Goal state after:
case fix
k' : Cont
c : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c (Cont.fix c (k.then k')) v = (stepNormal c (Cont.fix c k) v).then k'
Module: Mathlib.Computability.TuringMachine.Config

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

Tactic:
simp only [stepNormal, *]

Goal state after:
case zero'
k' k : Cont
v : List ℕ
⊢ Cfg.ret (k.then k') (0 :: v) = (Cfg.ret k (0 :: v)).then k'
Module: Mathlib.Computability.TuringMachine.Config

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

Tactic:
simp only [stepNormal, *]

Goal state after:
case succ
k' k : Cont
v : List ℕ
⊢ Cfg.ret (k.then k') [v.headI.succ] = (Cfg.ret k [v.headI.succ]).then k'
Module: Mathlib.Computability.TuringMachine.Config

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

Tactic:
simp only [stepNormal, *]

Goal state after:
case tail
k' k : Cont
v : List ℕ
⊢ Cfg.ret (k.then k') v.tail = (Cfg.ret k v.tail).then k'
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:
ext

Goal state after:
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
a✝ : ↑(of P ↑X.1).toTop
⊢ (ConcreteCategory.hom (ofHom P { toFun := fun x ↦ a, continuous_toFun := ⋯ } ≫ π)) a✝ =
    (ConcreteCategory.hom (ofHom P { toFun := fun x ↦ b, continuous_toFun := ⋯ } ≫ π)) a✝
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:
ext; exact hab

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:
ext

Goal state after:
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
a✝ : ↑(of P ↑X.1).toTop
⊢ (ConcreteCategory.hom (ofHom P { toFun := fun x ↦ a, continuous_toFun := ⋯ } ≫ π)) a✝ =
    (ConcreteCategory.hom (ofHom P { toFun := fun x ↦ b, continuous_toFun := ⋯ } ≫ π)) a✝
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:
ext; exact hab

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
⊢ ⋯.liftEquiv.symm (ConcreteCategory.hom g) = ⟨TopCat.Hom.hom e.hom, ⋯⟩

Tactic:
ext

Goal state after:
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✝ : (fun X ↦ ↑X.toTop) X
⊢ ↑(⋯.liftEquiv.symm (ConcreteCategory.hom g)) a✝ = ↑⟨TopCat.Hom.hom e.hom, ⋯⟩ a✝
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)

Tactic:
constructor

Goal state after:
case mp
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) → ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)

case mpr
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
⊢ (∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)) → x ∈ eval step (stepNormal f (Cont.fix f k) v)
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)
⊢ (ConcreteCategory.hom (π q.fst)) q.snd =
    (ConcreteCategory.hom (Sigma.desc π)) ((ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t))

Tactic:
change _ = (i.inv ≫ Sigma.desc π) (i.hom t)

Goal state after:
α : 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)
⊢ (ConcreteCategory.hom (π q.fst)) q.snd =
    (ConcreteCategory.hom (i.inv ≫ Sigma.desc π)) ((ConcreteCategory.hom i.hom) t)
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)
a : α
⊢ π a = finiteCoproduct.ι X a ≫ finiteCoproduct.desc X π

Tactic:
ext

Goal state after:
α : 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)
a : α
a✝ : ↑(X a).toTop
⊢ (ConcreteCategory.hom (π a)) a✝ = (ConcreteCategory.hom (finiteCoproduct.ι X a ≫ finiteCoproduct.desc X π)) a✝
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case none
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
⊢ match TM2.step M { l := none, var := v, stk := S } with
  | some b₁ =>
    ∃ b₂,
      TrCfg b₁ b₂ ∧
        Reaches₁ (TM1.step (tr M)) { l := Option.map normal none, var := v, Tape := Tape.mk' ∅ (addBottom L) } b₂
  | none => TM1.step (tr M) { l := Option.map normal none, var := v, Tape := Tape.mk' ∅ (addBottom L) } = none

Tactic:
constructor

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
h : IsTopologicalBasis {s | IsClopen s}
⊢ TotallySeparatedSpace X

Tactic:
constructor

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
h : IsTopologicalBasis {s | IsClopen s}
⊢ IsTotallySeparated univ
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
⊢ U ∈ 𝓝 x ↔ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
⊢ U ∈ 𝓝 x → ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

case mpr
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
⊢ (∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U) → U ∈ 𝓝 x
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case neg
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.halt.then (Cont.fix f k)) v'.tail = (stepNormal f Cont.halt v'.tail).then (Cont.fix f k)
⊢ ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
rw [e₀, Cont.then, Cfg.then] at e₁

Goal state after:
case neg
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 ((fun k' ↦ k') (Cont.fix f k)) v'.tail = (fun k' ↦ Cfg.ret (k₀.then k') v₀) (Cont.fix f k)
⊢ ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H

Tactic:
constructor

Goal state after:
case mp
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallyDisconnectedSpace H → TotallySeparatedSpace H

case mpr
H : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallySeparatedSpace H → TotallyDisconnectedSpace H
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 ((fun k v ↦ stepNormal f (Cont.cons₁ fs v k) v) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)

Tactic:
Code.eval,

Goal state after:
case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal f (Cont.cons₁ fs v k) v) k v) = 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 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:
Code.eval,

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 ← (fun v ↦ g.eval v >>= f.eval) v
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: c : Code
⊢ c.Ok

Tactic:
by
  induction c with (intro k v; rw [stepNormal])
  | cons f fs IHf IHfs =>
    rw [Code.eval, IHf]
    simp only [bind_assoc, pure_bind]; congr; funext v
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IHfs]; congr; funext v'
    refine Eq.trans (b := eval step (stepRet (Cont.cons₂ v k) v')) ?_ (Eq.symm ?_) <;>
      exact reaches_eval (ReflTransGen.single rfl)
  | comp f g IHf IHg =>
    rw [Code.eval, IHg]
    simp only [bind_assoc]; congr; funext v
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IHf]
  | case f g IHf IHg =>
    simp only [Code.eval]
    cases v.headI <;> simp only [Nat.rec_zero, Part.bind_eq_bind] <;> [apply IHf; apply IHg]
  | fix f IHf => rw [cont_eval_fix IHf]
  | _ => simp only [Code.eval, pure_bind]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: X Y : Profinite
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
constructor

Goal state after:
case mp
X Y : Profinite
f : X ⟶ Y
⊢ Epi f → Function.Surjective ⇑(ConcreteCategory.hom f)

case mpr
X Y : Profinite
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
⊢ (ρ '' G₁ᶜ ∪ ρ '' G₂ᶜ)ᶜ = ∅

Tactic:
← image_union,

Goal state after:
A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
⊢ (ρ '' (G₁ᶜ ∪ G₂ᶜ))ᶜ = ∅
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀ : ∀ (i : ι), ExtremallyDisconnected (X i)
⊢ ExtremallyDisconnected ((i : ι) × X i)

Tactic:
constructor

Goal state after:
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀ : ∀ (i : ι), ExtremallyDisconnected (X i)
⊢ ∀ (U : Set ((i : ι) × X i)), IsOpen U → IsOpen (closure U)
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Type u_1
inst✝² : Finite X
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ ExtremallyDisconnected X

Tactic:
constructor

Goal state after:
X : Type u_1
inst✝² : Finite X
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ ∀ (U : Set X),
    IsOpen[(CompHaus.of X).toTop.str] U → IsOpen[(CompHaus.of X).toTop.str] (closure[(CompHaus.of X).toTop.str] U)
Module: Mathlib.Condensed.Basic

Goal state before:
pp: C : Type w
inst✝ : Category.{v, w} C
X Y : Condensed C
f g : X ⟶ Y
h : ∀ (S : CompHausᵒᵖ), f.hom.app S = g.hom.app S
⊢ f = g

Tactic:
ext

Goal state after:
C : Type w
inst✝ : Category.{v, w} C
X Y : Condensed C
f g : X ⟶ Y
h : ∀ (S : CompHausᵒᵖ), f.hom.app S = g.hom.app S
x✝ : CompHausᵒᵖ
⊢ f.hom.app x✝ = g.hom.app x✝