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

Goal state before:
pp: case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
ha : a ≠ a₀
⊢ ∀ᶠ (y : α) in update pure a₀ l a, s ∈ update pure a₀ l y

Tactic:
simpa only [update_of_ne ha, mem_pure, eventually_pure] using hs

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
g : β → α
s : Set (TopologicalSpace α)
⊢ TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)

Tactic:
by
  rw [sInf_eq_iInf', sInf_image', induced_iInf]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ s = s ∩ u

Tactic:
inter_eq_left.2 hsu

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ s = s
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
hf : Surjective f
a : β
⊢ map f (𝓝 a) = 𝓝 (f a)

Tactic:
nhds_induced,

Goal state after:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
hf : Surjective f
a : β
⊢ map f (comap f (𝓝 (f a))) = 𝓝 (f a)
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
inst✝ : TopologicalSpace β
f : α → β
a : α
l : Filter α
⊢ l ≤ 𝓝 a ↔ Tendsto f l (𝓝 (f a))

Tactic:
nhds_induced,

Goal state after:
α : Type u
β : Type v
inst✝ : TopologicalSpace β
f : α → β
a : α
l : Filter α
⊢ l ≤ comap f (𝓝 (f a)) ↔ Tendsto f l (𝓝 (f a))
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
⊢ map f (𝓝 a) = 𝓝[range f] f a

Tactic:
nhds_induced,

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
⊢ map f (comap f (𝓝 (f a))) = 𝓝[range f] f a
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
h : range f ∈ 𝓝 (f a)
⊢ map f (𝓝 a) = 𝓝 (f a)

Tactic:
nhds_induced,

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
h : range f ∈ 𝓝 (f a)
⊢ map f (comap f (𝓝 (f a))) = 𝓝 (f a)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosedMap f ↔ ∀ {u : Set X}, IsOpen[inst✝¹] u → IsOpen[inst✝] (kernImage f u)

Tactic:
rw [IsClosedMap, compl_surjective.forall]

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ (x : Set X), IsClosed[inst✝¹] xᶜ → IsClosed[inst✝] (f '' xᶜ)) ↔
    ∀ {u : Set X}, IsOpen[inst✝¹] u → IsOpen[inst✝] (kernImage f u)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)) → ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})

Tactic:
exact fun H y ↦ nhdsSet_singleton (x := y) ▸ H

Goal state after:
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
hf : IsOpenEmbedding f
l : Filter Z
x : X
⊢ Tendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l

Tactic:
rw [Tendsto, ← map_map, hf.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
hf : IsOpenEmbedding f
l : Filter Z
x : X
⊢ map g (𝓝 (f x)) ≤ l ↔ Tendsto g (𝓝 (f x)) l
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
⊢ 𝓝 (x, y) ⊓ 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)

Tactic:
nhds_induced,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ comap Prod.fst (𝓝 (x, y).1) ⊓ 𝓝 (x, y) = comap Prod.fst (𝓝 x) ⊓ comap Prod.snd (𝓝 y)
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
⊢ 𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y

Tactic:
by
  rw [prod_eq_inf, instTopologicalSpaceProd, nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _)
    (t₂ := TopologicalSpace.induced Prod.snd _), nhds_induced, nhds_induced]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[≠] a ⊔ pure a = 𝓝 a

Tactic:
← nhdsWithin_singleton,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[≠] a ⊔ 𝓝[{a}] a = 𝓝 a
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hst : s =ᶠ[𝓝 x] t
h : x ∈ interior s
⊢ x ∈ interior t

Tactic:
rw [← nhdsWithin_eq_iff_eventuallyEq] at hst

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hst : 𝓝[s] x = 𝓝[t] x
h : x ∈ interior s
⊢ x ∈ interior t
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
⊢ t ⊆ closure[inst✝] (range (Subtype.val ∘ inclusion hst)) ↔ t ⊆ closure[inst✝] s

Tactic:
val_comp_inclusion,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
⊢ t ⊆ closure[inst✝] (range Subtype.val) ↔ t ⊆ closure[inst✝] s
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s : Set α
⊢ 𝓝ˢ (f '' s) ⊓ 𝓟 (range f) = 𝓝ˢ[range f] (f '' s)

Tactic:
nhdsSetWithin

Goal state after:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s : Set α
⊢ 𝓝ˢ (f '' s) ⊓ 𝓟 (range f) = 𝓝ˢ (f '' s) ⊓ 𝓟 (range f)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ IsTopologicalBasis ((fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})

Tactic:
refine ⟨?_, ?_, le_antisymm (le_generateFrom ?_) <| generateFrom_anti fun t ht => ?_⟩

Goal state after:
case refine_1
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ t₁ ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s},
    ∀ t₂ ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s},
      ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

case refine_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ⋃₀ ((fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}) = univ

case refine_3
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ s_1 ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, IsOpen[generateFrom s] s_1

case refine_4
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ t ∈ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
x : α × β
⊢ ContinuousAt f x ↔ ContinuousAt (fun x_1 ↦ f (x_1, x.2)) x.1

Tactic:
simp_rw [← continuousWithinAt_univ]; exact continuousWithinAt_prod_of_discrete_right

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
ι : 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 u, (∀ a_1 ∈ I, IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I).pi u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s

Tactic:
· rintro ⟨I, t, ⟨h1, h2⟩⟩
    classical
    refine ⟨I, fun a => ite (a ∈ I) (t a) univ, fun i => ?_, ?_⟩
    · by_cases hi : i ∈ I
      · use t i
        simp_rw [if_pos hi]
        exact ⟨Subset.rfl, (h1 i) hi⟩
      · use univ
        simp_rw [if_neg hi]
        exact ⟨Subset.rfl, isOpen_univ, mem_univ _⟩
    · rw [← univ_pi_ite]
      simp only [← ite_and, ← Finset.mem_coe, and_self_iff, univ_pi_ite, h2]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
X : Type u_9
f : X → (i : ι) → A i
⊢ induced f (⨅ i, induced (fun f ↦ f i) (T i)) = ⨅ i, induced (fun x ↦ f x i) inferInstance

Tactic:
induced_iInf,

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
X : Type u_9
f : X → (i : ι) → A i
⊢ ⨅ i, induced f (induced (fun f ↦ f i) (T i)) = ⨅ i, induced (fun x ↦ f x i) inferInstance
Module: Mathlib.Order.Filter.Ultrafilter.Basic

Goal state before:
pp: case insert
α : Type u
f : Ultrafilter α
s : Set (Set α)
a✝¹ : Set α
s✝ : Set (Set α)
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
his : ⋃₀ s✝ ∈ f ↔ ∃ t ∈ s✝, t ∈ f
⊢ ⋃₀ insert a✝¹ s✝ ∈ f ↔ ∃ t ∈ insert a✝¹ s✝, t ∈ f

Tactic:
| insert _ _ his =>

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
p : X × Y → Prop
⊢ (∀ x ∈ s, ∀ y ∈ t, ∀ᶠ (q : X × Y) in 𝓝 x ×ˢ 𝓝 y, p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ px,
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧ ∃ py, (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)

Tactic:
eventually_prod_iff

Goal state after:
Module: Mathlib.Data.Set.Functor

Goal state before:
pp: α β : Type u
s : Set α
f : α → Set β
α✝ β✝ γ✝ : Type u_1
x✝² : Set α✝
x✝¹ : α✝ → Set β✝
x✝ : β✝ → Set γ✝
⊢ x✝² >>= x✝¹ >>= x✝ = x✝² >>= fun x ↦ x✝¹ x >>= x✝

Tactic:
simp only [bind_def, biUnion_iUnion]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∈ coclosedCompact X ↔ IsCompact (closure[inst✝] s)

Tactic:
mem_coclosedCompact_iff,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact (closure[inst✝] sᶜᶜ) ↔ IsCompact (closure[inst✝] s)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case refine_1
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 ⊆ 𝔅

Tactic:
rintro _ ⟨S, hS, rfl⟩

Goal state after:
case refine_1
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
S : Set X
hS : S ∈ P
⊢ Sᶜ ∈ 𝔅
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
f : X → Y
⊢ (cocompact ℤ).NeBot

Tactic:
simp only [Filter.cocompact_eq_cofinite, Filter.cofinite_neBot]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t) → ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s

Tactic:
intro h s sS

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t
s : Set X
sS : s ⊆ S
⊢ ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s) → ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t

Tactic:
intro h s sS

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
s : Set X
sS : s ⊆ S
⊢ ∃ u, IsOpen[inst✝] u ∧ u ∩ S = s
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)
hu : u.Nonempty → uᶜ.Finite
hv : v.Nonempty → vᶜ.Finite
hu' : u.Nonempty
⊢ v.Nonempty → (u ∩ v).Nonempty

