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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ T0Space X ↔ Pairwise fun a b ↦ a ∉ closure[inst✝] {b} ∨ b ∉ closure[inst✝] {a}

Tactic:
by
  simp only [t0Space_iff_not_inseparable, inseparable_iff_mem_closure, not_and_or]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝 x ⊓ comap f (𝓝[s] f x) ≤ pure x
x✝ : X
⊢ x✝ ∈ f ⁻¹' s → f x✝ ∈ s

Tactic:
by exact id

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
← not_imp_not,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (x ∉ S → ¬ClusterPt x (𝓟 S)) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s z₁ z₂ : Set X
x✝¹ : IsClosed[inst✝] z₁
x✝ : IsClosed[inst✝] z₂
⊢ ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
rw [← and_imp, ← not_or, not_imp_not]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
x : X
t : Set X
H1 : IsCompact t
H2 : x ∉ t
⊢ Disjoint (𝓝ˢ t) (𝓝 x)

Tactic:
by
  simpa using SeparatedNhds.disjoint_nhdsSet <| .of_isCompact_isCompact_isClosed H1
    isCompact_singleton isClosed_singleton <| disjoint_singleton_right.mpr H2

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}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space X → Continuous[inst✝, _] ⇑CofiniteTopology.of
⊢ Continuous[inst✝, _] ⇑CofiniteTopology.of → ∀ (x : X), IsClosed[inst✝] {x}

Tactic:
intro h

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}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space X → Continuous[inst✝, _] ⇑CofiniteTopology.of
h : Continuous[inst✝, _] ⇑CofiniteTopology.of
⊢ ∀ (x : X), IsClosed[inst✝] {x}
Module: Mathlib.Topology.DiscreteSubset

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

Tactic:
intro h

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ (∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s) → s ⊆ t

Tactic:
intro h

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : ∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s
⊢ s ⊆ t
Module: Mathlib.Topology.DiscreteSubset

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

Tactic:
intro h

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

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
⊢ IsPreirreducible S → ∀ x ∈ S, S ⊆ closure[inst✝¹] {x}

Tactic:
intro h

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : IsPreirreducible S
⊢ ∀ x ∈ S, S ⊆ closure[inst✝¹] {x}
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
⊢ (∀ x ∈ S, S ⊆ closure[inst✝¹] {x}) → IsPreirreducible S

Tactic:
intro h

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}
⊢ IsPreirreducible S
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) → ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x

Tactic:
intro h

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x
⊢ ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x) → ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x

Tactic:
intro h

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
⊢ ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝¹] (U i)
hKU : closure[inst✝¹] K ⊆ ⋃ i, U i
t : Finset ι✝
ht : K ⊆ ⋃ i ∈ t, U i
⊢ ∃ t, closure[inst✝¹] K ⊆ ⋃ i ∈ t, U i

Tactic:
exact ⟨t, hK.closure_subset_of_isOpen (isOpen_biUnion fun _ _ ↦ hUo _) ht⟩

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
⊢ (𝓝 x✝).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ x✝ ∈ s ∧ IsConnected s) id →
    ∀ U ∈ 𝓝 x✝, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x✝ ∈ V ∧ IsConnected V

Tactic:
intro h

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α → ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)

Tactic:
intro h

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : LocallyConnectedSpace α
⊢ ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)) → LocallyConnectedSpace α

Tactic:
intro h

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)
⊢ LocallyConnectedSpace α
Module: Mathlib.Topology.Connected.LocallyConnected

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

Tactic:
intro h

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
⊢ IsConnected s ↔ ∃ i t, IsConnected t ∧ s = mk i '' t

Tactic:
refine ⟨fun hs => ?_, ?_⟩
  · obtain ⟨⟨i, x⟩, hx⟩ := hs.nonempty
    have : s ⊆ range (Sigma.mk i) :=
      hs.isPreconnected.subset_isClopen isClopen_range_sigmaMk ⟨⟨i, x⟩, hx, x, rfl⟩
    exact ⟨i, Sigma.mk i ⁻¹' s, hs.preimage_of_isOpenMap sigma_mk_injective isOpenMap_sigmaMk this,
      (Set.image_preimage_eq_of_subset this).symm⟩
  · rintro ⟨i, t, ht, rfl⟩
    exact ht.image _ continuous_sigmaMk.continuousOn

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

