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

Goal state before:
pp: case succ
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v

Tactic:
obtain ⟨cg, hg₁⟩ := hg 0

Goal state after:
case succ
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg₁ : ∀ (v : List.Vector ℕ m), cg.eval ↑v = pure <$> g 0 v
⊢ ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
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:
ext ⟨a, x⟩
  specialize h a
  apply_fun (fun q ↦ q x) at h
  exact h

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

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

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

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

Goal state before:
pp: case cons
_f fs : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal _f k v = Cfg.ret k' v'
_IHfs : ∀ (k : Cont) (v : List ℕ), ∃ k' v', stepNormal fs k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ k' v', stepNormal (_f.cons fs) k v = Cfg.ret k' v'

Tactic:
| cons _f fs IHf _IHfs =>

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✝
b : ↑B.toTop
⊢ ∃ a, (ConcreteCategory.hom (Sigma.desc π)) a = b

Tactic:
obtain ⟨t, x, h⟩ := e b

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 π)
x✝ : ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b
e : ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b := x✝
b : ↑B.toTop
t : α
x : ↑(X t).toTop
h : (ConcreteCategory.hom (π t)) x = b
⊢ ∃ a, (ConcreteCategory.hom (Sigma.desc π)) a = b
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case mp.halt
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step ((Cfg.halt v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.halt v').then (Cont.fix f k)) = 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')
⊢ ∃ 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₂)

Tactic:
rw [Cfg.then] at h IH

Goal state after:
case mp.halt
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step ((fun k' ↦ stepRet k' v') (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((fun k' ↦ stepRet k' v') (Cont.fix f k)) = 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')
⊢ ∃ 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₂)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case mp.ret
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v : List ℕ
k' : Cont
v' : List ℕ
h : x ∈ eval step ((Cfg.ret k' v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.ret k' v').then (Cont.fix f k)) = 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.ret k' v')
⊢ ∃ 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₂)

Tactic:
rw [Cfg.then] at h IH

Goal state after:
case mp.ret
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v : List ℕ
k' : Cont
v' : List ℕ
h : x ∈ eval step ((fun k'_1 ↦ Cfg.ret (k'.then k'_1) v') (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((fun k'_1 ↦ Cfg.ret (k'.then k'_1) v') (Cont.fix f k)) = 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.ret k' v')
⊢ ∃ 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₂)
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Profinite
j k : J
⊢ ∀ (f : j ⟶ k),
    ((Functor.const J).obj
              { toTop := (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop, is_compact := ⋯, is_hausdorff := ⋯,
                prop := ⋯ }).map
          f ≫
        InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app k).hom =
      InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app j).hom ≫ F.map f

Tactic:
f

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Profinite
j k : J
f : j ⟶ k
⊢ ((Functor.const J).obj
            { toTop := (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop, is_compact := ⋯, is_hausdorff := ⋯,
              prop := ⋯ }).map
        f ≫
      InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app k).hom =
    InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app j).hom ≫ F.map f
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: ⊢ Limits.PreservesLimits (forget Profinite)

Tactic:
apply Limits.comp_preservesLimits Profinite.toTopCat (forget TopCat)

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : CompactSpace Z
_csZ : T2Space Z
⊢ ∀ {f : StoneCech X → Z} {g : Y → Z}, Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
f

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ✝ : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
⊢ ∀ {g : Y → Z}, Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
⊢ IsOpen (closure U)

Tactic:
have f_sur : Surjective f := by
    intro x
    by_cases hx : x ∈ U
    · exact ⟨⟨(x, false), Or.inr ⟨subset_closure hx, mem_singleton _⟩⟩, rfl⟩
    · exact ⟨⟨(x, true), Or.inl ⟨hx, mem_singleton _⟩⟩, rfl⟩

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
⊢ IsOpen (closure U)
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
⊢ ∀ {g : B → C}, Continuous φ → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = φ

Tactic:
f

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
⊢ Continuous φ → Continuous f → Surjective f → ∃ h, Continuous h ∧ f ∘ h = φ
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
⊢ ∀ {f : ↑X.toTop → B} {g : A → B},
    Continuous[_, inst✝⁴] f →
      Continuous[inst✝⁵, inst✝⁴] g → Function.Surjective g → ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f

Tactic:
f

Goal state after:
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
f : ↑X.toTop → B
⊢ ∀ {g : A → B},
    Continuous[_, inst✝⁴] f →
      Continuous[inst✝⁵, inst✝⁴] g → Function.Surjective g → ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f
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)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
⊢ Sigma.mk i ⁻¹' closure s = closure (Sigma.mk i ⁻¹' s)

Tactic:
apply IsOpenMap.preimage_closure_eq_closure_preimage

Goal state after:
case hf
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
⊢ IsOpenMap (Sigma.mk i)

case hfc
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
⊢ Continuous (Sigma.mk i)
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
⊢ ∀ (e : B ⟶ C) [Epi e], ∃ f', f' ≫ e = φ

Tactic:
f

Goal state after:
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
⊢ ∀ [Epi f], ∃ f', f' ≫ f = φ
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
⊢ ∀ (e : B ⟶ C) [Epi e], ∃ f', f' ≫ e = φ

Tactic:
f

Goal state after:
X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
f : B ⟶ C
⊢ ∀ [Epi f], ∃ f', f' ≫ f = φ
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X B C : Stonean
φ : X ⟶ C
⊢ ∀ (e : B ⟶ C) [Epi e], ∃ f', f' ≫ e = φ

Tactic:
f

