awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst] U ⊆ V
UV : (↑s : Type u_1) := Subtype.mk (p := fun (x : Set X × Set X) ↦ x ∈ s) (U, V) ⋯
y : X
hy : ¬y ∈ V
⊢ ε UV ≤ norm (E := ℝ) ((fun (x : X) ↦ ε UV) y)

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst] U ⊆ V
UV : (↑s : Type u_1) := Subtype.mk (p := fun (x : Set X × Set X) ↦ x ∈ s) (U, V) ⋯
y : X
hy : ¬y ∈ V
⊢ ε UV ≤ norm (E := ℝ) ((fun (x : X) ↦ ε UV) y)

Tactic:
exact le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
⊢ PseudoMetrizableSpace X

Tactic:
let ⟨_, hf⟩ := exists_isInducing_l_infty X
  hf.pseudoMetrizableSpace

Premises used: TopologicalSpace.PseudoMetrizableSpace, _private.0.TopologicalSpace.PseudoMetrizableSpace.of_regularSpace_secondCountableTopology.match_1, Topology.IsInducing.pseudoMetrizableSpace, TopologicalSpace.exists_isInducing_l_infty
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T3Space X
inst_2 : SecondCountableTopology X
⊢ ∃ (f : X → ℕ →ᵇ ℝ), IsEmbedding f

Tactic:
let ⟨f, hf⟩ := exists_isInducing_l_infty X; ⟨f, hf.isEmbedding⟩

Premises used: _private.0.TopologicalSpace.PseudoMetrizableSpace.of_regularSpace_secondCountableTopology.match_1, Exists, Topology.IsInducing.isEmbedding, TopologicalSpace.exists_isInducing_l_infty, Exists.intro, Topology.IsEmbedding
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T3Space X
inst_2 : SecondCountableTopology X
⊢ MetrizableSpace X

Tactic:
let ⟨_, hf⟩ := exists_embedding_l_infty X
  hf.metrizableSpace

Premises used: Topology.IsEmbedding.metrizableSpace, TopologicalSpace.MetrizableSpace, _private.0.TopologicalSpace.metrizableSpace_of_t3_secondCountable.match_1, TopologicalSpace.exists_embedding_l_infty
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
this : ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
rcases :
  ∀ (U : ℕ → Set X) (hne : ∀ (n : ℕ), (U n).Nonempty) (ho : ∀ (n : ℕ), IsOpen[inst] (U n))
    (hd : Pairwise (Disjoint on U)),
    ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
rcases this with ⟨U, hne, ho, hd⟩
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
⟨fun n ↦ ⋃ m, U (.pair n m), ?_, fun _ ↦ isOpen_iUnion fun _ ↦ ho _, ?_⟩

Premises used: Nat.pair, isOpen_iUnion, And.intro, Exists.intro, Set.iUnion
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
refine_1 : ∀ (n : ℕ), Set.Infinite.{u_1} (α := X) ((fun (n : ℕ) ↦ (⋃ (m : ℕ), U (Nat.pair n m) : Set X)) n)
refine_2 : Pairwise (α := ℕ) (onFun.{1, u_1 + 1, 1} (β := Set X) Disjoint fun (n : ℕ) ↦ ⋃ (m : ℕ), U (Nat.pair n m))
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
refine ⟨fun n ↦ ⋃ m, U (.pair n m), ?_, fun _ ↦ isOpen_iUnion fun _ ↦ ho _, ?_⟩
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
⊢ ∀ (n : ℕ), Set.Infinite.{u_1} (α := X) ((fun (n : ℕ) ↦ (⋃ (m : ℕ), U (Nat.pair n m) : Set X)) n)

Tactic:
fun n ↦ infinite_iUnion fun i j hij ↦ ?_

Premises used: Set.infinite_iUnion
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
refine_1 : ∀ (n i j : ℕ) (hij : U (Nat.pair n i) = U (Nat.pair n j)), i = j
⊢ ∀ (n : ℕ), Set.Infinite.{u_1} (α := X) ((fun (n : ℕ) ↦ (⋃ (m : ℕ), U (Nat.pair n m) : Set X)) n)