Goal state before:
pp: case refine_1.inl
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (X i)
hs : IsPreconnected ∅
⊢ ∃ i t, IsPreconnected t ∧ ∅ = mk i '' t

pp: case refine_1.inr
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsPreconnected s
h : s.Nonempty
⊢ ∃ i t, IsPreconnected t ∧ s = mk i '' t

Tactic:
· exact ⟨Classical.choice hι, ∅, isPreconnected_empty, (Set.image_empty _).symm⟩

Goal state after:
case refine_1.inr
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsPreconnected s
h : s.Nonempty
⊢ ∃ i t, IsPreconnected t ∧ s = mk i '' t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1.inl.refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ s = inl '' inl ⁻¹' s

Tactic:
exact (image_preimage_eq_of_subset h).symm

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

Goal state before:
pp: case mp
α : Type u_2
g : Set (Set α)
s : Set α
⊢ s ∈ countableGenerate g → ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s

Tactic:
intro h

Goal state after:
case mp
α : Type u_2
g : Set (Set α)
s : Set α
h : s ∈ countableGenerate g
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mpr
α : Type u_2
g : Set (Set α)
s : Set α
⊢ (∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s) → s ∈ countableGenerate g

Tactic:
intro h

Goal state after:
case mpr
α : Type u_2
g : Set (Set α)
s : Set α
h : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1.inr.refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ s = inr '' inr ⁻¹' s

Tactic:
exact (image_preimage_eq_of_subset h).symm

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

Goal state before:
pp: case mp.sInter
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : S.Countable
a✝ : ∀ s ∈ S, CountableGenerateSets g s
ih : ∀ s ∈ S, ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
⊢ ∃ S_1 ⊆ g, S_1.Countable ∧ ⋂₀ S_1 ⊆ ⋂₀ S

Tactic:
choose T Tg Tct hT using ih

Goal state after:
case mp.sInter
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : S.Countable
a✝ : ∀ s ∈ S, CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), (T s a).Countable
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ∃ S_1 ⊆ g, S_1.Countable ∧ ⋂₀ S_1 ⊆ ⋂₀ S
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mp
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ f ≤ countableGenerate g → g ⊆ f.sets

Tactic:
intro h

Goal state after:
case mp
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : f ≤ countableGenerate g
⊢ g ⊆ f.sets
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mpr
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ g ⊆ f.sets → f ≤ countableGenerate g

Tactic:
intro h

Goal state after:
case mpr
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
⊢ f ≤ countableGenerate g
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
⊢ sᶜ ∈ f

Tactic:
refine hs.compl_mem_sets fun x hx ↦ ?_
  rw [← disjoint_principal_right, disjoint_right_comm, (basis_sets _).disjoint_iff_left]
  exact hf x hx

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

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

Tactic:
intro h

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 α
⊢ (∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) → IsPreconnected s

Tactic:
intro h

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
⊢ IsPreconnected s
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
have hxv : x ∈ v := or_iff_not_imp_left.mp (hs hxs) hxu

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
hxv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1.insert.refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
x✝ :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH : (∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) → (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst✝] u ∧ ∀ x ∈ U, IsOpen[inst✝] x
hsU : s ⊆ u ∪ ⋃₀ ↑U
⊢ s ∩ (u ∩ ⋃₀ ↑U) = ∅

pp: case refine_1.insert.refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
x✝ :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH : (∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) → (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst✝] u ∧ ∀ x ∈ U, IsOpen[inst✝] x
hsU : s ⊆ u ∪ ⋃₀ ↑U
⊢ s ⊆ ⋃₀ ↑U → ∃ x ∈ U, s ⊆ x

