awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompletelyNormalSpace X
inst_2 : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
a : Disjoint (closure[inst] (SeparationQuotient.mk ⁻¹' s)) (SeparationQuotient.mk ⁻¹' t)
a₁ : Disjoint (SeparationQuotient.mk ⁻¹' s) (closure[inst] (SeparationQuotient.mk ⁻¹' t))
⊢ Disjoint (𝓝ˢ (SeparationQuotient.mk ⁻¹' s)) (𝓝ˢ (SeparationQuotient.mk ⁻¹' t))

Tactic:
apply completely_normal

Premises used: CompletelyNormalSpace.completely_normal
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompletelyNormalSpace X
inst_2 : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
a : Disjoint (SeparationQuotient.mk ⁻¹' closure s) (SeparationQuotient.mk ⁻¹' t)
⊢ Disjoint (closure[inst] (SeparationQuotient.mk ⁻¹' s)) (SeparationQuotient.mk ⁻¹' t)

Tactic:
rw [← preimage_mk_closure]

Premises used: SeparationQuotient.preimage_mk_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompletelyNormalSpace X
inst_2 : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
a : Disjoint (SeparationQuotient.mk ⁻¹' s) (SeparationQuotient.mk ⁻¹' closure t)
⊢ Disjoint (SeparationQuotient.mk ⁻¹' s) (closure[inst] (SeparationQuotient.mk ⁻¹' t))

Tactic:
rw [← preimage_mk_closure]

Premises used: SeparationQuotient.preimage_mk_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompletelyNormalSpace X
inst_2 : 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)

Tactic:
hd₁.preimage mk

Premises used: SeparationQuotient.mk, Disjoint.preimage
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompletelyNormalSpace X
inst_2 : 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:
hd₂.preimage mk

Premises used: SeparationQuotient.mk, Disjoint.preimage
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompletelyNormalSpace X
inst_2 : 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)

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

