mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
⊢ s ∈ 𝓝 x ×ˢ 𝓝 y ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s

Tactic:
mem_prod_iff

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
⊢ (∃ t₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 y, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
tx : Set X
ty : Set Y
⊢ s ∈ 𝓝[tx] x ×ˢ 𝓝[ty] y ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s

Tactic:
mem_prod_iff

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
tx : Set X
ty : Set Y
⊢ (∃ t₁ ∈ 𝓝[tx] x, ∃ t₂ ∈ 𝓝[ty] y, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
⊢ t ∈ 𝓝 a

Tactic:
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.mp h2 with ⟨_, Hw, hw⟩

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
w✝ : Set α
Hw : w✝ ∈ 𝓝 a
hw : w✝ ∩ s ⊆ t
⊢ t ∈ 𝓝 a
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set (X × X)
x : X
hx : s ∈ 𝓝 (x, x)
⊢ ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ U ×ˢ U ⊆ s

Tactic:
simpa [nhds_prod_eq, (nhds_basis_opens x).prod_self.mem_iff, and_assoc, and_left_comm] using hx

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen[inst✝] t
⊢ f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s

Tactic:
@inter_comm _ s (f ⁻¹' t),

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen[inst✝] t
⊢ f ⁻¹' t ∩ s = f ⁻¹' t ∩ s ∩ s
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s₁ : Set X
s₂ : Set Y
h₁ : IsClosed[inst✝¹] s₁
h₂ : IsClosed[inst✝] s₂
⊢ closure[instTopologicalSpaceProd] (s₁ ×ˢ s₂) = s₁ ×ˢ s₂

Tactic:
by simp only [h₁.closure_eq, h₂.closure_eq, closure_prod_eq]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst✝] s
x✝ : Set ↑s
⊢ IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x✝) ↔ IsOpen[instTopologicalSpaceSubtype] x✝

Tactic:
hs.isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst✝] s
x✝ : Set ↑s
⊢ IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x✝) ↔ IsOpen[inst✝] (Subtype.val '' x✝)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed[inst✝] s
h : IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t)
⊢ IsClosed[inst✝] (s ∩ t)

Tactic:
simpa using hs.isClosedMap_subtype_val _ h

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
⊢ Sum.elim f g '' range inl ⊆ C

Tactic:
image_subset_iff,

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
⊢ range inl ⊆ Sum.elim f g ⁻¹' C
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : PartialOrder α
⊢ ∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∈ s) ∧ ∀ (x : α), IsTop x → x ∈ s

Tactic:
by
  simpa using dense_univ.exists_countable_dense_subset_bot_top

Goal state after:
Module: Mathlib.Topology.Bases

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

Tactic:
choose! s hst s_count hs using A

Goal state after:
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
⊢ ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
u : Set β
hu : u ∈ lb
⊢ (∃ s ∈ la, f '' s ⊆ u) ↔ u ∈ map f la

Tactic:
simp only [image_subset_iff, exists_mem_subset_iff, mem_map]

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed[inst✝] (f i)
⊢ IsClosed[inst✝] (⋃ i, f i)

Tactic:
by
  simp only [← closure_eq_iff_isClosed, hf.closure_iUnion, (hc _).closure_eq]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hst : tᶜ ∈ f
⊢ sᶜ ∈ 𝓝 x ⊓ f

Tactic:
replace ht := mem_inf_principal.1 ht

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
t : Set X
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 x
⊢ sᶜ ∈ 𝓝 x ⊓ f
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝[s] x
⊢ ∃ t, s ⊆ ⋃ x ∈ t, U ↑x ⋯

Tactic:
choose V V_nhds hV using fun x hx => mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (hU x hx)

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝[s] x
V : (x : X) → x ∈ s → Set X
V_nhds : ∀ (x : X) (hx : x ∈ s), V x hx ∈ 𝓝 x
hV : ∀ (x : X) (hx : x ∈ s), V x hx ∩ s ⊆ U x hx
⊢ ∃ t, s ⊆ ⋃ x ∈ t, U ↑x ⋯
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
this : ∀ (f : Filter X), f ⊓ l = comap Function.diag (f ×ˢ l)
⊢ comap Function.diag (𝓝ˢ K ×ˢ l) = comap Function.diag (⨆ i ∈ K, 𝓝 i ×ˢ l)

Tactic:
hK.nhdsSet_prod_eq_biSup

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
⊢ Minimal (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) x ↔ x ∈ s

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨⟨x, h, rfl.le⟩, fun b ⟨a, has, hab⟩ hbx ↦ ?_⟩⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
h : Minimal (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) x
⊢ x ∈ s

case refine_2
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
h : x ∈ s
b : α
x✝ : (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) b
hbx : b ≤ x
a : α
has : a ∈ s
hab : a ≤ b
⊢ x ≤ b
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : Infinite X
⊢ ∃ z, (𝓝[≠] z).NeBot