Tactic:
· refine subset_empty_iff.1 fun x ⟨hxs, hxu, v, hvU, hxv⟩ => ?_
        exact ne_of_mem_of_not_mem hvU uU (hU.1 v hvU ⟨x, hxs, hxu, hxv⟩).symm

Goal state after:
case refine_1.insert.refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
x✝ :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH : (∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) → (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst✝] u ∧ ∀ x ∈ U, IsOpen[inst✝] x
hsU : s ⊆ u ∪ ⋃₀ ↑U
⊢ s ⊆ ⋃₀ ↑U → ∃ x ∈ U, s ⊆ x
Module: Mathlib.Topology.Connected.Clopen

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

Tactic:
intro h

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.Connected.Clopen

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

Tactic:
intro h

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
⊢ IsPreconnected s
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
have hxv : x ∈ v := or_iff_not_imp_left.mp (hs hxs) hxu

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
hxv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝²] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hL' : IsClosed[inst✝²] L
hKL : K ⊆ interior L
hLU : L ⊆ U
⊢ L ∈ 𝓝ˢ K

Tactic:
rwa [← subset_interior_iff_mem_nhdsSet]

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

Goal state before:
pp: case refine_2
α : 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
⊢ s ∩ (a ∩ b) ≠ ∅

Tactic:
intro h

Goal state after:
case refine_2
α : 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) = ∅
⊢ False
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
F : Set β
hf : ContinuousOn f (f ⁻¹' F)
y : β
x : α
hx : x ∈ f ⁻¹' connectedComponentIn F y
z : α
hz : z ∈ connectedComponentIn (f ⁻¹' F) x
⊢ f z ∈ connectedComponentIn F y

Tactic:
connectedComponentIn_eq hx

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
F : Set β
hf : ContinuousOn f (f ⁻¹' F)
y : β
x : α
hx : x ∈ f ⁻¹' connectedComponentIn F y
z : α
hz : z ∈ connectedComponentIn (f ⁻¹' F) x
⊢ f z ∈ connectedComponentIn F (f x)
Module: Mathlib.Topology.Connected.Basic

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

Tactic:
intro h

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : PreconnectedSpace α
⊢ ∀ (x : α), connectedComponent x = univ
Module: Mathlib.Topology.Connected.Basic

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

Tactic:
intro h

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y✝ : Y
hf : Tendsto f (coLindelof X) (𝓝 y✝)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y✝ (range f))
s : Set Y
hsy : s ∈ 𝓝 y✝
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
⊢ y ∈ insert y✝ (range f) → y ∈ f '' K

Tactic:
hyf

Goal state after:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y✝ : Y
hf : Tendsto f (coLindelof X) (𝓝 y✝)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y✝ (range f))
s : Set Y
hsy : s ∈ 𝓝 y✝
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsLindelof K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hyf : y ∈ insert y✝ (range f)
⊢ y ∈ f '' K
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ TotallyDisconnectedSpace α → ∀ (x : α), (connectedComponent x).Subsingleton

Tactic:
intro h

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
⊢ ∀ (x : α), (connectedComponent x).Subsingleton
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), (connectedComponent x).Subsingleton) → TotallyDisconnectedSpace α

Tactic:
intro h

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
⊢ TotallyDisconnectedSpace α
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
hs : IsOpen[inst✝¹] s
hne : s.Nonempty
⊢ ¬IsMeagre s

Tactic:
intro h

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
hs : IsOpen[inst✝¹] s
hne : s.Nonempty
h : IsMeagre s
⊢ False
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Nonempty X
s : Set X
hs : IsGδ s
hd : Dense s
⊢ ¬IsMeagre s

Tactic:
intro h

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Nonempty X
s : Set X
hs : IsGδ s
hd : Dense s
h : IsMeagre s
⊢ False
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPreconnected (⇑h ⁻¹' s) ↔ IsPreconnected s

Tactic:
rw [← image_symm, isPreconnected_image]

Goal state after: