mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsOpenEmbedding g
⊢ (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), 𝓝 (g (f x)) ≤ map g (map f (𝓝 x))

Tactic:
← hg.map_nhds_eq,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsOpenEmbedding g
⊢ (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), map g (𝓝 (f x)) ≤ map g (map f (𝓝 x))
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ L ∪ R ∈ 𝓝 b

Tactic:
rw [← nhdsWithin_univ b, h, nhdsWithin_union]
  exact ⟨mem_of_superset hL (by simp), mem_of_superset hR (by simp)⟩

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
⊢ (∃ t_1, IsOpen[inst✝¹] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t) → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
· rintro ⟨u, ou, useq⟩
        exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩

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 α
t : Set β
⊢ (∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s) → ∃ t_1, IsOpen[inst✝¹] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t

Tactic:
· rintro ⟨u, ou, useq⟩
        exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩

Goal state after:
Module: Mathlib.Topology.ContinuousOn

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

Tactic:
intro h t ht
    rcases h t ht with ⟨u, u_open, hu⟩
    rw [inter_comm, hu]
    apply IsOpen.inter u_open hs

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ Continuous[inst✝, _] f ↔ IsClopen (f ⁻¹' {b})

Tactic:
by
  rw [continuous_discrete_rng, Bool.forall_bool' b, IsClopen, ← isOpen_compl_iff, ← preimage_compl,
    Bool.compl_singleton, and_comm]

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 ⊕ Y → Z
⊢ IsOpenMap f ↔ (IsOpenMap fun a ↦ f (inl a)) ∧ IsOpenMap fun b ↦ f (inr b)

Tactic:
simp only [isOpenMap_iff_nhds_le, Sum.forall, nhds_inl, nhds_inr, Filter.map_map, comp_def]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen[t] u
⊢ u = ⋃₀ {s | s ∈ B ∧ s ⊆ u}

Tactic:
apply hB.open_eq_sUnion' ou

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen[T a] (s a)
⊢ IsOpen[Pi.topologicalSpace] (i.pi s)

Tactic:
by
  rw [pi_def]; exact hi.isOpen_biInter fun a ha => (hs _ ha).preimage (continuous_apply _)

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (n : ℕ), s n ≠ univ
n : ℕ
⊢ accumulate s n ≠ univ

Tactic:
obtain ⟨m, hm⟩ := exists_subset_accumulate_of_directed hd n

Goal state after:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (n : ℕ), s n ≠ univ
n m : ℕ
hm : accumulate s n ⊆ s m
⊢ accumulate s n ≠ univ
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
⊢ IsSeparable s ↔ SeparableSpace α

Tactic:
by
  simp_rw [IsSeparable, separableSpace_iff, dense_iff_closure_eq, ← univ_subset_iff,
    ← hs.closure_eq, isClosed_closure.closure_subset_iff]

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

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : s ∉ f
g : Filter ↑sᶜ := comap Subtype.val f
this : g.NeBot
⊢ False

Tactic:
simpa using H ((of g).map (↑)) (map_le_iff_le_comap.mpr (of_le g))

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

Goal state before:
pp: α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : f.NeBot
⊢ Filter.map m (Filter.comap m ↑g) ⊓ Filter.map m (𝓟 s) = Filter.map m (Filter.comap m ↑g) ⊓ 𝓟 (m '' s)

Tactic:
rw [map_principal]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
⊢ ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s

Tactic:
have A : ∀ u ∈ countableBasis α, ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a :=
    fun u hu ↦ ht.exists_countable_biUnion_of_isOpen ((isBasis_countableBasis α).isOpen hu)

Goal state after:
α : 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
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds
α : 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
x : α
⊢ ∀ (u : Set α), x ∈ u → IsOpen[t✝] u → ∃ v ∈ ⋃ u ∈ countableBasis α, s u, x ∈ v ∧ v ⊆ u

Tactic:
v

Goal state after:
case h_nhds
α : 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
x : α
v : Set α
⊢ x ∈ v → IsOpen[t✝] v → ∃ v_1 ∈ ⋃ u ∈ countableBasis α, s u, x ∈ v_1 ∧ v_1 ⊆ v
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
⊢ ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s

Tactic:
by
  have A : ∀ u ∈ countableBasis α, ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a :=
    fun u hu ↦ ht.exists_countable_biUnion_of_isOpen ((isBasis_countableBasis α).isOpen hu)
  choose! s hst s_count hs using A
  refine ⟨⋃ u ∈ countableBasis α, s u, by simpa using hst,
    (countable_countableBasis α).biUnion s_count, ?_⟩
  apply isTopologicalBasis_of_isOpen_of_nhds
  · simp only [mem_iUnion, exists_prop, forall_exists_index, and_imp]
    have := @ht.isOpen
    grind
  · intro x v hx hv
    simp only [mem_iUnion, exists_prop]
    obtain ⟨u, u_mem, xu, uv⟩ : ∃ u ∈ countableBasis α, x ∈ u ∧ u ⊆ v :=
      (isBasis_countableBasis α).isOpen_iff.1 hv _ hx
    have : x ∈ ⋃ a ∈ s u, a := by
      convert! xu
      exact (hs u u_mem).symm
    obtain ⟨w, ws, xw⟩ : ∃ w ∈ s u, x ∈ w := by simpa using this
    refine ⟨w, ⟨u, u_mem, ws⟩, xw, ?_⟩
    apply Subset.trans (Subset.trans _ (hs u u_mem).symm.subset) uv
    exact subset_iUnion₂_of_subset w ws (Subset.refl _)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ f u ⊆ {s | IsOpen[ts] s}

Tactic:
v

Goal state after:
case refine_2.a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
v : Set α
⊢ v ∈ f u → v ∈ {s | IsOpen[ts] s}
Module: Mathlib.Topology.Bases

Goal state before:
pp: case a.hs
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ (f u).Finite

pp: case a.h
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ ∀ i ∈ f u, IsOpen[generateFrom (⋃ u ∈ s', f u)] i

Tactic:
· apply f_fin u hu

Goal state after:
case a.h
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ ∀ i ∈ f u, IsOpen[generateFrom (⋃ u ∈ s', f u)] i
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
⊢ x ∈ K n ↔ K.find x ≤ n

Tactic:
classical
  exact ⟨fun h => Nat.find_min' (K.exists_mem x) h, fun h => K.subset h <| K.mem_find x⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
Y : Type u_2
l : Filter Y
y : X
f : Y → X
hs : IsCompact s
hmem : ∀ᶠ (x : Y) in l, f x ∈ s
h : ∀ x ∈ s, MapClusterPt x l f → x = y
⊢ Tendsto f l (𝓝 y)

Tactic:
rw [← nhdsSet_singleton]
  exact hs.tendsto_nhdsSet_of_mapClusterPt hmem h

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

Tactic:
refine (hs.elim_nhds_subcover' V V_nhds).imp fun t ht =>
    subset_trans ?_ (iUnion₂_mono fun x _ => hV x x.2)

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 : Finset ↑s
ht : s ⊆ ⋃ x ∈ t, V ↑x ⋯
⊢ s ⊆ ⋃ i ∈ t, V ↑i ⋯ ∩ s
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) = ⨆ x ∈ K, comap Function.diag (𝓝 x ×ˢ l)

Tactic:
← comap_iSup,

Goal state after:
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)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ¬(x ~ᵢ y) ↔ ∃ s, IsOpen[inst✝] s ∧ Xor (x ∈ s) (y ∈ s)

Tactic:
simp [inseparable_iff_forall_isOpen, ← xor_iff_not_iff]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ map mk (𝓝ˢ s) = 𝓝ˢ (mk '' s)

Tactic:
rw [← comap_mk_nhdsSet_image, map_comap_of_surjective surjective_mk]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
s t : Set X✝
X : Type u_3
inst✝ : Infinite X
u v : Set (CofiniteTopology X)
⊢ IsOpen u → IsOpen v → (univ ∩ u).Nonempty → (univ ∩ v).Nonempty → (univ ∩ (u ∩ v)).Nonempty

Tactic:
simp only [CofiniteTopology.isOpen_iff, univ_inter]

Goal state after:
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
s t : Set X✝
X : Type u_3
inst✝ : Infinite X
u v : Set (CofiniteTopology X)
⊢ (u.Nonempty → uᶜ.Finite) → (v.Nonempty → vᶜ.Finite) → u.Nonempty → v.Nonempty → (u ∩ v).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
u : Set X
⊢ ∀ (v : Set X), IsOpen[inst✝] u → IsOpen[inst✝] v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
v

Goal state after:
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
u v : Set X
⊢ IsOpen[inst✝] u → IsOpen[inst✝] v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsIrreducible t
f : Y → X
hf : IsOpenEmbedding f
h : (t ∩ range f).Nonempty
⊢ IsIrreducible (f ⁻¹' t)

Tactic:
by
  refine ht.preimage_of_isPreirreducible_fiber f hf.isOpenMap
    (fun _ ↦ (subsingleton_singleton.preimage hf.injective).isPreirreducible) h

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
⊢ s.Subsingleton

Tactic:
intro x hxs y hys
  obtain ⟨U, hU, hUx⟩ := isDiscrete_iff_forall_mem_exists_isOpen.mp hs x hxs
  obtain ⟨V, hV, hVy⟩ := isDiscrete_iff_forall_mem_exists_isOpen.mp hs y hys
  obtain ⟨z, hz⟩ := hs' _ _ hU hV ⟨x, by grind⟩ ⟨y, by grind⟩
  exact (hUx.le (by grind)).symm.trans (b := z) (hVy.le (by grind))

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible (f '' univ)

Tactic:
exact (PreirreducibleSpace.isPreirreducible_univ).image _ hfc.continuousOn

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : IrreducibleSpace X
⊢ IsPreirreducible (f '' univ)

Tactic:
exact (PreirreducibleSpace.isPreirreducible_univ).image _ hfc.continuousOn

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

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

Tactic:
← nhdsSet_singleton,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x : X
⊢ 𝓝ˢ {x} ≤ 𝓝ˢ s ↔ x ∈ s
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : ∀ x ∈ S, S ⊆ closure[inst✝¹] {x}
u : Set X
⊢ ∀ (v : Set X), IsOpen[inst✝¹] u → IsOpen[inst✝¹] v → (S ∩ u).Nonempty → (S ∩ v).Nonempty → (S ∩ (u ∩ v)).Nonempty

Tactic:
v

Goal state after:
case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : ∀ x ∈ S, S ⊆ closure[inst✝¹] {x}
u v : Set X
⊢ IsOpen[inst✝¹] u → IsOpen[inst✝¹] v → (S ∩ u).Nonempty → (S ∩ v).Nonempty → (S ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
s : Set α
a : α
⊢ a ∈ upperBounds (closure[inst✝²] s) ↔ a ∈ upperBounds s

Tactic:
simp_rw [mem_upperBounds_iff_subset_Iic, isClosed_Iic.closure_subset_iff]

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

Goal state before:
pp: case insert.refine_1.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X},
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ i ∈ t, IsOpen[inst✝¹] (U i)) →
          s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst✝¹] (U x) ∧ ∀ x ∈ t, IsOpen[inst✝¹] (U x)
hU' : ∀ i ∈ t, IsOpen[inst✝¹] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ ↑t, U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
hi : i ≠ x
⊢ IsCompact (update K x K₁ i)

Tactic:
simp only [update_of_ne hi, h1K]

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

Goal state before:
pp: case tail
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ j ∈ p, s j)
⊢ IsPreconnected (⋃ j ∈ insert k p, s j)

Tactic:
rw [biUnion_insert]

Goal state after:
case tail
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ j ∈ p, s j)
⊢ IsPreconnected (s k ∪ ⋃ x ∈ p, s x)
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
s : Set α
hsF : id s ⊆ F
h1s : IsOpen[inst✝¹] s
hxs : x ∈ s
h2s : IsConnected s
⊢ connectedComponentIn F x ∈ 𝓝 x

Tactic:
exact mem_nhds_iff.mpr ⟨s, h2s.isPreconnected.subset_connectedComponentIn hxs hsF, h1s, hxs⟩

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u : Set α
⊢ ∀ (v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
v

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
⊢ IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u : Set α
⊢ ∀ (v : Set α),
    IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
v

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
⊢ IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case basic
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
h : inst✝ = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t✝ t : Set X
ht : t ∈ s
ha : a ∈ t
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
| basic t ht =>

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
x✝¹ x✝ : X
h : ¬x✝¹ ⤳ x✝
⊢ Disjoint (𝓝 x✝¹) (𝓝 x✝)

Tactic:
← nhdsSet_singleton,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
x✝¹ x✝ : X
h : ¬x✝¹ ⤳ x✝
⊢ Disjoint (𝓝ˢ {x✝¹}) (𝓝 x✝)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u : Set α
⊢ ∀ (v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
v

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
⊢ IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : U ∈ 𝓝ˢ K
⊢ U ∈ (𝓝ˢ K).lift' closure[inst✝¹]

Tactic:
rcases hK.exists_isOpen_closure_subset hU with ⟨V, hVo, hKV, hVU⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : U ∈ 𝓝ˢ K
V : Set X
hVo : IsOpen[inst✝¹] V
hKV : K ⊆ V
hVU : closure[inst✝¹] V ⊆ U
⊢ U ∈ (𝓝ˢ K).lift' closure[inst✝¹]
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u : Set α
⊢ ∀ (t' : Set α),
    IsClosed[inst✝] u → IsClosed[inst✝] t' → s ⊆ u ∪ t' → (s ∩ u).Nonempty → (s ∩ t').Nonempty → (s ∩ (u ∩ t')).Nonempty

Tactic:
v

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
⊢ IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u : Set α
⊢ ∀ (v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v

Tactic:
v

Goal state after:
case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
⊢ IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u : Set α
⊢ ∀ (v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
v

Goal state after:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
⊢ IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v