Tactic:
by
  simpa [AccPt] using (@infinite_univ X _).exists_accPt_principal

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderGeneralization s → ∃ S, (∀ s ∈ S, IsOpen[inst✝] s) ∧ ⋂₀ S = s

Tactic:
rw [← stableUnderSpecialization_compl_iff, stableUnderSpecialization_iff_exists_sUnion_eq]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ s ∈ S, IsClosed[inst✝] s) ∧ ⋃₀ S = sᶜ) → ∃ S, (∀ s ∈ S, IsOpen[inst✝] s) ∧ ⋂₀ S = s
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure[inst✝²] t)
h' : ContinuousOn g (s' ∩ closure[inst✝²] tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ContinuousOn g (t.ite s s' ∩ closure[inst✝²] tᶜ)

Tactic:
· rwa [ite_inter_closure_compl_eq_of_inter_frontier_eq H]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : PreirreducibleSpace X
⊢ IsOpen[inst✝¹] s → IsOpen[inst✝¹] t → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty

Tactic:
simpa only [univ_inter, univ_subset_iff] using
    @PreirreducibleSpace.isPreirreducible_univ X _ _ s t

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
H : sᶜ ∈ Filter.coprodᵢ fun d ↦ cocompact (X d)
⊢ sᶜ ∈ cocompact ((d : ι) → X d)

Tactic:
simp only [compl_mem_coprodᵢ, Filter.mem_cocompact, compl_subset_compl, image_subset_iff] at H ⊢

Goal state after:
ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
H : ∀ (i : ι), ∃ t, IsCompact t ∧ s ⊆ eval i ⁻¹' t
⊢ ∃ t, IsCompact t ∧ s ⊆ t
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
⊢ Pairwise fun x y ↦
    ∃ u v, IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
rintro (x | x) (y | y) h

Goal state after:
case inl.inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x y : X
h : Sum.inl x ≠ Sum.inl y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inl x ∈ u ∧ Sum.inl y ∈ v ∧ Disjoint u v

case inl.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
y : Y
h : Sum.inl x ≠ Sum.inr y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inl x ∈ u ∧ Sum.inr y ∈ v ∧ Disjoint u v

case inr.inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : Y
y : X
h : Sum.inr x ≠ Sum.inl y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inr x ∈ u ∧ Sum.inl y ∈ v ∧ Disjoint u v

case inr.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x y : Y
h : Sum.inr x ≠ Sum.inr y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inr x ∈ u ∧ Sum.inr y ∈ v ∧ Disjoint u v
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∉ U \ s
⊢ (U \ s ∩ insert z t).Finite

Tactic:
inter_insert_of_notMem hz,

Goal state after:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∉ U \ s
⊢ (U \ s ∩ t).Finite
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ↔ s ⊆ t

Tactic:
refine ⟨?_, fun h => monotone_nhdsSet h⟩
  simp_rw [Filter.le_def]; intro h x hx
  specialize h {x}ᶜ
  simp_rw [compl_singleton_mem_nhdsSet_iff] at h
  by_contra hxt
  exact h hxt hx

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
t : Set X
h₁t : t ∈ 𝓝[s] p
h₂t : t.Finite
⊢ ∀ᶠ (x : X) in 𝓝[s] p, x ⤳ p

Tactic:
set S := {y ∈ t ∩ s | ¬(y ⤳ p)}

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
t : Set X
h₁t : t ∈ 𝓝[s] p
h₂t : t.Finite
S : Set X := {y | y ∈ t ∩ s ∧ ¬y ⤳ p}
⊢ ∀ᶠ (x : X) in 𝓝[s] p, x ⤳ p
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : f '' s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
⊢ s ⊆ u' ∪ v'

Tactic:
image_subset_iff,

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : s ⊆ f ⁻¹' (u ∪ v)
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
⊢ s ⊆ u' ∪ v'
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
⊢ ∃ V, IsOpen[inst✝¹] V ∧ K ⊆ V ∧ closure[inst✝¹] V ⊆ U

Tactic:
have hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ) := by
    simpa [hK.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet,
      ← subset_interior_iff_mem_nhdsSet] using! hU
  rcases ((hasBasis_nhdsSet _).disjoint_iff (hasBasis_nhdsSet _)).1 hd
    with ⟨V, ⟨hVo, hKV⟩, W, ⟨hW, hUW⟩, hVW⟩
  refine ⟨V, hVo, hKV, Subset.trans ?_ (compl_subset_comm.1 hUW)⟩
  exact closure_minimal hVW.subset_compl_right hW.isClosed_compl

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed[inst✝²] s
t_cl : IsClosed[inst✝²] t
st_dis : Disjoint s t
⊢ _root_.HasSeparatingCover s t

