awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
hs : IsClosed[inst] (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X))
a b : Set X
ha : IsClosed[inst] a
hb : IsClosed[inst] b
hab : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ 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 ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
neg : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a ∨
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b

Tactic:
right
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
hs : IsClosed[inst] (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X))
a b : Set X
ha : IsClosed[inst] a
hb : IsClosed[inst] b
hab : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ 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 ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
pos : ∀ (hxu : x ∈ u), ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a
neg : ∀ (hxu : x ∉ u), ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a ∨
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b

Tactic:
by_cases hxu : x ∈ u <;> [left; right]
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
hs : IsClosed[inst] (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X))
a b : Set X
ha : IsClosed[inst] a
hb : IsClosed[inst] b
hab : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ 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 ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∈ u
pos : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ u
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a

Tactic:
suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ u
        from Disjoint.left_le_of_le_sup_right hab (huv.mono this hbv)
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
hs : IsClosed[inst] (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X))
a b : Set X
ha : IsClosed[inst] a
hb : IsClosed[inst] b
hab : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ 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 ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∈ u
apply : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ s ∩ u
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ u

Tactic:
apply Subset.trans _ s.inter_subset_right

Premises used: Set.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
hs : IsClosed[inst] (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X))
a b : Set X
ha : IsClosed[inst] a
hb : IsClosed[inst] b
hab : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ 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 ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∈ u
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ s ∩ u

Tactic:
iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ u, H1, mem_inter H.2.1 hxu⟩

Premises used: Subtype.mk, Inter.inter, Set.mem_inter, And.right, And.left, And.intro, Set.iInter_subset, Subtype.val
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
hs : IsClosed[inst] (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X))
a b : Set X
ha : IsClosed[inst] a
hb : IsClosed[inst] b
hab : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ 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 ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∈ u
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ s ∩ u

Tactic:
exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ u, H1, mem_inter H.2.1 hxu⟩

Premises used: Subtype.mk, Inter.inter, Set.mem_inter, And.right, And.left, And.intro, Set.iInter_subset, Subtype.val
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
hs : IsClosed[inst] (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X))
a b : Set X
ha : IsClosed[inst] a
hb : IsClosed[inst] b
hab : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ 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 ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
⊢ x ∈ v

Tactic:
have h1 : x ∈ v :=
        (hab.trans (union_subset_union hau hbv) (mem_iInter.2 fun i => i.2.2)).resolve_left hxu
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
hs : IsClosed[inst] (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X))
a b : Set X
ha : IsClosed[inst] a
hb : IsClosed[inst] b
hab : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ 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 ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
h1 : x ∈ v
neg : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ v
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b

Tactic:
suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ v
        from (huv.symm.mono this hau).left_le_of_le_sup_left hab
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
hs : IsClosed[inst] (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X))
a b : Set X
ha : IsClosed[inst] a
hb : IsClosed[inst] b
hab : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ 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 ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
h1 : x ∈ v
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ v

Tactic:
Subset.trans ?_ s.inter_subset_right

Premises used: Set.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
hs : IsClosed[inst] (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X))
a b : Set X
ha : IsClosed[inst] a
hb : IsClosed[inst] b
hab : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ 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 ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
h1 : x ∈ v
neg : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ s ∩ v
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ v

Tactic:
refine Subset.trans ?_ s.inter_subset_right

Premises used: Set.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
hs : IsClosed[inst] (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X))
a b : Set X
ha : IsClosed[inst] a
hb : IsClosed[inst] b
hab : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ 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 ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
h1 : x ∈ v
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ s ∩ v

Tactic:
iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ v, H2, mem_inter H.2.1 h1⟩

Premises used: Subtype.mk, Inter.inter, Set.mem_inter, And.right, And.left, And.intro, Set.iInter_subset, Subtype.val
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
hs : IsClosed[inst] (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X))
a b : Set X
ha : IsClosed[inst] a
hb : IsClosed[inst] b
hab : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ 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 ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
h1 : x ∈ v
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ s ∩ v

Tactic:
exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ v, H2, mem_inter H.2.1 h1⟩

Premises used: Subtype.mk, Inter.inter, Set.mem_inter, And.right, And.left, And.intro, Set.iInter_subset, Subtype.val
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
⊢ T2Space.{u_1} (ConnectedComponents X)

Tactic:
⟨ConnectedComponents.surjective_coe.forall₂.2 fun a b ne => ?_⟩

Premises used: Iff.mpr, ConnectedComponents.surjective_coe, T2Space.mk, Function.Surjective.forall₂
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
refine :
  ∀ (a b : X) (ne : Ne (α := ConnectedComponents X) (mk a) (mk b)),
    (fun (x y : ConnectedComponents X) ↦
        ∃ (u : Set (ConnectedComponents X)) (v : Set (ConnectedComponents X)),
          IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v)
      (mk a) (mk b)
⊢ T2Space.{u_1} (ConnectedComponents X)

Tactic:
refine ⟨ConnectedComponents.surjective_coe.forall₂.2 fun a b ne => ?_⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : Ne (α := ConnectedComponents X) (mk a) (mk b)
⊢ connectedComponent a ≠ connectedComponent b

Tactic:
rw [ConnectedComponents.coe_ne_coe] at ne

Premises used: ConnectedComponents.coe_ne_coe
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
⊢ Disjoint (connectedComponent a) (connectedComponent b)

Tactic:
have h := connectedComponent_disjoint ne
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : Disjoint (connectedComponent a) (connectedComponent b)
⊢ connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅

Tactic:
rw [connectedComponent_eq_iInter_isClopen b, disjoint_iff_inter_eq_empty] at h

