awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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
⊢ ⋂ U ∈ si, (↑U : Set X) ⊆ u ∪ v
have refine_3 : Disjoint (u ∪ v)ᶜ (⋂ U ∈ si, (↑U : Set X))
Tactic: rwa [← disjoint_compl_left_iff_subset, disjoint_iff_inter_eq_empty,
        ← not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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))
⊢ ⋂ U ∈ si, (↑U : Set X) ⊆ u ∪ v
have refine_3₁ : (u ∪ v)ᶜ ∩ ⋂ U ∈ si, (↑U : Set X) = ∅
Tactic: rwa [← disjoint_compl_left_iff_subset, disjoint_iff_inter_eq_empty,
        ← not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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 : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a ∨
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a ∨
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
have H1 : IsClopen (s ∩ u)
Tactic: have H1 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hu hv huv
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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)
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a ∨
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
have H₁ : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
Tactic: rw [union_comm] at H
Cleared hypotheses: H, H1
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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)
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a ∨
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
have H2 : IsClopen (s ∩ v)
Tactic: have H2 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hv hu huv.symm
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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)
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a ∨
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
have 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
Tactic: by_cases hxu : x ∈ u
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a ∨
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
have 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
Tactic: by_cases hxu : x ∈ u
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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) ⊆ a ∨
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
have pos : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a
Tactic: left
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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) ⊆ a ∨
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
have neg : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
Tactic: right
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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)
⊢ ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a ∨
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
have pos : ∀ (hxu : x ∈ u), ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ a
Tactic: by_cases hxu : x ∈ u <;> [left; right]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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) ⊆ a ∨
    ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
have neg : ∀ (hxu : x ∉ u), ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ b
Tactic: by_cases hxu : x ∈ u <;> [left; right]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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) ⊆ a
have pos : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ u
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)
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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) ⊆ u
have apply : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ s ∩ u
Tactic: apply Subset.trans _ s.inter_subset_right
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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) ⊆ b
have h1 : 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
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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) ⊆ b
have neg : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ v
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
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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
have neg : ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X) ⊆ s ∩ v
Tactic: refine Subset.trans ?_ s.inter_subset_right
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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)
have 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)
Tactic: refine ⟨ConnectedComponents.surjective_coe.forall₂.2 fun a b ne => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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)
⊢ (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)
have ne₁ : connectedComponent a ≠ connectedComponent b
Tactic: rw [ConnectedComponents.coe_ne_coe] at ne
Cleared hypotheses: ne
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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
⊢ ∃ (u : Set (ConnectedComponents X)) (v : Set (ConnectedComponents X)),
    IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v
have h : Disjoint (connectedComponent a) (connectedComponent b)
Tactic: have h := connectedComponent_disjoint ne
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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)
⊢ ∃ (u : Set (ConnectedComponents X)) (v : Set (ConnectedComponents X)),
    IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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 : Set X) (V : Set (ConnectedComponents X)),
    IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ mk ⁻¹' V = U
have h₁ : ∃ (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
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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) = ∅
⊢ ∃ (U : Set X) (V : Set (ConnectedComponents X)),
    IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ mk ⁻¹' V = U
have 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
Tactic: obtain ⟨fin_a, ha⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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 = ∅
⊢ ∃ (U : Set X) (V : Set (ConnectedComponents X)),
    IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ mk ⁻¹' V = U
have hU : IsClopen U
Tactic: have hU : IsClopen U := isClopen_biInter_finset fun i _ => i.2.1
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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 : Set (ConnectedComponents X)) (v : Set (ConnectedComponents X)),
    IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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
⊢ ∃ (u : Set (ConnectedComponents X)) (v : Set (ConnectedComponents X)),
    IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v
have hU₁ : IsClopen V
Tactic: rw [ConnectedComponents.isQuotientMap_coe.isClopen_preimage] at hU
Cleared hypotheses: hU, ha, hb
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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
have refine : mk a ∈ Vᶜ
Tactic: refine ⟨Vᶜ, V, hU.compl.isOpen, hU.isOpen, ?_, hb mem_connectedComponent, disjoint_compl_left⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t
have mp : HasSeparatingCover s t ∧ HasSeparatingCover t s → SeparatedNhds s t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
mp : HasSeparatingCover s t ∧ HasSeparatingCover t s → SeparatedNhds s t
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t
have mpr : SeparatedNhds s t → HasSeparatingCover s t ∧ HasSeparatingCover t s
Tactic: constructor