Tactic:
refine fun n ↦ infinite_iUnion fun i j hij ↦ ?_

Premises used: Set.infinite_iUnion
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
n i j : ℕ
hij : U (Nat.pair n i) = U (Nat.pair n j)
this : Nat.pair n i = Nat.pair n j
⊢ i = j

Tactic:
simpa
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
n i j : ℕ
hij : U (Nat.pair n i) = U (Nat.pair n j)
refine_1 : Nat.pair n i = Nat.pair n j
⊢ i = j

Tactic:
suffices n.pair i = n.pair j by simpa
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
n i j : ℕ
hij : U (Nat.pair n i) = U (Nat.pair n j)
refine_1 : ¬(Disjoint on U) (Nat.pair n i) (Nat.pair n j)
⊢ Nat.pair n i = Nat.pair n j

Tactic:
apply hd.eq

Premises used: Pairwise.eq
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
n i j : ℕ
hij : U (Nat.pair n i) = U (Nat.pair n j)
⊢ ¬(Disjoint on U) (Nat.pair n i) (Nat.pair n j)

Tactic:
simpa [hij, onFun] using (hne _).ne_empty

Premises used: Function.onFun, Set.Nonempty.ne_empty
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
⊢ Pairwise (α := ℕ) (onFun.{1, u_1 + 1, 1} (β := Set X) Disjoint fun (n : ℕ) ↦ ⋃ (m : ℕ), U (Nat.pair n m))

Tactic:
fun n n' hne ↦ disjoint_iUnion_left.2 fun m ↦ disjoint_iUnion_right.2 fun m' ↦ hd ?_

Premises used: Iff.mpr, Set.disjoint_iUnion_left, Set.disjoint_iUnion_right, Pairwise
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
refine_2 : ∀ (n n' : ℕ) (hne : n ≠ n') (m m' : ℕ), Nat.pair n m ≠ Nat.pair n' m'
⊢ Pairwise (α := ℕ) (onFun.{1, u_1 + 1, 1} (β := Set X) Disjoint fun (n : ℕ) ↦ ⋃ (m : ℕ), U (Nat.pair n m))

Tactic:
refine fun n n' hne ↦ disjoint_iUnion_left.2 fun m ↦ disjoint_iUnion_right.2 fun m' ↦ hd ?_

Premises used: Iff.mpr, Set.disjoint_iUnion_left, Set.disjoint_iUnion_right
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hne_1 : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
n n' : ℕ
hne : n ≠ n'
m m' : ℕ
⊢ Nat.pair n m ≠ Nat.pair n' m'

Tactic:
simp [hne]
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
suffices : ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
suffices ∃ U : ℕ → Set X, (∀ n, (U n).Nonempty) ∧ (∀ n, IsOpen (U n)) ∧
      Pairwise (Disjoint on U) by
    rcases this with ⟨U, hne, ho, hd⟩
    refine ⟨fun n ↦ ⋃ m, U (.pair n m), ?_, fun _ ↦ isOpen_iUnion fun _ ↦ ho _, ?_⟩
    · refine fun n ↦ infinite_iUnion fun i j hij ↦ ?_
      suffices n.pair i = n.pair j by simpa
      apply hd.eq
      simpa [hij, onFun] using (hne _).ne_empty
    · refine fun n n' hne ↦ disjoint_iUnion_left.2 fun m ↦ disjoint_iUnion_right.2 fun m' ↦ hd ?_
      simp [hne]
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
pos :
  ∀ (h : DiscreteTopology X),
    ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
neg :
  ∀ (h : ¬DiscreteTopology X),
    ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
by_cases h : DiscreteTopology X

Premises used: DiscreteTopology
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
h : DiscreteTopology X
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
⟨fun n ↦ {Infinite.natEmbedding X n}, fun _ ↦ singleton_nonempty _,
      fun _ ↦ isOpen_discrete _, fun _ _ h ↦ ?_⟩

Premises used: Set.singleton_nonempty, And.intro, isOpen_discrete, Exists.intro, Singleton.singleton, DFunLike.coe, Infinite.natEmbedding
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
h : DiscreteTopology X
pos :
  ∀ (x x_1 : ℕ) (h : x ≠ x_1),
    onFun.{1, u_1 + 1, 1} (β := Set X) Disjoint
      (fun (n : ℕ) ↦ singleton (α := X) ((Infinite.natEmbedding X : (a : ℕ) → X) n : X)) x x_1
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
refine ⟨fun n ↦ {Infinite.natEmbedding X n}, fun _ ↦ singleton_nonempty _,
      fun _ ↦ isOpen_discrete _, fun _ _ h ↦ ?_⟩
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
h_1 : DiscreteTopology X
x x_1 : ℕ
h : x ≠ x_1
⊢ onFun.{1, u_1 + 1, 1} (β := Set X) Disjoint
    (fun (n : ℕ) ↦ singleton (α := X) ((Infinite.natEmbedding X : (a : ℕ) → X) n : X)) x x_1

Tactic:
simpa using h
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
h : ¬DiscreteTopology X
⊢ ∃ (x : X), (𝓝[≠] x).NeBot

Tactic:
simp only [discreteTopology_iff_nhds_ne, not_forall, ← ne_eq, ← neBot_iff] at h

Premises used: Filter.neBot_iff, ne_eq, discreteTopology_iff_nhds_ne, Classical.not_forall
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
h : ∃ (x : X), (𝓝[≠] x).NeBot
neg :
  ∀ (x : X) (hx : (𝓝[≠] x).NeBot),
    ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
rcases h with ⟨x, hx⟩
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this : ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty ∧ IsOpen[inst] (U n) ∧ (U n)ᶜ ∈ 𝓝 x) ∧ Pairwise (Disjoint on U)
rcases :
  ∀ (U : ℕ → Set X) (hU : ∀ (n : ℕ), (U n).Nonempty ∧ IsOpen[inst] (U n) ∧ (U n)ᶜ ∈ 𝓝 x)
    (hd : Pairwise (Disjoint on U)),
    ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
rcases this with ⟨U, hU, hd⟩
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
U : ℕ → Set X
hU : ∀ (n : ℕ), (U n).Nonempty ∧ IsOpen[inst] (U n) ∧ (U n)ᶜ ∈ 𝓝 x
hd : Pairwise (Disjoint on U)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
⟨U, fun n ↦ (hU n).1, fun n ↦ (hU n).2.1, hd⟩

Premises used: And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
U : ℕ → Set X
hU : ∀ (n : ℕ), (U n).Nonempty ∧ IsOpen[inst] (U n) ∧ (U n)ᶜ ∈ 𝓝 x
hd : Pairwise (Disjoint on U)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
exact ⟨U, fun n ↦ (hU n).1, fun n ↦ (hU n).2.1, hd⟩
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
neg : ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty ∧ IsOpen[inst] (U n) ∧ (U n)ᶜ ∈ 𝓝 x) ∧ Pairwise (Disjoint on U)
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
suffices ∃ U : ℕ → Set X, (∀ n, (U n).Nonempty ∧ IsOpen (U n) ∧ (U n)ᶜ ∈ 𝓝 x) ∧
        Pairwise (Disjoint on U) by
      rcases this with ⟨U, hU, hd⟩
      exact ⟨U, fun n ↦ (hU n).1, fun n ↦ (hU n).2.1, hd⟩
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
⊢ Std.Symm.{u_1 + 1} (α := Set X) Disjoint

Tactic:
have : Std.Symm (α := Set X) Disjoint := ⟨fun _ _ h ↦ h.symm⟩
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty ∧ IsOpen[inst] (U n) ∧ (U n)ᶜ ∈ 𝓝 x) ∧ Pairwise (Disjoint on U)

Tactic:
exists_seq_of_forall_finset_exists' (fun U : Set X ↦ U.Nonempty ∧ IsOpen U ∧ Uᶜ ∈ 𝓝 x)
      Disjoint fun S hS ↦ ?_

Premises used: Compl.compl, Disjoint, Membership.mem, nhds, And, Set.Nonempty, IsOpen, exists_seq_of_forall_finset_exists'
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
neg :
  ∀ (S : Finset (Set X)) (hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1),
    ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y