Premises used: Set.disjoint_iff_inter_eq_empty, connectedComponent_eq_iInter_isClopen
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
⊢ ∃ (u : Finset { s : Set X // IsClopen s ∧ b ∈ s }), connectedComponent a ∩ ⋂ i ∈ u, (↑i : Set X) = ∅

Tactic:
have h :=
      (isClosed_connectedComponent (α := X)).isCompact.elim_finite_subfamily_closed
        _ (fun s : { s : Set X // IsClopen s ∧ b ∈ s } => s.2.1.1) h
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h_1 : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
h : ∃ (u : Finset { s : Set X // IsClopen s ∧ b ∈ s }), connectedComponent a ∩ ⋂ i ∈ u, (↑i : Set X) = ∅
obtain :
  ∀ (fin_a : Finset { s : Set X // IsClopen s ∧ b ∈ s }) (ha : connectedComponent a ∩ ⋂ i ∈ fin_a, (↑i : Set X) = ∅),
    ∃ (U : Set X) (V : Set (ConnectedComponents X)),
      IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ mk ⁻¹' V = U
⊢ ∃ (U : Set X) (V : Set (ConnectedComponents X)),
    IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ mk ⁻¹' V = U

Tactic:
obtain ⟨fin_a, ha⟩ := h
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
fin_a : Finset { s : Set X // IsClopen s ∧ b ∈ s }
ha : connectedComponent a ∩ ⋂ i ∈ fin_a, (↑i : Set X) = ∅
⊢ let U : Set X := ⋂ i ∈ fin_a, (↑i : Set X);
  connectedComponent a ∩ U = ∅

Tactic:
set U : Set X := ⋂ (i : { s // IsClopen s ∧ b ∈ s }) (_ : i ∈ fin_a), i

Premises used: Set
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
fin_a : Finset { s : Set X // IsClopen s ∧ b ∈ s }
U : Set X := ⋂ i ∈ fin_a, (↑i : Set X)
ha : connectedComponent a ∩ U = ∅
⊢ IsClopen U

Tactic:
have hU : IsClopen U := isClopen_biInter_finset fun i _ => i.2.1
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
fin_a : Finset { s : Set X // IsClopen s ∧ b ∈ s }
U : Set X := ⋂ i ∈ fin_a, (↑i : Set X)
ha : connectedComponent a ∩ U = ∅
hU : IsClopen U
⊢ ∃ (U : Set X) (V : Set (ConnectedComponents X)),
    IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ mk ⁻¹' V = U

Tactic:
⟨U, (↑) '' U, hU, ha, subset_iInter₂ fun s _ => s.2.1.connectedComponent_subset s.2.2,
      (connectedComponents_preimage_image U).symm ▸ hU.biUnion_connectedComponent_eq⟩

Premises used: Set.subset_iInter₂, IsClopen.connectedComponent_subset, And.right, And.left, And.intro, Exists.intro, Set.image, Subtype.property
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
fin_a : Finset { s : Set X // IsClopen s ∧ b ∈ s }
U : Set X := ⋂ i ∈ fin_a, (↑i : Set X)
ha : connectedComponent a ∩ U = ∅
hU : IsClopen U
⊢ ∃ (U : Set X) (V : Set (ConnectedComponents X)),
    IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ mk ⁻¹' V = U

Tactic:
exact ⟨U, (↑) '' U, hU, ha, subset_iInter₂ fun s _ => s.2.1.connectedComponent_subset s.2.2,
      (connectedComponents_preimage_image U).symm ▸ hU.biUnion_connectedComponent_eq⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
obtain :
  ∀ (V : Set (ConnectedComponents X)) (hU : IsClopen (mk ⁻¹' V)) (ha : connectedComponent a ∩ mk ⁻¹' V = ∅)
    (hb : connectedComponent b ⊆ mk ⁻¹' V),
    ∃ (u : Set (ConnectedComponents X)) (v : Set (ConnectedComponents X)),
      IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v
⊢ ∃ (u : Set (ConnectedComponents X)) (v : Set (ConnectedComponents X)),
    IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v

Tactic:
obtain ⟨U, V, hU, ha, hb, rfl⟩ : ∃ (U : Set X) (V : Set (ConnectedComponents X)),
      IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ (↑) ⁻¹' V = U := by
    have h :=
      (isClosed_connectedComponent (α := X)).isCompact.elim_finite_subfamily_closed
        _ (fun s : { s : Set X // IsClopen s ∧ b ∈ s } => s.2.1.1) h
    obtain ⟨fin_a, ha⟩ := h
    -- This clopen and its complement will separate the connected components of `a` and `b`
    set U : Set X := ⋂ (i : { s // IsClopen s ∧ b ∈ s }) (_ : i ∈ fin_a), i
    have hU : IsClopen U := isClopen_biInter_finset fun i _ => i.2.1
    exact ⟨U, (↑) '' U, hU, ha, subset_iInter₂ fun s _ => s.2.1.connectedComponent_subset s.2.2,
      (connectedComponents_preimage_image U).symm ▸ hU.biUnion_connectedComponent_eq⟩

Premises used: connectedComponent, ConnectedComponents, rfl, Set
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
V : Set (ConnectedComponents X)
hU : IsClopen (mk ⁻¹' V)
ha : connectedComponent a ∩ mk ⁻¹' V = ∅
hb : connectedComponent b ⊆ mk ⁻¹' V
⊢ IsClopen V

Tactic:
rw [ConnectedComponents.isQuotientMap_coe.isClopen_preimage] at hU

Premises used: Topology.IsQuotientMap.isClopen_preimage, ConnectedComponents.isQuotientMap_coe
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
V : Set (ConnectedComponents X)
hU : IsClopen (mk ⁻¹' V)
ha : connectedComponent a ∩ mk ⁻¹' V = ∅
hb : connectedComponent b ⊆ mk ⁻¹' V
hU₁ : IsClopen V
⊢ connectedComponent a ∩ mk ⁻¹' V = ∅

Tactic:
rw [ConnectedComponents.isQuotientMap_coe.isClopen_preimage] at hU

Premises used: Topology.IsQuotientMap.isClopen_preimage, ConnectedComponents.isQuotientMap_coe
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
V : Set (ConnectedComponents X)
hU : IsClopen (mk ⁻¹' V)
ha : connectedComponent a ∩ mk ⁻¹' V = ∅
hb : connectedComponent b ⊆ mk ⁻¹' V
hU₁ : IsClopen V
ha₁ : connectedComponent a ∩ mk ⁻¹' V = ∅
⊢ connectedComponent b ⊆ mk ⁻¹' V

Tactic:
rw [ConnectedComponents.isQuotientMap_coe.isClopen_preimage] at hU

Premises used: Topology.IsQuotientMap.isClopen_preimage, ConnectedComponents.isQuotientMap_coe
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
V : Set (ConnectedComponents X)
hU : IsClopen V
ha : connectedComponent a ∩ mk ⁻¹' V = ∅
hb : connectedComponent b ⊆ mk ⁻¹' V
⊢ ∃ (u : Set (ConnectedComponents X)) (v : Set (ConnectedComponents X)),
    IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v

Tactic:
⟨Vᶜ, V, hU.compl.isOpen, hU.isOpen, ?_, hb mem_connectedComponent, disjoint_compl_left⟩

Premises used: Compl.compl, mem_connectedComponent, IsClopen.compl, disjoint_compl_left, IsClopen.isOpen, And.intro, Exists.intro
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
V : Set (ConnectedComponents X)
hU : IsClopen V
ha : connectedComponent a ∩ mk ⁻¹' V = ∅
hb : connectedComponent b ⊆ mk ⁻¹' V
refine : mk a ∈ Vᶜ
⊢ ∃ (u : Set (ConnectedComponents X)) (v : Set (ConnectedComponents X)),
    IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v

Tactic:
refine ⟨Vᶜ, V, hU.compl.isOpen, hU.isOpen, ?_, hb mem_connectedComponent, disjoint_compl_left⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
V : Set (ConnectedComponents X)
hU : IsClopen V
ha : connectedComponent a ∩ mk ⁻¹' V = ∅
hb : connectedComponent b ⊆ mk ⁻¹' V
⊢ mk a ∈ Vᶜ

Tactic:
fun h => flip Set.Nonempty.ne_empty ha ⟨a, mem_connectedComponent, h⟩

Premises used: Set.Mem, Set.Nonempty.ne_empty, mem_connectedComponent, setOf, flip, And.intro, Exists.intro, Not
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ (s : { s : Set X // IsClopen s ∧ b ∈ s }), (↑s : Set X) = ∅
V : Set (ConnectedComponents X)
hU : IsClopen V
ha : connectedComponent a ∩ mk ⁻¹' V = ∅
hb : connectedComponent b ⊆ mk ⁻¹' V
⊢ mk a ∈ Vᶜ

Tactic:
exact fun h => flip Set.Nonempty.ne_empty ha ⟨a, mem_connectedComponent, h⟩

Premises used: Set.Nonempty.ne_empty, mem_connectedComponent, flip, And.intro, Exists.intro
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
⊢ SeparatedNhds s t ↔ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
simp only [(hasBasis_nhdsSet s).disjoint_iff (hasBasis_nhdsSet t), SeparatedNhds, ←
    exists_and_left, and_assoc, and_comm, and_left_comm]

Premises used: hasBasis_nhdsSet, exists_and_left, and_left_comm, and_comm, Filter.HasBasis.disjoint_iff, and_assoc, SeparatedNhds
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
mp : HasSeparatingCover s t ∧ HasSeparatingCover t s → SeparatedNhds s t
mpr : SeparatedNhds s t → HasSeparatingCover s t ∧ HasSeparatingCover t s
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
⊢ ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))

Tactic:
have open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ n, IsOpen (u₀ n)) →
      IsOpen (⋃ n, u₀ n \ closure (a n)) := fun _ _ u₀i_open ↦
        isOpen_iUnion fun i ↦ (u₀i_open i).sdiff isClosed_closure