Premises used: SeparationQuotient.mk, Disjoint.preimage
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
apply : ⋂ (Z : { Z : Set X // IsClopen Z ∧ x ∈ Z }), (↑Z : Set X) ⊆ connectedComponent x
⊢ connectedComponent x = ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)

Tactic:
apply Subset.antisymm connectedComponent_subset_iInter_isClopen

Premises used: Set.Subset.antisymm, connectedComponent_subset_iInter_isClopen
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
⊢ ⋂ (Z : { Z : Set X // IsClopen Z ∧ x ∈ Z }), (↑Z : Set X) ⊆ connectedComponent x

Tactic:
IsPreconnected.subset_connectedComponent ?_ (mem_iInter.2 fun s => s.2.2)

Premises used: Iff.mpr, Set.mem_iInter, And.right, Subtype.property, IsPreconnected.subset_connectedComponent
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
refine : IsPreconnected.{u_1} (α := X) (⋂ (Z : { Z : Set X // IsClopen Z ∧ x ∈ Z }), (↑Z : Set X))
⊢ ⋂ (Z : { Z : Set X // IsClopen Z ∧ x ∈ Z }), (↑Z : Set X) ⊆ connectedComponent x

Tactic:
refine IsPreconnected.subset_connectedComponent ?_ (mem_iInter.2 fun s => s.2.2)

Premises used: Iff.mpr, Set.mem_iInter, IsPreconnected.subset_connectedComponent
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
⊢ IsClosed[inst] (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X))

Tactic:
have hs : @IsClosed X _ (⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, s) :=
    isClosed_iInter fun s => s.2.1.1
-- 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))
rw :
  ∀ (u v : Set X),
    IsClosed[inst] u →
      IsClosed[inst] v →
        ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ u ∪ v →
          Disjoint u v →
            ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ u ∨
              ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ v
⊢ IsPreconnected.{u_1} (α := X) (⋂ (Z : { Z : Set X // IsClopen Z ∧ x ∈ Z }), (↑Z : Set X))

Tactic:
rw [isPreconnected_iff_subset_of_fully_disjoint_closed hs]

Premises used: isPreconnected_iff_subset_of_fully_disjoint_closed
-- 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
rcases :
  ∀ (u v : Set X) (hu : IsOpen[inst] u) (hv : IsOpen[inst] v) (hau : a ⊆ u) (hbv : b ⊆ v) (huv : Disjoint u v),
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a ∨
      ⋂ (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:
rcases normal_separation ha hb ab_disj with ⟨u, v, hu, hv, hau, hbv, huv⟩

Premises used: normal_separation
-- 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
⊢ ∀
    (hst :
      ∀ (u_1 : Finset { s : Set X // IsClopen s ∧ x ∈ s }),
        ((u ∪ v)ᶜ ∩ ⋂ i ∈ u_1, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty),
    ((u ∪ v)ᶜ ∩
        ⋂ (i : { s : Set X // IsClopen s ∧ x ∈ s }),
          (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty

Tactic:
have H1 := (hu.union hv).isClosed_compl.isCompact.inter_iInter_nonempty
      (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s) fun s => s.2.1.1
-- 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
H1 :
  ∀
    (hst :
      ∀ (u_1 : Finset { s : Set X // IsClopen s ∧ x ∈ s }),
        ((u ∪ v)ᶜ ∩ ⋂ i ∈ u_1, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty),
    ((u ∪ v)ᶜ ∩
        ⋂ (i : { s : Set X // IsClopen s ∧ x ∈ s }),
          (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
⊢ Disjoint (u ∪ v)ᶜ
      (⋂ (i : { s : Set X // IsClopen s ∧ x ∈ s }), (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i) →
    ∃ (x_1 : Finset { s : Set X // IsClopen s ∧ x ∈ s }),
      ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty

Tactic:
rw [← not_disjoint_iff_nonempty_inter, imp_not_comm, not_forall] at H1

Premises used: Set.not_disjoint_iff_nonempty_inter, imp_not_comm, Classical.not_forall
-- 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
H1 :
  Disjoint (u ∪ v)ᶜ
      (⋂ (i : { s : Set X // IsClopen s ∧ x ∈ s }), (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i) →
    ∃ (x_1 : Finset { s : Set X // IsClopen s ∧ x ∈ s }),
      ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
obtain :
  ∀ (si : Finset { s : Set X // IsClopen s ∧ x ∈ s })
    (H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty),
    ∃ (s : Set X), IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
⊢ ∃ (s : Set X), IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Tactic:
obtain ⟨si, H2⟩ :=
      H1 (disjoint_compl_left_iff_subset.2 <| hab.trans <| union_subset_union hau hbv)

Premises used: Iff.mpr, Set.disjoint_compl_left_iff_subset, Set.union_subset_union, HasSubset.Subset.trans
-- 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
H1 :
  Disjoint (u ∪ v)ᶜ
      (⋂ (i : { s : Set X // IsClopen s ∧ x ∈ s }), (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i) →
    ∃ (x_1 : Finset { s : Set X // IsClopen s ∧ x ∈ s }),
      ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
si : Finset { s : Set X // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
⊢ ∃ (s : Set X), IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Tactic:
⟨⋂ U ∈ si, Subtype.val U, ?_, ?_, ?_⟩

Premises used: Set.iInter, And.intro, Exists.intro, 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
H1 :
  Disjoint (u ∪ v)ᶜ
      (⋂ (i : { s : Set X // IsClopen s ∧ x ∈ s }), (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i) →
    ∃ (x_1 : Finset { s : Set X // IsClopen s ∧ x ∈ s }),
      ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
si : Finset { s : Set X // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
refine_1 : IsClopen.{u_1} (X := X) (⋂ U ∈ si, (↑U : Set X))
refine_2 : Membership.mem (γ := Set X) (⋂ U ∈ si, (↑U : Set X)) x
refine_3 : ⋂ U ∈ si, (↑U : Set X) ⊆ u ∪ v
⊢ ∃ (s : Set X), IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Tactic:
refine ⟨⋂ U ∈ si, Subtype.val U, ?_, ?_, ?_⟩
-- 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
H1 :
  Disjoint (u ∪ v)ᶜ
      (⋂ (i : { s : Set X // IsClopen s ∧ x ∈ s }), (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i) →
    ∃ (x_1 : Finset { s : Set X // IsClopen s ∧ x ∈ s }),
      ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
si : Finset { s : Set X // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
⊢ IsClopen.{u_1} (X := X) (⋂ U ∈ si, (↑U : Set X))

Tactic:
isClopen_biInter_finset fun s _ => s.2.1

Premises used: And.left, isClopen_biInter_finset, Subtype.property
-- 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
H1 :
  Disjoint (u ∪ v)ᶜ
      (⋂ (i : { s : Set X // IsClopen s ∧ x ∈ s }), (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i) →
    ∃ (x_1 : Finset { s : Set X // IsClopen s ∧ x ∈ s }),
      ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
si : Finset { s : Set X // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
⊢ IsClopen.{u_1} (X := X) (⋂ U ∈ si, (↑U : Set X))

Tactic:
exact isClopen_biInter_finset fun s _ => s.2.1

Premises used: isClopen_biInter_finset
-- 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
H1 :
  Disjoint (u ∪ v)ᶜ
      (⋂ (i : { s : Set X // IsClopen s ∧ x ∈ s }), (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i) →
    ∃ (x_1 : Finset { s : Set X // IsClopen s ∧ x ∈ s }),
      ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
si : Finset { s : Set X // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
⊢ Membership.mem (γ := Set X) (⋂ U ∈ si, (↑U : Set X)) x

Tactic:
mem_iInter₂.2 fun s _ => s.2.2

Premises used: Iff.mpr, Set.mem_iInter₂, And.right, Subtype.property
-- 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
H1 :
  Disjoint (u ∪ v)ᶜ
      (⋂ (i : { s : Set X // IsClopen s ∧ x ∈ s }), (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i) →
    ∃ (x_1 : Finset { s : Set X // IsClopen s ∧ x ∈ s }),
      ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
si : Finset { s : Set X // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
⊢ Membership.mem (γ := Set X) (⋂ U ∈ si, (↑U : Set X)) x

Tactic:
exact mem_iInter₂.2 fun s _ => s.2.2

Premises used: Iff.mpr, Set.mem_iInter₂
-- 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
H1 :
  Disjoint (u ∪ v)ᶜ
      (⋂ (i : { s : Set X // IsClopen s ∧ x ∈ s }), (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i) →
    ∃ (x_1 : Finset { s : Set X // IsClopen s ∧ x ∈ s }),
      ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
si : Finset { s : Set X // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, (fun (s : { s : Set X // IsClopen s ∧ x ∈ s }) ↦ (↑s : Set X)) i).Nonempty
refine_3 : Disjoint (u ∪ v)ᶜ (⋂ U ∈ si, (↑U : Set X))
refine_3₁ : (u ∪ v)ᶜ ∩ ⋂ U ∈ si, (↑U : Set X) = ∅
refine_3₂ refine_3₃ refine_3₄ refine_3₅ : ¬((u ∪ v)ᶜ ∩ ⋂ U ∈ si, (↑U : Set X)).Nonempty
⊢ ⋂ U ∈ si, (↑U : Set X) ⊆ u ∪ v

Tactic:
rwa [← disjoint_compl_left_iff_subset, disjoint_iff_inter_eq_empty,
        ← not_nonempty_iff_eq_empty]

Premises used: Set.disjoint_compl_left_iff_subset, Set.not_nonempty_iff_eq_empty, Set.disjoint_iff_inter_eq_empty
-- 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
obtain :
  ∀ (s : Set X) (H : IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v),
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a ∨
      ⋂ (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:
obtain ⟨s, H⟩ : ∃ s : Set X, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v := by
    /- Now we find a clopen set `s` around `x`, contained in `u ∪ v`. We utilize the fact that
    `X \ u ∪ v` will be compact, so there must be some finite intersection of clopen neighbourhoods
    of `X` disjoint to it, but a finite intersection of clopen sets is clopen,
    so we let this be our `s`. -/
    have H1 := (hu.union hv).isClosed_compl.isCompact.inter_iInter_nonempty
      (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s) fun s => s.2.1.1
    rw [← not_disjoint_iff_nonempty_inter, imp_not_comm, not_forall] at H1
    obtain ⟨si, H2⟩ :=
      H1 (disjoint_compl_left_iff_subset.2 <| hab.trans <| union_subset_union hau hbv)
    refine ⟨⋂ U ∈ si, Subtype.val U, ?_, ?_, ?_⟩
    · exact isClopen_biInter_finset fun s _ => s.2.1
    · exact mem_iInter₂.2 fun s _ => s.2.2
    · rwa [← disjoint_compl_left_iff_subset, disjoint_iff_inter_eq_empty,
        ← not_nonempty_iff_eq_empty]

Premises used: Set
-- 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 ⊆ u ∪ v
⊢ IsClopen (s ∩ u)

Tactic:
have H1 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hu hv huv
-- 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 ⊆ u ∪ v
H1 : IsClopen (s ∩ u)
⊢ IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u

Tactic:
rw [union_comm] at H

Premises used: Set.union_comm
-- 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 ⊆ u ∪ v
H1 : IsClopen (s ∩ u)
H₁ : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
⊢ IsClopen (s ∩ u)

Tactic:
rw [union_comm] at H

Premises used: Set.union_comm
-- 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)
⊢ IsClopen (s ∩ v)

Tactic:
have H2 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hv hu huv.symm
-- 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 ∨
      ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
neg :
  ∀ (hxu : x ∉ u),
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a ∨
      ⋂ (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
-- 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) ⊆ a
⊢ ⋂ (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:
left