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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
L R : ListBlank Γ
⊢ move Dir.right (mk' L R) = mk' (ListBlank.cons R.head L) R.tail

Tactic:
simp only [Tape.move, Tape.mk']

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ RecursiveIn O g

Tactic:
rw [iff_nat]

Goal state after:
O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ Nat.RecursiveIn O g
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
⊢ SupportsStmt S q₁

Tactic:
induction q₂ with
    simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs
  | branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
  | goto l => subst h; exact hs
  | halt => subst h; trivial
  | _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

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

Goal state before:
pp: case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d)^[i + 1] q) v T = stepAux q v ((Tape.move d)^[i + 1] T)

Tactic:
| succ i IH =>

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

Goal state before:
pp: case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ SupportsStmt S (readAux (i + 1) f)

Tactic:
| succ i IH =>

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

Goal state before:
pp: case succ
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
L✝ : Tape Bool
i : ℕ
IH : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L✝) = L✝
⊢ (Tape.move Dir.right)^[i + 1] ((Tape.move Dir.left)^[i + 1] L✝) = L✝

Tactic:
| succ i IH =>

Goal state after:
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 → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L R : ListBlank Γ
this :
  ∀ (f : List.Vector Bool n → Stmt Bool (Λ' ?m.41 ?m.42 σ) σ),
    stepAux (readAux n f) v (trTape' enc0 L R) =
      stepAux (f (enc R.head)) v (trTape' enc0 (ListBlank.cons R.head L) R.tail)
⊢ stepAux (read dec f) v (trTape' enc0 L R) = stepAux (f R.head) v (trTape' enc0 L R)

Tactic:
by
    rw [read, this, stepAux_move, encdec, trTape'_move_left enc0]
    simp only [ListBlank.head_cons, ListBlank.cons_head_tail, ListBlank.tail_cons]

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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) n (addBottom L) = addBottom (ListBlank.modifyNth f n L)

Tactic:
cases n <;>
    simp only [addBottom, ListBlank.head_cons, ListBlank.modifyNth, ListBlank.tail_cons]

Goal state after:
case succ
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.cons (true, L.head)
      (ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)) =
    ListBlank.cons (true, L.head) (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos
n : ℕ
m : PosNum
⊢ m.testBit n = (↑(pos m)).testBit n

Tactic:
| pos m =>

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

Goal state before:
pp: case prim.prec.succ
n✝² : ℕ
f✝¹ : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
f : List.Vector ℕ n✝ → ℕ
g : List.Vector ℕ (n✝ + 2) → ℕ
a✝² : Nat.Primrec' f
a✝¹ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n✝ + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
a✝ :
  (cf.prec cg).eval (n :: (↑v).tail) =
    pure (pure (Nat.rec (f (n ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (n ::ᵥ v.tail).tail)) (n ::ᵥ v.tail).head))
a b : ℕ
e : a + b = n
⊢ n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail ∈
    PFun.fix
      (fun v ↦
        (cg.eval (v.headI :: v.tail.tail)).bind fun x ↦
          Part.some
            (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
            else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
      (a :: b :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail)

Tactic:
induction b generalizing a with
      | zero =>
        refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)
        simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]
        rfl
      | succ b IH =>
        refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH (a + 1) (by rwa [add_right_comm])⟩)
        simp only [hg, Part.bind_some, List.tail_cons, pure]
        exact Part.mem_some_iff.2 rfl

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

Goal state before:
pp: case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
l : Λ
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = 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 L))) b
IH₂ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = 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 L))) b
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
⊢ ∃ b,
    TrCfg (TM2.stepAux (TM2.Stmt.branch p q₁ q₂) v S) b ∧
      Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal (TM2.Stmt.branch p q₁ q₂)) v (Tape.mk' ∅ (addBottom L))) b

Tactic:
unfold TM2.stepAux trNormal TM1.stepAux

Goal state after:
case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
l : Λ
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = 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 L))) b
IH₂ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = 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 L))) b
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
⊢ ∃ b,
    TrCfg (bif p v then TM2.stepAux q₁ v S else TM2.stepAux q₂ v S) b ∧
      Reaches (TM1.step (tr M))
        (bif (fun x ↦ p) (Tape.mk' ∅ (addBottom L)).head v then TM1.stepAux (trNormal q₁) v (Tape.mk' ∅ (addBottom L))
        else TM1.stepAux (trNormal q₂) v (Tape.mk' ∅ (addBottom L)))
        b
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos.refine_2
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ (↑c ∩ X ⁻¹' {a}).Nonempty

pp: case pos.refine_3
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ X ⁻¹' {a})

pp: case pos.refine_4
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ X ⁻¹' {a})

Tactic:
· rw [← image_inter_nonempty_iff, (C_sub c.mem).right, univ_inter]
      exact singleton_nonempty a

Goal state after:
case pos.refine_3
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ X ⁻¹' {a})

case pos.refine_4
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ X ⁻¹' {a})
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
⊢ Injective ρ

Tactic:
intro x₁ x₂ hρx
  by_contra hx
  -- let $G_1$ and $G_2$ be disjoint open neighbourhoods of $x_1$ and $x_2$ respectively
  rcases t2_separation hx with ⟨G₁, G₂, G₁_open, G₂_open, hx₁, hx₂, disj⟩
  -- prove $A \setminus \rho(E - G_1)$ and $A \setminus \rho(E - G_2)$ are disjoint
  have G₁_comp : IsCompact G₁ᶜ := IsClosed.isCompact G₁_open.isClosed_compl
  have G₂_comp : IsCompact G₂ᶜ := IsClosed.isCompact G₂_open.isClosed_compl
  have G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ := (G₁_comp.image ρ_cont).isClosed.isOpen_compl
  have G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ := (G₂_comp.image ρ_cont).isClosed.isOpen_compl
  have disj' : Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ := by
    rw [disjoint_iff_inter_eq_empty, ← compl_union, ← image_union, ← compl_inter,
      disjoint_iff_inter_eq_empty.mp disj, compl_empty, compl_empty_iff,
      image_univ_of_surjective ρ_surj]
  -- apply Lemma 2.2 to prove their closures are disjoint
  have disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ) :=
    disjoint_closure_of_disjoint_isOpen disj' G₁_open' G₂_open'
  -- apply Lemma 2.1 to prove $\rho(x_1) = \rho(x_2)$ lies in their intersection
  have hx₁' := image_subset_closure_compl_image_compl_of_isOpen ρ_cont ρ_surj zorn_subset G₁_open <|
    mem_image_of_mem ρ hx₁
  have hx₂' := image_subset_closure_compl_image_compl_of_isOpen ρ_cont ρ_surj zorn_subset G₂_open <|
    mem_image_of_mem ρ hx₂
  exact disj''.ne_of_mem hx₁' hx₂' hρx

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

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

Tactic:
rcases (E_onto ▸ mem_univ a : a ∈ X₁ '' E) with ⟨d, ⟨hd, rfl⟩⟩

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

Goal state before:
pp: case nil
q : Λ'
c : List Γ'
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a [] c d }
    { l := some q, var := none, stk := elim ([].reverseAux a) [] c ([].reverseAux d) }

Tactic:
refine TransGen.single ?_

Goal state after:
case nil
q : Λ'
c : List Γ'
s : Option Γ'
a d : List Γ'
⊢ { l := some q, var := none, stk := elim ([].reverseAux a) [] c ([].reverseAux d) } ∈
    TM2.step tr { l := some q.copy, var := s, stk := elim a [] c d }
Module: Mathlib.Computability.TuringMachine.ToPartrec

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

Tactic:
| bit0 m _ =>

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_3.mp
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
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i ↦ if h : i = j then ⋯.mpr V else Set.univ
⊢ ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V ∈
    {S | ∃ U F_1, (∀ i ∈ F_1, U i ∈ T i) ∧ S = ⋂ i ∈ F_1, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i}

Tactic:
refine ⟨U, {j}, ?_, ?_⟩

Goal state after:
case e'_3.mp.refine_1
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
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i ↦ if h : i = j then ⋯.mpr V else Set.univ
⊢ ∀ i ∈ {j}, U i ∈ T i

case e'_3.mp.refine_2
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
j : J
V : Set ↑(F.obj j)
hV : V ∈ T j
U : (i : J) → Set ↑(F.obj i) := fun i ↦ if h : i = j then ⋯.mpr V else Set.univ
⊢ ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V = ⋂ i ∈ {j}, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: case refine_1
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
f : ↑{s | IsClopen s} → Clopens X := fun s ↦ { carrier := ↑s, isClopen' := ⋯ }
⊢ {s | IsClopen s}.Countable

Tactic:
exact Injective.of_eq_imp_le (f := f) (·.le) |>.countable

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

Goal state before:
pp: case refine_2
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
i j : J
f : i ⟶ j
V : Set ↑((F ⋙ toTopCat).obj j)
hV : IsClopen V
⊢ ⇑(ConcreteCategory.hom ((F ⋙ toTopCat).map f)) ⁻¹' V ∈ {W | IsClopen W}

Tactic:
refine ⟨hV.1.preimage ?_, hV.2.preimage ?_⟩ <;> fun_prop

Goal state after:
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 V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V

Tactic:
let j : S → J := fun s => (hS s.2).choose

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 ⋯
⊢ ∃ j V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
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:
intro _ _ 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: ⊢ ∀ {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:
intro _ _ 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.Topology.Category.Profinite.Extend

Goal state before:
pp: I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
C : Type u_1
inst✝ : Category.{v_1, u_1} C
G : Profinite ⥤ C
S : Profinite
x✝¹ x✝ : StructuredArrow S toProfinite
f : x✝¹ ⟶ x✝
⊢ ((const (StructuredArrow S toProfinite)).obj (G.obj S)).map f ≫ G.map x✝.hom =
    G.map x✝¹.hom ≫ (StructuredArrow.proj S toProfinite ⋙ toProfinite ⋙ G).map f

Tactic:
simp [← map_comp]

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

Goal state before:
pp: case fix.refine_2
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
x✝ : {Λ'.ret k} ⊆ S
⊢ Supports {Λ'.ret k} S

Tactic:
exact supports_singleton.2 (ret_supports <| Finset.union_subset_right H)

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Profinite
inst✝ : Finite ↑X.toTop
x✝¹ : Cofan fun x ↦ Profinite.of PUnit.{?u.15 + 1}
x✝ : (fintypeCatAsCofan X).pt ⟶ x✝¹.pt
h : ∀ (j : ↑X.toTop), (fintypeCatAsCofan X).inj j ≫ x✝ = x✝¹.inj j
⊢ x✝ = ConcreteCategory.ofHom { toFun := fun x ↦ (ConcreteCategory.hom (x✝¹.inj x)) PUnit.unit, continuous_toFun := ⋯ }

Tactic:
by ext x; exact CategoryTheory.congr_fun (h x) _

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (toProfinite.op ⋙ F).map x✝ ≫ (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop Y✝))).hom =
    (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop X✝))).hom ≫ (finYoneda F).map x✝

Tactic:
simp only [comp_obj, op_obj, finYoneda_obj, Functor.comp_map, op_map]

Goal state after:
S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ F.map (toProfinite.map x✝.unop).op ≫ (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop Y✝))).hom =
    (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop X✝))).hom ≫ (finYoneda F).map x✝
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
this : Finite ↑(fiber f x).toTop
y : ↑(fiber f x).toTop
⊢ (ConcreteCategory.hom (X.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) y).op))
      ((ConcreteCategory.hom (X.map (sigmaIncl f x).op))
        ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f)) =
    Function.Fiber.image (⇑f) x

Tactic:
simpa [← dsimp% isoFinYonedaComponents_inv_comp X _ (sigmaIncl.{u, u + 1} f x),
    ← isoFinYonedaComponents_hom_apply, -isoFinYonedaComponents_hom] using! x.map_eq_image f y

Goal state after: