awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
hst :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
U V : Set { x : X // x ∈ e }
hU : IsOpen[instTopologicalSpaceSubtype] U
hV : IsOpen[instTopologicalSpaceSubtype] V
hsU : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s ⊆ U
htV : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V
hUV : Disjoint U V
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have hU₁ : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = U
Tactic: rw [Topology.IsInducing.subtypeVal.isOpen_iff] at hU hV
Cleared hypotheses: hU, hV, hsU, htV, hUV
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
hst :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
U V : Set { x : X // x ∈ e }
hU : IsOpen[instTopologicalSpaceSubtype] U
hV : IsOpen[instTopologicalSpaceSubtype] V
hsU : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s ⊆ U
htV : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V
hUV : Disjoint U V
hU₁ : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = U
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have hV₁ : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = V
Tactic: rw [Topology.IsInducing.subtypeVal.isOpen_iff] at hU hV
Cleared hypotheses: hU, hV, hsU, htV, hUV
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
hst :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
U V : Set { x : X // x ∈ e }
hU : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = U
hV : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = V
hsU : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s ⊆ U
htV : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V
hUV : Disjoint U V
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have obtain : ∀ (U : Set X) (hU : IsOpen[inst] U)
  (hsU :
    Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
      (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U))
  (hUV : Disjoint (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U) V), Disjoint (𝓝ˢ s) (𝓝ˢ t)
Tactic: obtain ⟨U, hU, rfl⟩ := hU
Cleared hypotheses: U, hU, hsU, hUV
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
hst :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
V : Set { x : X // x ∈ e }
hV : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = V
htV : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V
U : Set X
hU : IsOpen[inst] U
hsU :
  Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
hUV : Disjoint (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U) V
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have obtain : ∀ (V : Set X) (hV : IsOpen[inst] V)
  (htV :
    Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
      (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V))
  (hUV :
    Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
      (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)),
  Disjoint (𝓝ˢ s) (𝓝ˢ t)
Tactic: obtain ⟨V, hV, rfl⟩ := hV
Cleared hypotheses: V, hV, htV, hUV
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
hst :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
U : Set X
hU : IsOpen[inst] U
hsU :
  Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
V : Set X
hV : IsOpen[inst] V
htV :
  Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have rw : SeparatedNhds s t
Tactic: rw [← separatedNhds_iff_disjoint]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
hst :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
U : Set X
hU : IsOpen[inst] U
hsU :
  Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
V : Set X
hV : IsOpen[inst] V
htV :
  Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
⊢ SeparatedNhds s t
have rw : ∀ (hsU : closure[inst] s ∩ e ⊆ U ∩ e) (V : Set X) (hV : IsOpen[inst] V) (htV : closure[inst] t ∩ e ⊆ V ∩ e)
  (hUV :
    Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
      (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)),
  SeparatedNhds s t
Tactic: rw [Subtype.preimage_val_subset_preimage_val_iff, inter_comm e, inter_comm e] at hsU htV
Cleared hypotheses: hsU, V, hV, htV, hUV
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
hst :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
U : Set X
hU : IsOpen[inst] U
hsU : closure[inst] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst] V
htV : closure[inst] t ∩ e ⊆ V ∩ e
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
⊢ SeparatedNhds s t
have refine_1 : s ⊆ U ∩ e
Tactic: refine ⟨U ∩ e, V ∩ e, hU.inter he, hV.inter he, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
hst :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
U : Set X
hU : IsOpen[inst] U
hsU : closure[inst] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst] V
htV : closure[inst] t ∩ e ⊆ V ∩ e
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
refine_1 : s ⊆ U ∩ e
⊢ SeparatedNhds s t
have refine_2 : t ⊆ V ∩ e
Tactic: refine ⟨U ∩ e, V ∩ e, hU.inter he, hV.inter he, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
hst :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
U : Set X
hU : IsOpen[inst] U
hsU : closure[inst] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst] V
htV : closure[inst] t ∩ e ⊆ V ∩ e
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
refine_1 : s ⊆ U ∩ e
refine_2 : t ⊆ V ∩ e
⊢ SeparatedNhds s t
have refine_3 : Disjoint (U ∩ e) (V ∩ e)
Tactic: refine ⟨U ∩ e, V ∩ e, hU.inter he, hV.inter he, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
hst :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
U : Set X
hU : IsOpen[inst] U
hsU : closure[inst] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst] V
htV : closure[inst] t ∩ e ⊆ V ∩ e
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
⊢ Disjoint (U ∩ e) (V ∩ e)
have refine_3 : ∀
  (hUV :
    ∀ ⦃a : { x : X // x ∈ e }⦄,
      Membership.mem (γ := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U) a →
        a ∉ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
  ⦃a : X⦄, a ∈ U ∩ e → a ∉ V ∩ e
Tactic: rw [disjoint_left] at hUV ⊢
Cleared hypotheses: hUV
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T5Space Y
e : X → Y
he : IsEmbedding e
⊢ ∀ ⦃s t : Set X⦄, Disjoint (closure[inst] s) t → Disjoint s (closure[inst] t) → Disjoint (𝓝ˢ s) (𝓝ˢ t)
have this : CompletelyNormalSpace X
Tactic: have := he.completelyNormalSpace
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompletelyNormalSpace X
inst_2 : R0Space X
⊢ ∀ (x : SeparationQuotient X), IsClosed (X := SeparationQuotient X) {x}
have rwa : T1Space.{u_1} (SeparationQuotient X)
Tactic: rwa [((t1Space_TFAE (SeparationQuotient X)).out 1 0 :), SeparationQuotient.t1Space_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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 (𝓝ˢ s) (𝓝ˢ t)
have rw : Disjoint (𝓝ˢ (SeparationQuotient.mk ⁻¹' s)) (𝓝ˢ (SeparationQuotient.mk ⁻¹' t))
Tactic: rw [← disjoint_comap_iff surjective_mk, comap_mk_nhdsSet, comap_mk_nhdsSet]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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 ⁻¹' t))
have a : Disjoint (closure[inst] (SeparationQuotient.mk ⁻¹' s)) (SeparationQuotient.mk ⁻¹' t)
Tactic: apply completely_normal
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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)
⊢ Disjoint (𝓝ˢ (SeparationQuotient.mk ⁻¹' s)) (𝓝ˢ (SeparationQuotient.mk ⁻¹' t))
have a₁ : Disjoint (SeparationQuotient.mk ⁻¹' s) (closure[inst] (SeparationQuotient.mk ⁻¹' t))
Tactic: apply completely_normal
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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 (closure[inst] (SeparationQuotient.mk ⁻¹' s)) (SeparationQuotient.mk ⁻¹' t)
have a : Disjoint (SeparationQuotient.mk ⁻¹' closure s) (SeparationQuotient.mk ⁻¹' t)
Tactic: rw [← preimage_mk_closure]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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) (closure[inst] (SeparationQuotient.mk ⁻¹' t))
have a : Disjoint (SeparationQuotient.mk ⁻¹' s) (SeparationQuotient.mk ⁻¹' closure t)
Tactic: rw [← preimage_mk_closure]
-- 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
⊢ connectedComponent x = ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)
have apply : ⋂ (Z : { Z : Set X // IsClopen Z ∧ x ∈ Z }), (↑Z : Set X) ⊆ connectedComponent x
Tactic: apply Subset.antisymm connectedComponent_subset_iInter_isClopen
-- 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
⊢ ⋂ (Z : { Z : Set X // IsClopen Z ∧ x ∈ Z }), (↑Z : Set X) ⊆ connectedComponent x
have refine : IsPreconnected.{u_1} (α := X) (⋂ (Z : { Z : Set X // IsClopen Z ∧ x ∈ Z }), (↑Z : Set X))
Tactic: refine IsPreconnected.subset_connectedComponent ?_ (mem_iInter.2 fun s => s.2.2)
-- 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
⊢ IsPreconnected.{u_1} (α := X) (⋂ (Z : { Z : Set X // IsClopen Z ∧ x ∈ Z }), (↑Z : Set X))
have hs : 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
-- 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))
⊢ IsPreconnected.{u_1} (α := X) (⋂ (Z : { Z : Set X // IsClopen Z ∧ x ∈ Z }), (↑Z : Set X))
have 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
Tactic: rw [isPreconnected_iff_subset_of_fully_disjoint_closed hs]
-- 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
⊢ ⋂ (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 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
Tactic: rcases normal_separation ha hb ab_disj with ⟨u, v, hu, hv, hau, hbv, 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), IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
have 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
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
-- 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
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
⊢ ∃ (s : Set X), IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
have 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
Tactic: rw [← not_disjoint_iff_nonempty_inter, imp_not_comm, not_forall] at H1
Cleared hypotheses: H1
-- 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
⊢ ∃ (s : Set X), IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
have 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
Tactic: obtain ⟨si, H2⟩ :=
      H1 (disjoint_compl_left_iff_subset.2 <| hab.trans <| union_subset_union hau 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
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
have refine_1 : IsClopen.{u_1} (X := X) (⋂ U ∈ si, (↑U : Set X))
Tactic: refine ⟨⋂ U ∈ si, Subtype.val 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
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))
⊢ ∃ (s : Set X), IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
have refine_2 : Membership.mem (γ := Set X) (⋂ U ∈ si, (↑U : Set X)) x
Tactic: refine ⟨⋂ U ∈ si, Subtype.val 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
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
⊢ ∃ (s : Set X), IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
have refine_3 : ⋂ U ∈ si, (↑U : Set X) ⊆ u ∪ v
Tactic: refine ⟨⋂ U ∈ si, Subtype.val U, ?_, ?_, ?_⟩