awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : ℝ
h : ∀ (i : ℕ), Membership.mem (γ := Set ℝ) (range (ι := X) (⇑f : (a : X) → ℝ)) x ∧ x < 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ x ≤ 0

Tactic:
exact ge_of_tendsto' tendsto_one_div_add_atTop_nhds_zero_nat (fun n => (h n).2.le)

Premises used: tendsto_one_div_add_atTop_nhds_zero_nat, LT.lt.le, ge_of_tendsto', And.right
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : ℝ
h :
  Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) x
neg :
  ∀ (x : X)
    (h :
      Membership.mem (α := ℝ) (γ := Set ℝ)
        (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1))
        ((f : (a : X) → ℝ) x : ℝ)),
    LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ 0 ≤ x

Tactic:
rcases (mem_iInter.1 h 0).1 with ⟨x, rfl⟩

Premises used: Set.mem_iInter, And.left, Iff.mp, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
h :
  Membership.mem (α := ℝ) (γ := Set ℝ)
    (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) ((f : (a : X) → ℝ) x : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
(hfr x).1

Premises used: And.left
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
inst : TopologicalSpace X
h_1 :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
s : Set X
hs : IsClosed[inst] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0}
hfr : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
h :
  Membership.mem (α := ℝ) (γ := Set ℝ)
    (⋂ (i : ℕ), range (ι := X) (⇑f : (a : X) → ℝ) ∩ Iio (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) ((f : (a : X) → ℝ) x : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
exact (hfr x).1

Premises used: And.left
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X → Y
he : IsEmbedding e
inst_2 : PerfectlyNormalSpace Y
rw :
  ∀ (s : Set X),
    IsClosed[inst] s →
      ∃ (f : C(X, ℝ)),
        s = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ PerfectlyNormalSpace X

Tactic:
rw [perfectlyNormalSpace_iff_forall_isClosed_preimage_zero]

Premises used: perfectlyNormalSpace_iff_forall_isClosed_preimage_zero
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X → Y
he : IsEmbedding e
inst_2 : PerfectlyNormalSpace Y
t : Set X
ht : IsClosed[inst] t
⊢ ∃ (c : Set Y), IsClosed[inst_1] c ∧ e '' t = c ∩ range e

Tactic:
he.image_eq_isClosed_inter_range ht

Premises used: Topology.IsEmbedding.toIsInducing, Topology.IsInducing.image_eq_isClosed_inter_range
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X → Y
he : IsEmbedding e
inst_2 : PerfectlyNormalSpace Y
t : Set X
ht : IsClosed[inst] t
obtain :
  ∀ (c : Set Y) (hc : IsClosed[inst_1] c ∧ e '' t = c ∩ range e),
    ∃ (f : C(X, ℝ)),
      t = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    t = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
obtain ⟨c, hc⟩ : ∃ c, IsClosed c ∧ e '' t = c ∩ range e := he.image_eq_isClosed_inter_range ht

Premises used: Topology.IsEmbedding.toIsInducing, Set.range, Topology.IsInducing.image_eq_isClosed_inter_range
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X → Y
he : IsEmbedding e
inst_2 : PerfectlyNormalSpace Y
t : Set X
ht : IsClosed[inst] t
c : Set Y
hc : IsClosed[inst_1] c ∧ e '' t = c ∩ range e
obtain :
  ∀ (f : C(Y, ℝ)) (hf : ∀ (x : Y), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : Y) → ℝ) x : ℝ))
    (hc :
      IsClosed[inst_1] (preimage (β := ℝ) (⇑f : (a : Y) → ℝ) {0}) ∧
        e '' t = preimage (β := ℝ) (⇑f : (a : Y) → ℝ) {0} ∩ range e),
    ∃ (f : C(X, ℝ)),
      t = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    t = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
obtain ⟨f, rfl, hf⟩ :=
    perfectlyNormalSpace_iff_forall_isClosed_preimage_zero.1 inferInstance c hc.1