⊢ ∃ (U : ℕ → Set X), (∀ (n : ℕ), (U n).Nonempty ∧ IsOpen[inst] (U n) ∧ (U n)ᶜ ∈ 𝓝 x) ∧ Pairwise (Disjoint on U)

Tactic:
refine exists_seq_of_forall_finset_exists' (fun U : Set X ↦ U.Nonempty ∧ IsOpen U ∧ Uᶜ ∈ 𝓝 x)
      Disjoint fun S hS ↦ ?_

Premises used: Compl.compl, Disjoint, Membership.mem, nhds, And, Set.Nonempty, IsOpen, exists_seq_of_forall_finset_exists'
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
⊢ (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x

Tactic:
have : (⋂ U ∈ S, interior (Uᶜ)) \ {x} ∈ 𝓝[≠] x := inter_mem_inf ((biInter_finset_mem _).2
      fun U hU ↦ interior_mem_nhds.2 (hS _ hU).2.2) (mem_principal_self _)
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this_1 : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
neg :
  ∀ (y : X) (hyU : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) y) (hyx : y ≠ x),
    ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y
⊢ ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y

Tactic:
rcases hx.nonempty_of_mem this with ⟨y, hyU, hyx : y ≠ x⟩

Premises used: Filter.NeBot.nonempty_of_mem
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this_1 : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) y
hyx : y ≠ x
neg :
  ∀ (V W : Set X) (hVo : IsOpen[inst] V) (hWo : IsOpen[inst] W) (hyV : y ∈ V) (hxW : x ∈ W) (hVW : Disjoint V W),
    ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y
⊢ ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y

Tactic:
rcases t2_separation hyx with ⟨V, W, hVo, hWo, hyV, hxW, hVW⟩

Premises used: t2_separation
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this_1 : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) y
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst] V
hWo : IsOpen[inst] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
⊢ ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y

Tactic:
⟨V ∩ ⋂ U ∈ S, interior (Uᶜ), ⟨⟨y, hyV, hyU⟩, ?_, ?_⟩, fun U hU ↦ ?_⟩

Premises used: Set.iInter, Compl.compl, Inter.inter, And.intro, interior, Exists.intro
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this_1 : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) y
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst] V
hWo : IsOpen[inst] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
neg : IsOpen[inst] (V ∩ ⋂ U ∈ S, interior Uᶜ)
neg₁ : (V ∩ ⋂ U ∈ S, interior Uᶜ)ᶜ ∈ 𝓝 x
neg₂ : ∀ (U : Set X) (hU : U ∈ S), Disjoint U (V ∩ ⋂ U ∈ S, interior Uᶜ)
⊢ ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y

Tactic:
refine ⟨V ∩ ⋂ U ∈ S, interior (Uᶜ), ⟨⟨y, hyV, hyU⟩, ?_, ?_⟩, fun U hU ↦ ?_⟩
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this_1 : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) y
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst] V
hWo : IsOpen[inst] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
⊢ IsOpen[inst] (V ∩ ⋂ U ∈ S, interior Uᶜ)

Tactic:
hVo.inter (isOpen_biInter_finset fun _ _ ↦ isOpen_interior)

Premises used: isOpen_interior, isOpen_biInter_finset, IsOpen.inter
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this_1 : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) y
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst] V
hWo : IsOpen[inst] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
⊢ IsOpen[inst] (V ∩ ⋂ U ∈ S, interior Uᶜ)

Tactic:
exact hVo.inter (isOpen_biInter_finset fun _ _ ↦ isOpen_interior)

Premises used: isOpen_interior, isOpen_biInter_finset, IsOpen.inter
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this_1 : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) y
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst] V
hWo : IsOpen[inst] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
⊢ (V ∩ ⋂ U ∈ S, interior Uᶜ)ᶜ ∈ 𝓝 x

Tactic:
mem_of_superset (hWo.mem_nhds hxW) fun z hzW ⟨hzV, _⟩ ↦ ?_

Premises used: False, IsOpen.mem_nhds, Filter.mem_of_superset, _private.0.exists_seq_infinite_isOpen_pairwise_disjoint.match_5