Tactic:
hv'

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)
hu : u.Nonempty → uᶜ.Finite
hv : v.Nonempty → vᶜ.Finite
hu' : u.Nonempty
hv' : 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 v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hu' : (s ∩ u).Nonempty
⊢ (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
hv'

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
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hu' : (s ∩ u).Nonempty
hv' : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
⊢ IsPreirreducible univ ↔ ∀ ⦃U : Set X⦄, IsOpen[inst✝] U → U.Nonempty → Dense U

Tactic:
isPreirreducible_iff_subset_closure_inter_open

Goal state after:
X : Type u_3
inst✝ : TopologicalSpace X
⊢ (∀ (U : Set X), IsOpen[inst✝] U → (univ ∩ U).Nonempty → univ ⊆ closure[inst✝] (univ ∩ U)) ↔
    ∀ ⦃U : Set X⦄, IsOpen[inst✝] U → U.Nonempty → Dense U
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case pos
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_mem hz,

Goal state after:
case pos
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
⊢ (insert z (U \ s ∩ t)).Finite
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
⊢ {x} ∈ 𝓝[s] x

Tactic:
by
  rw [isDiscrete_iff_discreteTopology] at hs
  have : ({⟨x, hx⟩} : Set s) ∈ 𝓝 (⟨x, hx⟩ : s) := by simp [nhds_discrete]
  simpa only [nhdsWithin_eq_map_subtype_coe hx, image_singleton] using
    @image_mem_map _ _ _ ((↑) : s → X) _ this

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : ∀ x ∈ K, ¬Inseparable x y
⊢ y ∉ closure[inst✝¹] K

Tactic:
have : Disjoint (𝓝 y) (𝓝ˢ K) := hK.disjoint_nhdsSet_right.2 fun x hx ↦
    (disjoint_nhds_nhds_iff_not_inseparable.2 (hy x hx)).symm

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : ∀ x ∈ K, ¬Inseparable x y
this : Disjoint (𝓝 y) (𝓝ˢ K)
⊢ y ∉ closure[inst✝¹] K
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
hi : s i = univ
⊢ False

Tactic:
hi,

Goal state after:
case inr
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : univ ∩ s j = ∅
hi : s i = univ
⊢ False
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
⊢ IsClosed[inst✝¹] u

Tactic:
apply isClosed_iff_nhds.2 (fun z hz ↦ ?_)

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
z : α
hz : ∀ U ∈ 𝓝 z, (U ∩ u).Nonempty
⊢ z ∈ u
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case neg
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst✝] u
h'u : (s ∩ u).Nonempty
h : closure[inst✝] u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∉ u
⊢ x ∈ u ∪ (closure[inst✝] u)ᶜ

Tactic:
right

Goal state after:
case neg
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst✝] u
h'u : (s ∩ u).Nonempty
h : closure[inst✝] u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∉ u
⊢ x ∈ (closure[inst✝] u)ᶜ
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
this :
  ∀ (a : X),
    (𝓝 a).HasBasis (fun If ↦ If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed[↑↑i] (If.snd i)) fun If ↦
      ⋂ i, If.snd i
⊢ RegularSpace X

Tactic:
refine .of_hasBasis this fun a If hIf => isClosed_iInter fun i => ?_

Goal state after:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
this :
  ∀ (a : X),
    (𝓝 a).HasBasis (fun If ↦ If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed[↑↑i] (If.snd i)) fun If ↦
      ⋂ i, If.snd i
a : X
If : (I : Set ↑T) × (↑I → Set X)
hIf : If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed[↑↑i] (If.snd i)
i : ↑If.fst
⊢ IsClosed[sInf T] (If.snd i)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
⊢ (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅) ⊆ F

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ PreconnectedSpace α → ∀ (x : α), connectedComponent x = univ

pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), connectedComponent x = univ) → PreconnectedSpace α

Tactic:
· intro h x
    exact eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), connectedComponent x = univ) → PreconnectedSpace α
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (SeparationQuotient.mk ⁻¹' closure s) (SeparationQuotient.mk ⁻¹' t)

pp: case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (SeparationQuotient.mk ⁻¹' s) (SeparationQuotient.mk ⁻¹' closure t)

Tactic:
exacts [hd₁.preimage mk, hd₂.preimage mk]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
⊢ y ∈ t → x = y

Tactic:
y_in

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
⊢ x = y
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : IsNowhereDense s
⊢ IsNowhereDense (f '' s)

Tactic:
by
  rw [isNowhereDense_iff_forall_notMem_nhds, forall_mem_image] at *
  simp_rw [hf.nhds_eq_comap, hf.closure_eq_preimage_closure_image] at h
  exact fun x x_mem hx ↦ h x x_mem (preimage_mem_comap hx)

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

Goal state before:
pp: case inr
α : 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
htv : f ⁻¹' {t'} ⊆ v
⊢ t' ∈ T₁ ∨ t' ∈ T₂

Tactic:
right

Goal state after:
case inr
α : 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₂ : Set β := ⋯
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
htv : f ⁻¹' {t'} ⊆ v
⊢ t' ∈ T₂
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b

Tactic:
have H1 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hu hv huv

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
H1 : IsClopen (s ∩ u)
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr
α : 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_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₂
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
right

Goal state after:
case inr
α : 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₂ : Set β := ⋯
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_decomp : t ⊆ T₁ ∪ T₂
T_disjoint : Disjoint T₁ T₂
h : t ⊆ T₂
⊢ f ⁻¹' t ⊆ v