Premises used: perfectlyNormalSpace_iff_forall_isClosed_preimage_zero, inferInstance, And.left, Iff.mp, rfl
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X → Y
he : IsEmbedding e
inst_2 : PerfectlyNormalSpace Y
t : Set X
ht : IsClosed[inst] t
f : C(Y, ℝ)
hf : ∀ (x : Y), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : Y) → ℝ) x : ℝ)
hc :
  IsClosed[inst_1] (preimage (β := ℝ) (⇑f : (a : Y) → ℝ) {0}) ∧
    e '' t = preimage (β := ℝ) (⇑f : (a : Y) → ℝ) {0} ∩ range e
⊢ ∃ (f : C(X, ℝ)),
    t = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
⟨⟨f ∘ e, f.continuous.comp he.continuous⟩, ?_, fun x => hf (e x)⟩

Premises used: ContinuousMap.continuous, ContinuousMap.mk, Continuous.comp, Function.comp, And.intro, Exists.intro, DFunLike.coe, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X → Y
he : IsEmbedding e
inst_2 : PerfectlyNormalSpace Y
t : Set X
ht : IsClosed[inst] t
f : C(Y, ℝ)
hf : ∀ (x : Y), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : Y) → ℝ) x : ℝ)
hc :
  IsClosed[inst_1] (preimage (β := ℝ) (⇑f : (a : Y) → ℝ) {0}) ∧
    e '' t = preimage (β := ℝ) (⇑f : (a : Y) → ℝ) {0} ∩ range e
refine : t = preimage (β := ℝ) (⇑{ toFun := (⇑f : (a : Y) → ℝ) ∘ e, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) {0}
⊢ ∃ (f : C(X, ℝ)),
    t = preimage (β := ℝ) (⇑f : (a : X) → ℝ) {0} ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
refine ⟨⟨f ∘ e, f.continuous.comp he.continuous⟩, ?_, fun x => hf (e x)⟩
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X → Y
he : IsEmbedding e
inst_2 : PerfectlyNormalSpace Y
t : Set X
ht : IsClosed[inst] t
f : C(Y, ℝ)
hf : ∀ (x : Y), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : Y) → ℝ) x : ℝ)
hc :
  IsClosed[inst_1] (preimage (β := ℝ) (⇑f : (a : Y) → ℝ) {0}) ∧
    e '' t = preimage (β := ℝ) (⇑f : (a : Y) → ℝ) {0} ∩ range e
⊢ t = preimage (β := ℝ) (⇑{ toFun := (⇑f : (a : Y) → ℝ) ∘ e, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) {0}

Tactic:
simpa [Set.ext_iff, he.injective.preimage_image] using congr(e ⁻¹' $(hc.2))

Premises used: And.right, Function.Injective.preimage_image, Topology.IsEmbedding.injective, Set.ext_iff
-- Module: Mathlib.Topology.Separation.PerfectlyNormal
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
inst_2 : PerfectlyNormalSpace X
⊢ PerfectlyNormalSpace.{u_1} (↑s : Type u_1)

Tactic:
IsEmbedding.subtypeVal.perfectlyNormalSpace

Premises used: Topology.IsEmbedding.perfectlyNormalSpace, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
isTotallySeparated_univ : IsTotallySeparated.{u_1} (α := X) univ
⊢ TotallySeparatedSpace X

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
isTotallySeparated_univ :
  ∀ (U : Set X) (hU : IsOpen[inst] U ∧ Xor (x ∈ U) (y ∈ U)),
    ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
choose U hU using exists_isOpen_xor_mem hxy

Premises used: exists_isOpen_xor_mem
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU : IsOpen[inst] U ∧ Xor (x ∈ U) (y ∈ U)
⊢ IsOpen[inst] U

Tactic:
obtain ⟨hU₀, hU₁⟩ := hU
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU : IsOpen[inst] U ∧ Xor (x ∈ U) (y ∈ U)
hU₀ : IsOpen[inst] U
⊢ Xor (x ∈ U) (y ∈ U)

Tactic:
obtain ⟨hU₀, hU₁⟩ := hU
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst] U
hU₁ : Xor (x ∈ U) (y ∈ U)
isTotallySeparated_univ :
  ∀ (hx : x ∈ U ∧ y ∉ U),
    ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
isTotallySeparated_univ₁ :
  ∀ (hy : y ∈ U ∧ x ∉ U),
    ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
rcases hU₁ with hx | hy
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst] U
hx : x ∈ U ∧ y ∉ U
isTotallySeparated_univ :
  ∀ (V : Set X) (hV : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} V ∧ x ∈ V ∧ V ⊆ U),
    ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
