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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
l₁ : Option Λ
v : σ
T : Tape Γ
⊢ FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := l₁, var := v, Tape := T })
    (step M { l := l₁, var := v, Tape := T })

Tactic:
obtain ⟨L, R, rfl⟩ := T.exists_mk'

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
l₁ : Option Λ
v : σ
L R : ListBlank Γ
⊢ FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := l₁, var := v, Tape := Tape.mk' L R })
    (step M { l := l₁, var := v, Tape := Tape.mk' L R })
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case zero
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ zero.rmatch x = true ↔ x ∈ zero.matches'

Tactic:
rw [zero_def, zero_rmatch]

Goal state after:
case zero
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ false = true ↔ x ∈ matches' 0
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
v : σ
L R : ListBlank Γ
l₁ : Λ
⊢ FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := some l₁, var := v, Tape := Tape.mk' L R })
    (step M { l := some l₁, var := v, Tape := Tape.mk' L R })

Tactic:
suffices ∀ q R, Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
        (trCfg enc enc0 (stepAux q v (Tape.mk' L R))) by
      refine TransGen.head' rfl ?_
      rw [trTape_mk']
      exact this _ R

Goal state after:
case some
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
v : σ
L R : ListBlank Γ
l₁ : Λ
⊢ ∀ (q : Stmt Γ Λ σ) (R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case pos
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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h✝ : v₁.headI = 0
hv₂ : v₂ ∈ pure v₁.tail
⊢ Sum.inl v₂ ∈ Part.some (Sum.inl v₁.tail) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inl v₁.tail) ∧
        v₂ ∈ PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) a'

Tactic:
Part.mem_some_iff.1 hv₂

Goal state after:
case pos
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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h✝ : v₁.headI = 0
hv₂ : v₂ ∈ pure v₁.tail
⊢ Sum.inl v₁.tail ∈ Part.some (Sum.inl v₁.tail) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inl v₁.tail) ∧
        v₁.tail ∈
          PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) a'
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:
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 (Cont.halt.then (Cont.fix f k)) v'.tail = (Cfg.ret k₀ v₀).then (Cont.fix f k)
⊢ ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case some.cons
α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun a ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
⊢ (bif p a then ([], some a, l₁.append (o :: l₂))
    else
      match splitAtPred p (l₁.append (o :: l₂)) with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a :: l₁, some o, l₂)

Tactic:
rw [h₁ a (List.Mem.head _), cond, IH l₁ (some o) l₂ _ ⟨h₂, _⟩]

Goal state after:
α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun a ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
⊢ ∀ x ∈ l₁, p x = false

α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun a ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
⊢ l₁.append (o :: l₂) = l₁ ++ o :: l₂
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
f_sur : Surjective f
this✝ : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
⊢ IsOpen (closure U)

Tactic:
by
    rw [this, preimage_comp, ← isClosed_compl_iff, ← preimage_compl,
      ← preimage_subtype_coe_eq_compl Subset.rfl]
    · exact hZ₁.preimage hφ
    · rw [hZ₁₂.inter_eq, inter_empty]

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

Goal state before:
pp: p : Γ' → Bool
k : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
e : 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₂ }

Tactic:
by
  induction L₁ generalizing S s with
  | nil =>
    refine TransGen.head' rfl ?_
    rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
    revert e; rcases S k with - | ⟨a, Sk⟩ <;> intro e
    · cases e
      rfl
    simp only [splitAtPred, List.head?, List.tail_cons] at e ⊢
    revert e; cases p a <;> intro e <;>
      simp only [cond_false, cond_true, Prod.mk.injEq, true_and, false_and, reduceCtorEq] at e ⊢
    rcases e with ⟨e₁, e₂⟩
    rw [e₁, e₂]
  | cons a L₁ IH =>
    refine TransGen.head rfl ?_
    rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
    rcases e₁ : S k with - | ⟨a', Sk⟩ <;> rw [e₁, splitAtPred] at e
    · cases e
    cases e₂ : p a' <;> simp only [e₂, cond] at e
    swap
    · cases e
    rcases e₃ : splitAtPred p Sk with ⟨_, _, _⟩
    rw [e₃] at e
    cases e
    simp only [List.head?_cons, e₂, List.tail_cons, cond_false]
    convert! @IH _ (update S k Sk) _ using 2 <;> simp [e₃]

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: 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)

Tactic:
· fun_prop

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

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

Tactic:
((CompHaus.effectiveEpiFamily_tfae
      (fun a ↦ Stonean.toCompHaus.obj (X a)) (fun a ↦ Stonean.toCompHaus.map (π a))).out 2 0 :)

Goal state after:
α : Type
inst✝ : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
⊢ (EffectiveEpiFamily (fun a ↦ toCompHaus.obj (X a)) fun a ↦ toCompHaus.map (π a)) ↔ EffectiveEpiFamily X π
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case insert
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
_ha : a ∉ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S → (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ E, P e ∈ S) → ⋂ e ∈ E, P e ∈ S
⊢ ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S →
      (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ insert a E, P e ∈ S) → ⋂ e ∈ insert a E, P e ∈ S

Tactic:
intro hh2

Goal state after:
case insert
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
S : Set (Set ↑(F.obj j))
a : J
E : Finset J
_ha : a ∉ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S → (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ E, P e ∈ S) → ⋂ e ∈ E, P e ∈ S
hh2 : J → Set ↑(F.obj j)
⊢ Set.univ ∈ S →
    (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ insert a E, hh2 e ∈ S) → ⋂ e ∈ insert a E, hh2 e ∈ S
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
⊢ ∃ j V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V

Tactic:
have hV : ∀ s : S, IsClopen (V s) ∧ s.1 = C.π.app (j s) ⁻¹' V s := fun s =>
    (hS s.2).choose_spec.choose_spec

Goal state after:
case refine_3
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
⊢ ∃ j V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: S : LightDiagram
⊢ ∀ (a : ℕ), Countable (LocallyConstant (↑((S.diagram ⋙ toProfinite).obj (op a)).toTop) (Fin 2))

Tactic:
intro n

Goal state after:
S : LightDiagram
n : ℕ
⊢ Countable (LocallyConstant (↑((S.diagram ⋙ toProfinite).obj (op n)).toTop) (Fin 2))
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₁ q → trStmts₁ q' ⊆ insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q)

Tactic:
repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Goal state after:
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₁ q → trStmts₁ q' ⊆ insert (Λ'.clear p✝ k✝ q) (trStmts₁ q)

Tactic:
repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Goal state after:
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 → trStmts₁ q' ⊆ insert q.copy (trStmts₁ q)

Tactic:
repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Goal state after:
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₁ q → trStmts₁ q' ⊆ insert (Λ'.push k✝ s✝ q) (trStmts₁ q)

Tactic:
repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Goal state after:
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' ∈ Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) →
    trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s))