Goal state after:
X B C : Stonean
φ : X ⟶ C
f : B ⟶ C
⊢ ∀ [Epi f], ∃ f', f' ≫ f = φ
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case zero
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trNum Num.zero ++ [Γ'.cons]) [] c d }
    { l := some q, var := none, stk := elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d }

pp: case pos
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
⊢ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trNum (Num.pos a) ++ [Γ'.cons]) [] c d }
    { l := some q, var := none, stk := elim (trNum (Num.pos a).succ ++ [Γ'.cons]) [] c d }

Tactic:
· refine TransGen.head rfl ?_
    simp only [Option.mem_def]
    convert! unrev_ok using 1
    simp only [elim_update_rev, elim_rev, elim_main, List.reverseAux_nil, elim_update_main]
    rfl

Goal state after:
case pos
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
⊢ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trNum (Num.pos a) ++ [Γ'.cons]) [] c d }
    { l := some q, var := none, stk := elim (trNum (Num.pos a).succ ++ [Γ'.cons]) [] c d }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pos
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
⊢ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trNum (Num.pos a) ++ [Γ'.cons]) [] c d }
    { l := some q, var := none, stk := elim (trNum (Num.pos a).succ ++ [Γ'.cons]) [] c d }

Tactic:
simp only [trNum, Num.succ, Num.succ']

Goal state after:
case pos
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
⊢ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) [] c d }
    { l := some q, var := none, stk := elim (trPosNum a.succ ++ [Γ'.cons]) [] c d }
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 ∈ ⋂ s, ↑s

Tactic:
mem_iInter

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
⊢ ∀ (i : { s // IsClopen s ∧ y ∈ s }), x ∈ ↑i
Module: Mathlib.Topology.Category.LightProfinite.EffectiveEpi

Goal state before:
pp: X✝ Y✝ : CompHausLike fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X
⊢ ∀ (f : X✝ ⟶ Y✝), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
f

Goal state after:
X✝ Y✝ : CompHausLike fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X
f : X✝ ⟶ Y✝
⊢ EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
j k : J
⊢ ∀ (f : j ⟶ k),
    ((Functor.const J).obj
              { toTop := (CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop, is_compact := ⋯,
                is_hausdorff := ⋯, prop := ⋯ }).map
          f ≫
        ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app k).hom) =
      ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app j).hom) ≫
        F.map f

Tactic:
f

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
j k : J
f : j ⟶ k
⊢ ((Functor.const J).obj
            { toTop := (CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop, is_compact := ⋯, is_hausdorff := ⋯,
              prop := ⋯ }).map
        f ≫
      ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app k).hom) =
    ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app j).hom) ≫ F.map f
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: X Y : LightProfinite
f : X ⟶ Y
A B : LightProfinite
⊢ ∀ (f : A ⟶ B) [IsIso ((forget LightProfinite).map f)], IsIso f

Tactic:
f

Goal state after:
X Y : LightProfinite
f✝ : X ⟶ Y
A B : LightProfinite
f : A ⟶ B
⊢ ∀ [IsIso ((forget LightProfinite).map f)], IsIso f
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: X✝ Y✝ : LightDiagram
⊢ ∀ (f : X✝ ⟶ Y✝),
    (lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).map f ≫
        (lightDiagramToProfinite.preimageIso
            (Iso.refl
              (lightDiagramToProfinite.obj
                ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj Y✝)))).hom =
      (lightDiagramToProfinite.preimageIso
            (Iso.refl
              (lightDiagramToProfinite.obj
                ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj X✝)))).hom ≫
        (𝟭 LightDiagram).map f

Tactic:
f

Goal state after:
X✝ Y✝ : LightDiagram
f : X✝ ⟶ Y✝
⊢ (lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).map f ≫
      (lightDiagramToProfinite.preimageIso
          (Iso.refl
            (lightDiagramToProfinite.obj ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj Y✝)))).hom =
    (lightDiagramToProfinite.preimageIso
          (Iso.refl
            (lightDiagramToProfinite.obj ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj X✝)))).hom ≫
      (𝟭 LightDiagram).map f
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move
q' : Λ'
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p✝ k₁✝ k₂✝ q)

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Goal state after:
case move
q' : Λ'
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case clear
q' : Λ'
p✝ : Γ' → Bool
k✝ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.clear p✝ k✝ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p✝ k✝ q)

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Goal state after:
case clear
q' : Λ'
p✝ : Γ' → Bool
k✝ : K'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.clear p✝ k✝ q) (trStmts₁ q)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case copy
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Goal state after:
case copy
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.copy (trStmts₁ q)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case push
q' : Λ'
k✝ : K'
s✝ : Option Γ' → Option Γ'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ (Λ'.push k✝ s✝ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k✝ s✝ q)

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Goal state after:
case push
q' : Λ'
k✝ : K'
s✝ : Option Γ' → Option Γ'
q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert (Λ'.push k✝ s✝ q) (trStmts₁ q)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case read
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
⊢ q' ∈ trStmts₁ (Λ'.read q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.read q)

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Goal state after:
case read
q' : Λ'
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)
⊢ (q' ∈ Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) →
    trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.succ → trStmts₁ q' ⊆ trStmts₁ q.succ

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Goal state after:
case succ
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ (q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))) ∧
    (q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q)))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
⊢ q' ∈ trStmts₁ (q₁.pred q₂) → trStmts₁ q' ⊆ trStmts₁ (q₁.pred q₂)

Tactic:
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union,
      or_imp, Finset.mem_singleton, Finset.Subset.refl, imp_true_iff, true_and]

Goal state after:
case pred
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
⊢ (q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
    (q' = unrev q₂ → trStmts₁ (unrev q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
      (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))