choose V hV using h.isOpen_iff.mp hU₀ x hx.1

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, And.left, Iff.mp
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst] U
hx : x ∈ U ∧ y ∉ U
V : Set X
hV : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} V ∧ x ∈ V ∧ V ⊆ U
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
⟨V, Vᶜ, hV.1.isOpen, hV.1.compl.isOpen, hV.2.1, notMem_subset hV.2.2 hx.2,
      (union_compl_self V).superset, disjoint_compl_right⟩

Premises used: Compl.compl, IsClopen.compl, Set.union_compl_self, IsClopen.isOpen, And.right, And.left, And.intro, Exists.intro, disjoint_compl_right, Eq.superset, Set.notMem_subset
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst] U
hx : x ∈ U ∧ y ∉ U
V : Set X
hV : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} V ∧ x ∈ V ∧ V ⊆ U
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
exact ⟨V, Vᶜ, hV.1.isOpen, hV.1.compl.isOpen, hV.2.1, notMem_subset hV.2.2 hx.2,
      (union_compl_self V).superset, disjoint_compl_right⟩
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst] U
hy : y ∈ U ∧ x ∉ U
isTotallySeparated_univ :
  ∀ (V : Set X) (hV : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} V ∧ y ∈ V ∧ V ⊆ U),
    ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
choose V hV using h.isOpen_iff.mp hU₀ y hy.1

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, And.left, Iff.mp
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst] U
hy : y ∈ U ∧ x ∉ U
V : Set X
hV : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} V ∧ y ∈ V ∧ V ⊆ U
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
⟨Vᶜ, V, hV.1.compl.isOpen, hV.1.isOpen, notMem_subset hV.2.2 hy.2, hV.2.1,
      (union_comm _ _ ▸ union_compl_self V).superset, disjoint_compl_left⟩

Premises used: Compl.compl, IsClopen.compl, disjoint_compl_left, IsClopen.isOpen, And.right, And.left, And.intro, Exists.intro, Set.notMem_subset
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
h : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU₀ : IsOpen[inst] U
hy : y ∈ U ∧ x ∉ U
V : Set X
hV : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} V ∧ y ∈ V ∧ V ⊆ U
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
exact ⟨Vᶜ, V, hV.1.compl.isOpen, hV.1.isOpen, notMem_subset hV.2.2 hy.2, hV.2.1,
      (union_comm _ _ ▸ union_compl_self V).superset, disjoint_compl_left⟩
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
mp : U ∈ 𝓝 x → ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
mpr : (∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U) → U ∈ 𝓝 x
⊢ U ∈ 𝓝 x ↔ ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
⊢ connectedComponent x = {x}

Tactic:
have hx : connectedComponent x = {x} :=
        totallyDisconnectedSpace_iff_connectedComponent_singleton.mp ‹_› x
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : connectedComponent x = {x}
⊢ Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}

Tactic:
rw [connectedComponent_eq_iInter_isClopen] at hx