Tactic:
rcases isEmpty_or_nonempty X with empty_X | nonempty_X
  · rw [subset_eq_empty (t := s) (fun ⦃_⦄ _ ↦ trivial) (univ_eq_empty_iff.mpr empty_X)]
    exact hasSeparatingCovers_iff_separatedNhds.mpr (SeparatedNhds.empty_left t) |>.1
  -- This is almost `HasSeparatingCover`, but is not countable. We define for all `a : X` for use
  -- with `IsLindelof.indexed_countable_subcover` momentarily.
  have (a : X) : ∃ n : Set X, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n) := by
    wlog ains : a ∈ s
    · exact ⟨∅, isOpen_empty, SeparatedNhds.empty_left t |>.disjoint_closure_left, fun a ↦ ains a⟩
    obtain ⟨n, nna, ncl, nsubkc⟩ := ((regularSpace_TFAE X).out 0 3 :).mp ‹RegularSpace X› a tᶜ <|
      t_cl.compl_mem_nhds (disjoint_left.mp st_dis ains)
    exact
      ⟨interior n,
       isOpen_interior,
       disjoint_left.mpr fun ⦃_⦄ ain ↦
         nsubkc <| (IsClosed.closure_subset_iff ncl).mpr interior_subset ain,
       fun _ ↦ mem_interior_iff_mem_nhds.mpr nna⟩
  -- By Lindelöf, we may obtain a countable subcover witnessing `HasSeparatingCover`
  choose u u_open u_dis u_nhds using this
  obtain ⟨f, f_cov⟩ := s_cl.isLindelof.indexed_countable_subcover
    u u_open (fun a ainh ↦ mem_iUnion.mpr ⟨a, u_nhds a ainh⟩)
  exact ⟨u ∘ f, f_cov, fun n ↦ ⟨u_open (f n), u_dis (f n)⟩⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
t : Set ↑s
ht : t.Countable
h : s ⊆ ⋃ i ∈ t, U i
uinf : ⋃ i ∈ t, U i ∈ f.sets
uninf : (⋃ i ∈ t, U i)ᶜ ∈ f
⊢ False

Tactic:
have uninf := compl_notMem uninf

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
t : Set ↑s
ht : t.Countable
h : s ⊆ ⋃ i ∈ t, U i
uinf : ⋃ i ∈ t, U i ∈ f.sets
uninf✝ : (⋃ i ∈ t, U i)ᶜ ∈ f
uninf : (⋃ i ∈ t, U i)ᶜᶜ ∉ f
⊢ False
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∉ F
⊢ ∅ ⊆ connectedComponentIn G x

Tactic:
exact Set.empty_subset _

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

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ e '' t ⊆ (closure[inst✝¹] (e '' s))ᶜ

Tactic:
image_subset_iff,

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ t ⊆ e ⁻¹' (closure[inst✝¹] (e '' s))ᶜ
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ Disjoint (s ∩ a) (s ∩ b)

Tactic:
by grind [Set.disjoint_iff_inter_eq_empty]

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

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ e '' s ⊆ (closure[inst✝¹] (e '' t))ᶜ

Tactic:
image_subset_iff,

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ s ⊆ e ⁻¹' (closure[inst✝¹] (e '' t))ᶜ
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
⊢ u = ⋃ x ∈ u, connectedComponentIn v x

Tactic:
by
  have := congr(((↑) : Set v → Set X) $(hu.biUnion_connectedComponent_eq.symm))
  simp only [Subtype.image_preimage_coe, mem_preimage, iUnion_coe_set, image_val_iUnion,
    inter_eq_right.mpr huv₁] at this
  nth_rw 1 [this]
  congr! 2 with x hx
  simp only [← connectedComponentIn_eq_image]
  exact le_antisymm (iUnion_subset fun _ ↦ le_rfl) <|
    iUnion_subset fun hx ↦ subset_iUnion₂_of_subset (huv₁ hx) hx le_rfl

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map (i ∘ f) (comap g (𝓝 d)) ≤ map h (𝓝 d)
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)

Tactic:
← Filter.map_map,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map i (map f (comap g (𝓝 d))) ≤ map h (𝓝 d)
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : (𝓝 x).HasBasis p s
f : α → β
hf : IsDenseInducing f
⊢ (𝓝 (f x)).HasBasis p fun i ↦ closure[inst✝¹] (f '' s i)

Tactic:
Filter.hasBasis_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
⊢ ∀ (t : Set β), t ∈ 𝓝 (f x) ↔ ∃ i, p i ∧ closure[inst✝¹] (f '' s i) ⊆ t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
htu : f ⁻¹' {t'} ⊆ u
⊢ t' ∈ T₁ ∨ t' ∈ T₂

Tactic:
left; exact ⟨ht', htu⟩

Goal state after: