mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : x ∈ (fun n ↦ u n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v m)) n
m : ℕ
xinvm : x ∈ v m
n_le_m : n ≤ m
⊢ x ∈ closure[inst✝] (⋃ m' ∈ {m' | m' ≤ m}, u m')

Tactic:
exact subset_closure (mem_biUnion n_le_m xinun.1)

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝 x = pure x

Tactic:
simp only [discreteTopology_iff_singleton_mem_nhds]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), {x} ∈ 𝓝 x) ↔ ∀ (x : α), 𝓝 x = pure x
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ h.symm.trans h = Homeomorph.refl Y

Tactic:
ext
  apply apply_symm_apply

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case a
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := ⋯
⊢ 𝓝 a ≤ pure a ⊔ f

Tactic:
rintro t ⟨hat : a ∈ t, htf : t ∈ f⟩
    exact IsOpen.mem_nhds (fun _ ↦ htf) hat

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z✝ : Type u_4
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen[inst✝²] (⇑e ⁻¹' s) ↔ IsOpen[inst✝¹] s
s : Set X
⊢ IsOpen[inst✝²] s → IsOpen[inst✝¹] (e.invFun ⁻¹' s)

Tactic:
by simpa using (he (e.symm ⁻¹' s)).1

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
y : β
s t : Set β
h : ContinuousWithinAt f (f ⁻¹' s) x
ht : t ∈ 𝓝[s] y
hxy : y = f x
⊢ f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x

Tactic:
rw [hxy] at ht
  exact h.preimage_mem_nhdsWithin' (nhdsWithin_mono _ (image_preimage_subset f s) ht)

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: case h₀
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f g : α → β
t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto f (𝓝[s] a ⊓ 𝓟 t) l

Tactic:
← nhdsWithin_inter'

Goal state after:
case h₀
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f g : α → β
t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto f (𝓝[s ∩ t] a) l
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f g : α → β
t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto g (𝓝[s] a ⊓ 𝓟 tᶜ) l

Tactic:
← nhdsWithin_inter'

Goal state after:
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f g : α → β
t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto g (𝓝[s ∩ tᶜ] a) l
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set X
x : ↑S
⊢ (𝓝[≠] x).NeBot ↔ (𝓝[≠] ↑x ⊓ 𝓟 S).NeBot

Tactic:
by
  rw [neBot_iff, neBot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
u : Set Y
hu : IsOpen[inst✝] u
⊢ IsOpen[instTopologicalSpaceSum] (inr '' u)

Tactic:
by
  simpa [isOpen_sum_iff, preimage_image_eq u Sum.inr_injective]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
B B' : Set (Set α)
hB : IsTopologicalBasis B
h_open : ∀ u ∈ B', IsOpen[t] u
h : ∀ u ∈ B, ∀ x ∈ u, ∃ v ∈ B', x ∈ v ∧ v ⊆ u
x : α
u : Set α
hx : x ∈ u
hu : IsOpen[t] u
w : Set α
hwB : w ∈ B
hxw : x ∈ w
hwu : w ⊆ u
v : Set α
hvB' : v ∈ B'
hxv : x ∈ v
hvw : v ⊆ w
⊢ ∃ v ∈ B', x ∈ v ∧ v ⊆ u

Tactic:
exact ⟨v, hvB', hxv, hvw.trans hwu⟩

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : LE α
x : α
z : β
⊢ z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y

Tactic:
by
  simp_rw [accumulate_def, mem_iUnion₂, exists_prop]

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
hx : x ∈ accumulate s i
⊢ x ∉ s j

Tactic:
simp only [accumulate, mem_iUnion, exists_prop] at hx

Goal state after:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
hx : ∃ i_1 ≤ i, x ∈ s i_1
⊢ x ∉ s j
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
⊢ (∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s) →
    ∃ I u, (∀ a_2 ∈ I, IsOpen[T a_2] (u a_2) ∧ a a_2 ∈ u a_2) ∧ (↑I).pi u ⊆ s

Tactic:
rintro ⟨I, t, ⟨h1, h2⟩⟩
    refine ⟨I, fun a => eval a '' (I : Set ι).pi fun a => (h1 a).choose, fun i hi => ?_, ?_⟩
    · simp_rw [eval_image_pi (Finset.mem_coe.mpr hi)
          (pi_nonempty_iff.mpr fun i => ⟨_, fun _ => (h1 i).choose_spec.2.2⟩)]
      exact (h1 i).choose_spec.2
    · exact Subset.trans
        (pi_mono fun i hi => (eval_image_pi_subset hi).trans (h1 i).choose_spec.1) h2

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Filter α
h₁ : f.NeBot
h₂ : ∀ (g : Filter α), g.NeBot → g ≤ f → f ≤ g
g : Filter α
neBot'✝ : g.NeBot
le_of_le✝ : ∀ (g_1 : Filter α), g_1.NeBot → g_1 ≤ g → g ≤ g_1
x✝ : ↑{ toFilter := f, neBot' := h₁, le_of_le := h₂ } = ↑{ toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }
⊢ { toFilter := f, neBot' := h₁, le_of_le := h₂ } = { toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }

Tactic:
by congr

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) ⋯
⊢ range id ∈ f

Tactic:
range_id

Goal state after:
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) ⋯
⊢ univ ∈ f
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
n : Type u_9
m : Type u_10
f : m → n
hf : Surjective f
⊢ IsEmbedding fun x ↦ x ∘ f

Tactic:
refine ⟨isInducing_iff_nhds.mpr fun x ↦ ?_, hf.injective_comp_right⟩
  simp only [nhds_pi, Filter.pi, Filter.comap_iInf, ← hf.iInf_congr, Filter.comap_comap,
    Function.comp_def]

Goal state after:
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι✝ : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
ι : Type u_4
inst✝² : Finite ι
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (X i)
f : (i : ι) → X i
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 f

Tactic:
by
    choose s hsc hs using fun i ↦ exists_compact_mem_nhds (f i)
    exact ⟨pi univ s, isCompact_univ_pi hsc, set_pi_mem_nhds univ.toFinite fun i _ ↦ hs i⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a

Tactic:
by
  have A : ∀ x ∈ u, ∃ a ∈ t, x ∈ a ∧ a ⊆ u :=
    fun x hx ↦ ht.exists_subset_of_mem_open hx hu
  choose! a hat xa au using A
  obtain ⟨T, T_count, hT⟩ : ∃ T : Set u, T.Countable ∧ ⋃ i ∈ T, a i = ⋃ (i : u), a i := by
    apply isOpen_iUnion_countable _
    rintro ⟨x, hx⟩
    exact ht.isOpen (hat x hx)
  refine ⟨(fun (x : u) ↦ a x) '' T, ?_, T_count.image _, ?_⟩
  · simp only [image_subset_iff]
    rintro ⟨x, xu⟩ -
    exact hat x xu
  rw [biUnion_image, hT]
  apply Subset.antisymm
  · intro x hx
    simp
    grind
  · simp
    grind

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
l l' : Filter α
p : α → Prop
⊢ (∃ s ∈ l, ∃ t ∈ l', ∀ x ∈ t, x ∈ s → p x) ↔ ∀ᶠ (x : α) in l ⊓ l', p x

Tactic:
by simp only [eventually_inf, and_comm, mem_inter_iff, ← and_imp]

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | ((fun n ↦ {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite
N : X → ℕ
hN : ∀ (x : X), ∀ n > N x, ∀ y ∈ U x, f (n + 1) y = f n y
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2

Tactic:
replace hN : ∀ (x), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y :=
    fun x n hn y hy => Nat.le_induction rfl (fun k hle => (hN x _ hle _ hy).trans) n hn

Goal state after:
X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | ((fun n ↦ {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite
N : X → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ IsTopologicalBasis ((fun u ↦ Sum.inl '' u) '' s ∪ (fun u ↦ Sum.inr '' u) '' t)

Tactic:
by
  apply isTopologicalBasis_of_isOpen_of_nhds
  · rintro u (⟨w, hw, rfl⟩ | ⟨w, hw, rfl⟩)
    · exact IsOpenEmbedding.inl.isOpenMap w (hs.isOpen hw)
    · exact IsOpenEmbedding.inr.isOpenMap w (ht.isOpen hw)
  · rintro (x | x) u hxu u_open
    · obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ s, x ∈ v ∧ v ⊆ Sum.inl ⁻¹' u :=
        hs.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).1
      exact ⟨Sum.inl '' v, mem_union_left _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
        image_subset_iff.2 vu⟩
    · obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ t, x ∈ v ∧ v ⊆ Sum.inr ⁻¹' u :=
        ht.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).2
      exact ⟨Sum.inr '' v, mem_union_right _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
        image_subset_iff.2 vu⟩

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → (⋃₀ Q)ᶜ.Nonempty
⊢ (⋃₀ P)ᶜ.Nonempty

Tactic:
Set.compl_sUnion

Goal state after:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → (⋂₀ (compl '' Q)).Nonempty
⊢ (⋂₀ (compl '' P)).Nonempty
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f g : X → Y
l : Filter X
y : Y
h : Tendsto g l (𝓝 y)
hl : ∀ (x : X), f x ⤳ g x
⊢ Tendsto f l (𝓝 y)

Tactic:
simp_all only [specializes_iff_forall_open, tendsto_nhds]
  refine fun s ho hy => mem_of_superset (h s ho hy) fun x hx => ?_
  exact mem_preimage.2 (hl x s ho (mem_preimage.1 hx))

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
K : Set Y
Kf : K ⊆ range f
⊢ IsCompact (f ⁻¹' K) ↔ IsCompact K

Tactic:
rw [hf.isCompact_iff, image_preimage_eq_of_subset Kf]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ SpecializingMap f ↔ ∀ (x : X), StableUnderSpecialization (f '' closure[inst✝¹] {x})

Tactic:
by
  simpa only [closure_singleton_eq_Iic] using! Relation.fibration_iff_isLowerSet_image_Iic

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ cocompact (X × Y) ≤ (cocompact X).coprod (cocompact Y)

Tactic:
refine (hasBasis_cocompact.coprod hasBasis_cocompact).ge_iff.2 fun K hK ↦ ?_

Goal state after:
case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X × Set Y
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ Prod.fst ⁻¹' K.1ᶜ ∪ Prod.snd ⁻¹' K.2ᶜ ∈ cocompact (X × Y)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (SeparationQuotient X × SeparationQuotient Y)
⊢ (∀ x ∈ s, ContinuousWithinAt (uncurry (lift₂ f hf)) s x) ↔
    ∀ x ∈ Prod.map mk mk ⁻¹' s, ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) x

Tactic:
(surjective_mk.prodMap surjective_mk).forall,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (SeparationQuotient X × SeparationQuotient Y)
⊢ (∀ (x : X × Y), Prod.map mk mk x ∈ s → ContinuousWithinAt (uncurry (lift₂ f hf)) s (Prod.map mk mk x)) ↔
    ∀ x ∈ Prod.map mk mk ⁻¹' s, ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case h.refine_3.htd
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
U : Set X
hU : U ∈ c
U' : Set X
hU' : U' ∈ c
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ (↑i)ᶜ) ⟨U, hU⟩) ((fun i ↦ (↑i)ᶜ) z) ∧
      (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ (↑i)ᶜ) ⟨U', hU'⟩) ((fun i ↦ (↑i)ᶜ) z)

Tactic:
obtain ⟨V, hVc, hVU, hVU'⟩ := hz.directedOn U hU U' hU'

Goal state after:
case h.refine_3.htd
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
U : Set X
hU : U ∈ c
U' : Set X
hU' : U' ∈ c
V : Set X
hVc : V ∈ c
hVU : U ⊆ V
hVU' : U' ⊆ V
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ (↑i)ᶜ) ⟨U, hU⟩) ((fun i ↦ (↑i)ᶜ) z) ∧
      (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ (↑i)ᶜ) ⟨U', hU'⟩) ((fun i ↦ (↑i)ᶜ) z)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_1.insert
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
a✝ : u ∉ U
IH : (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
hu : ∀ u_1 ∈ insert u U, IsOpen[inst✝] u_1
hU : ∀ u_1 ∈ insert u U, (s ∩ u_1).Nonempty
⊢ (s ∩ (u ∩ ⋂₀ ↑U)).Nonempty

Tactic:
rw [Finset.forall_mem_insert] at hu hU

Goal state after:
case refine_1.insert
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
a✝ : u ∉ U
IH : (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
hu : IsOpen[inst✝] u ∧ ∀ x ∈ U, IsOpen[inst✝] x
hU : (s ∩ u).Nonempty ∧ ∀ x ∈ U, (s ∩ x).Nonempty
⊢ (s ∩ (u ∩ ⋂₀ ↑U)).Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
⊢ IsPreirreducible s

Tactic:
(Tactic.tacticSeq
 (Tactic.tacticSeq1Indented
  [(Tactic.intro "intro" [`u `v `hu `hv `hu' `hv'])
   []
   (Tactic.simpa
    "simpa"
    []
    []
    (Tactic.simpaArgsRest
     (Tactic.optConfig [])
     []
     []
     [(Tactic.simpArgs "[" [(Tactic.simpStar "*")] "]")]
     ["using"
      (Term.app
       `h
       [(choice
         («term{_}» "{" [`u "," `v] "}")
         (Term.structInst
          "{"
          []
          (Term.structInstFields
           [(Term.structInstField (Term.structInstLVal `u []) [])
            ","
            (Term.structInstField (Term.structInstLVal `v []) [])])
          (Term.optEllipsis [])
          []
          "}"))])]))]))

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
⊢ [T1Space X, ∀ (x : X), IsClosed[inst✝] {x}, ∀ (x : X), IsOpen[inst✝] {x}ᶜ, Continuous[inst✝, _] ⇑CofiniteTopology.of,
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE

Tactic:
tfae_have 5 ↔ 3 := by
    refine forall_comm.trans ?_
    simp only [isOpen_iff_mem_nhds, mem_compl_iff, mem_singleton_iff]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
⊢ [T1Space X, ∀ (x : X), IsClosed[inst✝] {x}, ∀ (x : X), IsOpen[inst✝] {x}ᶜ, Continuous[inst✝, _] ⇑CofiniteTopology.of,
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Y → X
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst✝¹] s
⊢ (s ∩ range f).Nonempty

Tactic:
exact Set.nonempty_of_nonempty_preimage (f := f) (by simpa)

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

Goal state before:
pp: case inl
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
ι : Type u_4
X : ι → Type u_3
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (a : ι), T2Space (X a)
i : ι
x y : X i
ne : ⟨i, x⟩ ≠ ⟨i, y⟩
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSigma] u ∧ IsOpen[instTopologicalSpaceSigma] v ∧ ⟨i, x⟩ ∈ u ∧ ⟨i, y⟩ ∈ v ∧ Disjoint u v

Tactic:
replace ne : x ≠ y := ne_of_apply_ne _ ne
    exact separated_by_isOpenEmbedding .sigmaMk ne

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Finset X
⊢ Dense (s \ ↑t)

Tactic:
induction t using Finset.induction_on with

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
hd : Disjoint (𝓝 a) atBot
hbot : IsBot a
⊢ False

Tactic:
hbot.atBot_eq,

Goal state after:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
hd : Disjoint (𝓝 a) (𝓟 (Iic a))
hbot : IsBot a
⊢ False
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
a : α
inst✝ : PredOrder α
h : ¬IsMin a
⊢ 𝓝[<] a = ⊥

Tactic:
else

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
a : α
inst✝ : PredOrder α
h : ¬IsMin a
⊢ 𝓝[<] a = ⊥
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
x : α
⊢ Ioi x = ⋃ y ∈ s ∩ Ioi x, Ioi y

Tactic:
by
  refine Subset.antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun y hy ↦ Ioi_subset_Ioi (le_of_lt hy.2))
  rcases hs.exists_between hz with ⟨y, hys, hy⟩
  exact mem_iUnion₂.2 ⟨y, ⟨hys, hy.1⟩, hy.2⟩

Goal state after:
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V
x : α
U : Set α
⊢ U ∈ 𝓝 x → ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
hxU

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V
x : α
U : Set α
hxU : U ∈ 𝓝 x
⊢ ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case refine_1.inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
x : (i : ι) → X i
this : ∀ (i : ι), Nonempty (X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htV : J.pi t ⊆ connectedComponent x
⊢ {i | ¬PreconnectedSpace (X i)}.Finite

Tactic:
refine hJ.subset fun i hi ↦ by_contra fun hiJ ↦ hi ?_

Goal state after:
case refine_1.inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
x : (i : ι) → X i
this : ∀ (i : ι), Nonempty (X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htV : J.pi t ⊆ connectedComponent x
i : ι
hi : i ∈ {i | ¬PreconnectedSpace (X i)}
hiJ : i ∉ J
⊢ PreconnectedSpace (X i)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inl
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hsu : s ∩ u = ∅
⊢ s ⊆ u ∨ s ⊆ v

pp: case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hsu : (s ∩ u).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
· exact Or.inr ((Set.disjoint_iff_inter_eq_empty.2 hsu).subset_right_of_subset_union hsuv)

Goal state after:
case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hsu : (s ∩ u).Nonempty
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
l : Filter X
inst✝ : CountableInterFilter l
hs : IsLindelof s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
⊢ Disjoint (𝓝ˢ s) l

Tactic:
choose! U hxU hUl using fun x hx ↦ (nhds_basis_opens x).disjoint_iff_left.1 (H x hx)

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
l : Filter X
inst✝ : CountableInterFilter l
hs : IsLindelof s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hxU : ∀ x ∈ s, x ∈ U x ∧ IsOpen[inst✝¹] (U x)
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
⊢ Disjoint (𝓝ˢ s) l