Premises used: connectedComponent_eq_iInter_isClopen
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
mp :
  ∀ (s : Set X) (hs : IsClopen s) (hs' : x ∈ s)
    (hs'' : (↑(Subtype.mk (p := fun (s : Set X) ↦ IsClopen s ∧ x ∈ s) s ⋯) : Set X) ⊆ U),
    ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
rsuffices : ∃ (s : N), (↑s : Set X) ⊆ U
⊢ ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

Tactic:
rsuffices ⟨⟨s, hs, hs'⟩, hs''⟩ : ∃ s : N, s.val ⊆ U
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
s : Set X
hs : IsClopen s
hs' : x ∈ s
hs'' : (↑(Subtype.mk (p := fun (s : Set X) ↦ IsClopen s ∧ x ∈ s) s ⋯) : Set X) ⊆ U
⊢ ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

Tactic:
⟨s, ⟨hs', hs⟩, hs''⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
s : Set X
hs : IsClopen s
hs' : x ∈ s
hs'' : (↑(Subtype.mk (p := fun (s : Set X) ↦ IsClopen s ∧ x ∈ s) s ⋯) : Set X) ⊆ U
⊢ ∃ (i : Set X), (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

Tactic:
exact ⟨s, ⟨hs', hs⟩, hs''⟩
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
⊢ Nonempty N

Tactic:
haveI : Nonempty N := ⟨⟨univ, isClopen_univ, mem_univ x⟩⟩
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
this : Nonempty N
⊢ ∀ (s : N), IsClosed[inst] (↑s : Set X)

Tactic:
have hNcl : ∀ s : N, IsClosed s.val := fun s => s.property.1.1
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst] (↑s : Set X)
s : Set X
hs : IsClopen s
hxs : x ∈ s
t : Set X
ht : IsClopen t
hxt : x ∈ t
⊢ ∃ (z : N),
    Superset.{u_1} (α := Set X)
        ((fun (s : N) ↦ (↑s : Set X)) (Subtype.mk (p := fun (s : Set X) ↦ IsClopen s ∧ x ∈ s) s ⋯))
        ((fun (s : N) ↦ (↑s : Set X)) z) ∧
      Superset.{u_1} (α := Set X)
        ((fun (s : N) ↦ (↑s : Set X)) (Subtype.mk (p := fun (s : Set X) ↦ IsClopen s ∧ x ∈ s) t ⋯))
        ((fun (s : N) ↦ (↑s : Set X)) z)

Tactic:
⟨⟨s ∩ t, hs.inter ht, ⟨hxs, hxt⟩⟩, inter_subset_left, inter_subset_right⟩

Premises used: IsClopen.inter, Set.inter_subset_left, Subtype.mk, Inter.inter, And.intro, Exists.intro, Set.inter_subset_right
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst] (↑s : Set X)
s : Set X
hs : IsClopen s
hxs : x ∈ s
t : Set X
ht : IsClopen t
hxt : x ∈ t
⊢ ∃ (z : N),
    Superset.{u_1} (α := Set X)
        ((fun (s : N) ↦ (↑s : Set X)) (Subtype.mk (p := fun (s : Set X) ↦ IsClopen s ∧ x ∈ s) s ⋯))
        ((fun (s : N) ↦ (↑s : Set X)) z) ∧
      Superset.{u_1} (α := Set X)
        ((fun (s : N) ↦ (↑s : Set X)) (Subtype.mk (p := fun (s : Set X) ↦ IsClopen s ∧ x ∈ s) t ⋯))
        ((fun (s : N) ↦ (↑s : Set X)) z)

Tactic:
exact ⟨⟨s ∩ t, hs.inter ht, ⟨hxs, hxt⟩⟩, inter_subset_left, inter_subset_right⟩
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst] (↑s : Set X)
⊢ Directed (α := Set X) Superset fun (s : N) ↦ (↑s : Set X)

Tactic:
have hdir : Directed Superset fun s : N => s.val := by
        rintro ⟨s, hs, hxs⟩ ⟨t, ht, hxt⟩
        exact ⟨⟨s ∩ t, hs.inter ht, ⟨hxs, hxt⟩⟩, inter_subset_left, inter_subset_right⟩
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst] (↑s : Set X)
hdir : Directed (α := Set X) Superset fun (s : N) ↦ (↑s : Set X)
y : X
y_in : Membership.mem (γ := Set X) (⋂ (s : N), (↑s : Set X)) y
⊢ y = x

Tactic:
rw [hx, mem_singleton_iff] at y_in

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst] (↑s : Set X)
hdir : Directed (α := Set X) Superset fun (s : N) ↦ (↑s : Set X)
y : X
y_in : y = x
rwa rwa₁ rwa₂ rwa₃ : U ∈ 𝓝 x
⊢ U ∈ 𝓝 y

Tactic:
rwa [y_in]
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst] (↑s : Set X)
hdir : Directed (α := Set X) Superset fun (s : N) ↦ (↑s : Set X)
⊢ ∀ (y : X), Membership.mem (γ := Set X) (⋂ (s : N), (↑s : Set X)) y → U ∈ 𝓝 y

Tactic:
have h_nhds : ∀ y ∈ ⋂ s : N, s.val, U ∈ 𝓝 y := fun y y_in => by
        rw [hx, mem_singleton_iff] at y_in
        rwa [y_in]