Tactic:
repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

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' = 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)))

Tactic:
repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

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₁ → 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₂)))

Tactic:
repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

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₂)))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:

Tactic:
repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)

Goal state after:
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' ∈ Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) →
    trStmts₁ q' ⊆ insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s))

pp: 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)))

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₁ → 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₂)))

Tactic:
· simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, forall_exists_index]
    intro s h x h'
    simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, Finset.mem_insert]
    exact Or.inr ⟨_, q_ih s h h'⟩

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)))

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₂)))
Module: Mathlib.Topology.Category.LightProfinite.AsLimit

Goal state before:
pp: S : LightProfinite
n : ℕ
c : Cone (S.diagram ⋙ lightToProfinite) := S.toLightDiagram.cone
⊢ ConcreteCategory.ofHom (TopCat.Hom.hom (S.proj n).hom) =
    (lightToProfinite.obj S).asLimitCone.π.app
      ((IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))

Tactic:
let hc : IsLimit c := S.toLightDiagram.isLimit

Goal state after:
S : LightProfinite
n : ℕ
c : Cone (S.diagram ⋙ lightToProfinite) := S.toLightDiagram.cone
hc : IsLimit c := S.toLightDiagram.isLimit
⊢ ConcreteCategory.ofHom (TopCat.Hom.hom (S.proj n).hom) =
    (lightToProfinite.obj S).asLimitCone.π.app
      ((IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x ↦ false) main aux
          (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main (move₂ (fun x ↦ false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
H₂ : codeSupp f k.cons₂ ⊆ S
h : codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
⊢ Supports (codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k)) S

Tactic:
refine supports_union.2 ⟨codeSupp'_supports H₂, ?_⟩

Goal state after:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x ↦ false) main aux
          (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main (move₂ (fun x ↦ false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
H₂ : codeSupp f k.cons₂ ⊆ S
h : codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
⊢ Supports (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) S
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f✝ : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
f : ℕ → ↑X
⊢ ∀ ⦃p : ↑X⦄,
    Filter.Tendsto f Filter.atTop (nhds p) →
      Filter.Tendsto ((topCatAdjunctionCounitEquiv X).invFun ∘ f) Filter.atTop
        (nhds ((topCatAdjunctionCounitEquiv X).invFun p))

Tactic:
p

Goal state after:
X✝ Y : LightCondSet
f✝ : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
f : ℕ → ↑X
p : ↑X
⊢ Filter.Tendsto f Filter.atTop (nhds p) →
    Filter.Tendsto ((topCatAdjunctionCounitEquiv X).invFun ∘ f) Filter.atTop
      (nhds ((topCatAdjunctionCounitEquiv X).invFun p))