awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
b : Bool
x : α
hx : x ∈ S b
apply :
  ball x (B (U b (Subtype.mk (p := fun (x : α) ↦ x ∈ S b) x hx))) ⊆ ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x))
⊢ ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝 x

Tactic:
apply mem_of_superset (ball_mem_nhds x (hB.mem (U b ⟨x, hx⟩)))

Premises used: UniformSpace.ball_mem_nhds, Filter.HasAntitoneBasis.mem, Subtype.mk, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
b : Bool
x : α
hx : x ∈ S b
⊢ ball x (B (U b (Subtype.mk (p := fun (x : α) ↦ x ∈ S b) x hx))) ⊆ ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x))

Tactic:
subset_iUnion (fun x => ball x.1 (B (U b x))) ⟨x, hx⟩

Premises used: UniformSpace.ball, Subtype.mk, Set.subset_iUnion
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
b : Bool
x : α
hx : x ∈ S b
⊢ ball x (B (U b (Subtype.mk (p := fun (x : α) ↦ x ∈ S b) x hx))) ⊆ ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x))

Tactic:
exact subset_iUnion (fun x => ball x.1 (B (U b x))) ⟨x, hx⟩

Premises used: UniformSpace.ball, Subtype.mk, Set.subset_iUnion
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
⊢ ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)

Tactic:
have hUS (b : Bool) : ⋃ x, ball x.1 (B (U b x)) ∈ nhdsSet (S b) := by
      rw [mem_nhdsSet_iff_forall]
      intro x hx
      apply mem_of_superset (ball_mem_nhds x (hB.mem (U b ⟨x, hx⟩)))
      exact subset_iUnion (fun x => ball x.1 (B (U b x))) ⟨x, hx⟩
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
rw : ∃ s_1 ∈ 𝓝ˢ s, ∃ t_1 ∈ 𝓝ˢ t, Disjoint s_1 t_1
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
rw [Filter.disjoint_iff]

Premises used: Filter.disjoint_iff
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
⊢ ∃ s_1 ∈ 𝓝ˢ s, ∃ t_1 ∈ 𝓝ˢ t, Disjoint s_1 t_1

Tactic:
⟨_, hUS false, _, hUS true, ?_⟩

Premises used: Bool.true, And.intro, Exists.intro, Bool.false
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
refine :
  Disjoint.{u} (α := Set α) (⋃ (x : (↑(S false) : Type u)), ball (↑x : α) (B (U false x)))
    (⋃ (x : (↑(S true) : Type u)), ball (↑x : α) (B (U true x)))
⊢ ∃ s_1 ∈ 𝓝ˢ s, ∃ t_1 ∈ 𝓝ˢ t, Disjoint s_1 t_1

Tactic:
refine ⟨_, hUS false, _, hUS true, ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
b : Bool
x : (↑(S b) : Type u)
y : (↑(S !b) : Type u)
hxy : U b x ≤ U (!b) y
rw : ball (↑x : α) (B (U b x)) ∩ ball (↑y : α) (B (U (!b) y)) ⊆ ∅
⊢ Disjoint (ball (↑x : α) (B (U b x))) (ball (↑y : α) (B (U (!b) y)))

Tactic:
rw [Set.disjoint_iff]

Premises used: Set.disjoint_iff
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
b : Bool
x : (↑(S b) : Type u)
y : (↑(S !b) : Type u)
hxy : U b x ≤ U (!b) y
z : α
hz : z ∈ ball (↑x : α) (B (U b x)) ∩ ball (↑y : α) (B (U (!b) y))
⊢ Membership.mem (γ := Set α) ∅ z

Tactic:
(hU b x).notMem_of_mem_left (mem_ball_comp hz.1 (hB.antitone hxy hz.2)) y.2

Premises used: UniformSpace.mem_ball_comp, Set.Mem, And.right, And.left, Disjoint.notMem_of_mem_left, Filter.HasAntitoneBasis.antitone, Subtype.property
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
b : Bool
x : (↑(S b) : Type u)
y : (↑(S !b) : Type u)
hxy : U b x ≤ U (!b) y
z : α
hz : z ∈ ball (↑x : α) (B (U b x)) ∩ ball (↑y : α) (B (U (!b) y))
⊢ Membership.mem (γ := Set α) ∅ z

Tactic:
exact (hU b x).notMem_of_mem_left (mem_ball_comp hz.1 (hB.antitone hxy hz.2)) y.2

Premises used: UniformSpace.mem_ball_comp, And.right, And.left, Disjoint.notMem_of_mem_left, Filter.HasAntitoneBasis.antitone, Subtype.property
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
⊢ ∀ (b : Bool) (x : (↑(S b) : Type u)) (y : (↑(S !b) : Type u)) (hxy : U b x ≤ U (!b) y),
    Disjoint (ball (↑x : α) (B (U b x))) (ball (↑y : α) (B (U (!b) y)))

Tactic:
have hdj (b : Bool) (x : S b) (y : S (!b)) (hxy : U b x ≤ U (!b) y) :
        Disjoint (ball x.1 (B (U b x))) (ball y.1 (B (U (!b) y))) := by
      rw [Set.disjoint_iff]
      intro z hz
      exact (hU b x).notMem_of_mem_left (mem_ball_comp hz.1 (hB.antitone hxy hz.2)) y.2
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
hdj :
  ∀ (b : Bool) (x : (↑(S b) : Type u)) (y : (↑(S !b) : Type u)) (hxy : U b x ≤ U (!b) y),
    Disjoint (ball (↑x : α) (B (U b x))) (ball (↑y : α) (B (U (!b) y)))
simp_rw :
  ∀ (i : (↑(S false) : Type u)) (i_1 : (↑(S true) : Type u)),
    Disjoint (ball (↑i : α) (B (U false i))) (ball (↑i_1 : α) (B (U true i_1)))
⊢ Disjoint.{u} (α := Set α) (⋃ (x : (↑(S false) : Type u)), ball (↑x : α) (B (U false x)))
    (⋃ (x : (↑(S true) : Type u)), ball (↑x : α) (B (U true x)))

Tactic:
simp_rw [disjoint_iUnion_left, disjoint_iUnion_right]

Premises used: Set.disjoint_iUnion_left, Set.disjoint_iUnion_right
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
hdj :
  ∀ (b : Bool) (x : (↑(S b) : Type u)) (y : (↑(S !b) : Type u)) (hxy : U b x ≤ U (!b) y),
    Disjoint (ball (↑x : α) (B (U b x))) (ball (↑y : α) (B (U (!b) y)))
x : (↑(S false) : Type u)
y : (↑(S true) : Type u)
⊢ Disjoint (ball (↑x : α) (B (U false x))) (ball (↑y : α) (B (U true y)))

Tactic:
(le_total (U false x) (U true y)).elim
      (fun h => hdj false x y h) (fun h => (hdj true y x h).symm)

Premises used: le_total, Bool.true, Disjoint.symm, Or.elim, Bool.false
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst.toTopologicalSpace] t)
S : (b : Bool) → Set α := fun (b : Bool) ↦ Bool.casesOn (motive := fun (x : Bool) ↦ Set α) b s t
U : (b : Bool) → (x : (↑(S b) : Type u)) → ι
hU : ∀ (b : Bool) (x : (↑(S b) : Type u)), Disjoint (ball (↑x : α) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)
hdj :
  ∀ (b : Bool) (x : (↑(S b) : Type u)) (y : (↑(S !b) : Type u)) (hxy : U b x ≤ U (!b) y),
    Disjoint (ball (↑x : α) (B (U b x))) (ball (↑y : α) (B (U (!b) y)))
x : (↑(S false) : Type u)
y : (↑(S true) : Type u)
⊢ Disjoint (ball (↑x : α) (B (U false x))) (ball (↑y : α) (B (U true y)))

Tactic:
exact (le_total (U false x) (U true y)).elim
      (fun h => hdj false x y h) (fun h => (hdj true y x h).symm)

Premises used: le_total, Bool.true, Disjoint.symm, Or.elim, Bool.false
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : (𝓤 α).IsCountablyGenerated
⊢ CompletelyNormalSpace α

Tactic:
(has_seq_basis α).elim fun _ hB =>
    UniformSpace.completelyNormalSpace_of_hasAntitoneBasis hB.1

Premises used: And.left, UniformSpace.completelyNormalSpace_of_hasAntitoneBasis, UniformSpace.has_seq_basis, Exists.elim
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Sort u_1
p : ι → Prop
s : ι → Set (α × α)
h : (𝓤 α).HasBasis p s
x y : α
⊢ x ⤳ y ↔ ∀ (i : ι), p i → (x, y) ∈ s i

Tactic:
(nhds_basis_uniformity h).specializes_iff

Premises used: Set.Mem, setOf, nhds_basis_uniformity, Filter.HasBasis.specializes_iff
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Sort u_1
p : ι → Prop
s : ι → Set (α × α)
h : (𝓤 α).HasBasis p s
x y : α
⊢ Inseparable x y ↔ ∀ (i : ι), p i → (x, y) ∈ s i

Tactic:
specializes_iff_inseparable.symm.trans h.specializes_iff_uniformity

Premises used: Iff.trans, specializes_iff_inseparable, Iff.symm, Filter.HasBasis.specializes_iff_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
x y : α
⊢ Inseparable x y ↔ (x, y) ∈ (𝓤 α).ker

Tactic:
(𝓤 α).basis_sets.inseparable_iff_uniformity

Premises used: Set.Mem, uniformity, setOf, Filter.basis_sets, Set.sInter, Filter.ker, Filter.HasBasis.inseparable_iff_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
x y : α
h : Inseparable x y
rw : 𝓝 (y, y) ≤ 𝓤 α
⊢ 𝓝 (x, y) ≤ 𝓤 α

Tactic:
rw [h.prod rfl]

Premises used: Inseparable.rfl, Inseparable.prod
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
x y : α
h : Inseparable x y
⊢ 𝓝 (y, y) ≤ 𝓤 α

Tactic:
apply nhds_le_uniformity

Premises used: nhds_le_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
x y : α
⊢ Inseparable x y ↔ ClusterPt (x, y) (𝓤 α)

Tactic:
⟨fun h ↦ .of_nhds_le h.nhds_le_uniformity, fun h ↦ ?_⟩

Premises used: Iff.intro, ClusterPt.of_nhds_le, Inseparable.nhds_le_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
x y : α
refine : ∀ (h : ClusterPt (x, y) (𝓤 α)), Inseparable x y
⊢ Inseparable x y ↔ ClusterPt (x, y) (𝓤 α)

Tactic:
refine ⟨fun h ↦ .of_nhds_le h.nhds_le_uniformity, fun h ↦ ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
x y : α
h : ClusterPt (x, y) (𝓤 α)
simp_rw : ∀ (i : SetRel α α), (i ∈ 𝓤 α ∧ ∀ (a : α × α), ClusterPt a (𝓟 i) → a ∈ i) → (x, y) ∈ id i
⊢ Inseparable x y

Tactic:
simp_rw [uniformity_hasBasis_closed.inseparable_iff_uniformity, isClosed_iff_clusterPt]

Premises used: uniformity_hasBasis_closed, isClosed_iff_clusterPt, Filter.HasBasis.inseparable_iff_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
x y : α
h : ClusterPt (x, y) (𝓤 α)
⊢ ∀ (i : SetRel α α), (i ∈ 𝓤 α ∧ ∀ (a : α × α), ClusterPt a (𝓟 i) → a ∈ i) → (x, y) ∈ id i

Tactic:
fun U ⟨hU, hUc⟩ ↦ hUc _ <| h.mono <| le_principal_iff.2 hU

Premises used: Iff.mpr, ClusterPt.mono, Filter.le_principal_iff, Membership.mem, id, Prod.mk, _private.0.inseparable_iff_clusterPt_uniformity.match_1
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
x y : α
h : ClusterPt (x, y) (𝓤 α)
⊢ ∀ (i : SetRel α α), (i ∈ 𝓤 α ∧ ∀ (a : α × α), ClusterPt a (𝓟 i) → a ∈ i) → (x, y) ∈ id i

Tactic:
exact fun U ⟨hU, hUc⟩ ↦ hUc _ <| h.mono <| le_principal_iff.2 hU
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
⊢ T0Space α ↔ ∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y

Tactic:
simp only [t0Space_iff_inseparable, inseparable_iff_ker_uniformity, mem_ker]

Premises used: t0Space_iff_inseparable, inseparable_iff_ker_uniformity, Filter.mem_ker
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
⊢ T0Space α ↔ Pairwise fun (x y : α) ↦ ∃ r ∈ 𝓤 α, (x, y) ∉ r

Tactic:
simp [t0Space_iff_not_inseparable, inseparable_iff_ker_uniformity]

Premises used: inseparable_iff_ker_uniformity, t0Space_iff_not_inseparable
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
simp_rw : (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) → ∀ (x : α), ∀ s ∈ 𝓤 α, (x, x) ∈ s
⊢ T0Space α ↔ (𝓤 α).ker = diagonal α

Tactic:
simp_rw [t0Space_iff_uniformity, subset_antisymm_iff, diagonal_subset_iff, subset_def,
    Prod.forall, Filter.mem_ker, mem_diagonal_iff, iff_self_and]

Premises used: Set.subset_def, t0Space_iff_uniformity, iff_self_and, Set.mem_diagonal_iff, Filter.mem_ker, subset_antisymm_iff, Prod.forall, Set.diagonal_subset_iff
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
⊢ (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) → ∀ (x : α), ∀ s ∈ 𝓤 α, (x, x) ∈ s

Tactic:
fun _ x s hs ↦ refl_mem_uniformity hs

Premises used: refl_mem_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
⊢ (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) → ∀ (x : α), ∀ s ∈ 𝓤 α, (x, x) ∈ s

Tactic:
exact fun _ x s hs ↦ refl_mem_uniformity hs

Premises used: refl_mem_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
x y : α
h : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (x, y) ∈ V
⊢ x = y

Tactic:
t0Space_iff_uniformity.mp ‹T0Space α› x y @h

Premises used: t0Space_iff_uniformity, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
ι : Sort u_2
p : ι → Prop
s : ι → Set (α × α)
hs : (𝓤 α).HasBasis p s
x y : α
h : ∀ {i : ι}, p i → (x, y) ∈ s i
⊢ x = y

Tactic:
(hs.inseparable_iff_uniformity.2 @h).eq

Premises used: Iff.mpr, Inseparable.eq, Filter.HasBasis.inseparable_iff_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
x y : α
h : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SetRel.IsSymm V → (x, y) ∈ V
⊢ ∀ {i : SetRel α α}, i ∈ 𝓤 α ∧ i.IsSymm → (x, y) ∈ id i

Tactic:
simpa
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
x y : α
h : ClusterPt (x, y) (𝓤 α)
⊢ x = y

Tactic:
(inseparable_iff_clusterPt_uniformity.2 h).eq

Premises used: Iff.mpr, Inseparable.eq, inseparable_iff_clusterPt_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
β : Type u_1
l : Filter β
inst_1 : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
⊢ Inseparable a b ↔ Tendsto (fun (x : β) ↦ (f x, g x)) l (𝓤 α)

Tactic:
⟨fun h ↦ (ha.prodMk_nhds hb).mono_right h.nhds_le_uniformity, fun h ↦ ?_⟩

Premises used: Iff.intro, Inseparable.nhds_le_uniformity, Filter.Tendsto.mono_right, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
β : Type u_1
l : Filter β
inst_1 : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
refine : ∀ (h : Tendsto (fun (x : β) ↦ (f x, g x)) l (𝓤 α)), Inseparable a b
⊢ Inseparable a b ↔ Tendsto (fun (x : β) ↦ (f x, g x)) l (𝓤 α)

Tactic:
refine ⟨fun h ↦ (ha.prodMk_nhds hb).mono_right h.nhds_le_uniformity, fun h ↦ ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
β : Type u_1
l : Filter β
inst_1 : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
h : Tendsto (fun (x : β) ↦ (f x, g x)) l (𝓤 α)
rw : ClusterPt (a, b) (𝓤 α)
⊢ Inseparable a b

Tactic:
rw [inseparable_iff_clusterPt_uniformity]

Premises used: inseparable_iff_clusterPt_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
β : Type u_1
l : Filter β
inst_1 : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
h : Tendsto (fun (x : β) ↦ (f x, g x)) l (𝓤 α)
⊢ ClusterPt (a, b) (𝓤 α)

Tactic:
(ClusterPt.of_le_nhds (ha.prodMk_nhds hb)).mono h

Premises used: ClusterPt.mono, ClusterPt.of_le_nhds, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
β : Type u_1
l : Filter β
inst_1 : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
h : Tendsto (fun (x : β) ↦ (f x, g x)) l (𝓤 α)
⊢ ClusterPt (a, b) (𝓤 α)

Tactic:
exact (ClusterPt.of_le_nhds (ha.prodMk_nhds hb)).mono h

Premises used: ClusterPt.mono, ClusterPt.of_le_nhds, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
rcases :
  ∀ (V₁ : Set (α × α)) (V₁_in : V₁ ∈ 𝓤 α) (V₁_symm : SetRel.IsSymm V₁) (h_comp : SetRel.comp V₁ V₁ ⊆ V₀),
    IsClosed[inst.toTopologicalSpace] s
⊢ IsClosed[inst.toTopologicalSpace] s

Tactic:
rcases comp_symm_mem_uniformity_sets V₀_in with ⟨V₁, V₁_in, V₁_symm, h_comp⟩

Premises used: comp_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
h : closure[inst.toTopologicalSpace] s ⊆ s
⊢ IsClosed[inst.toTopologicalSpace] s

Tactic:
apply isClosed_of_closure_subset

Premises used: isClosed_of_closure_subset
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : x ∈ closure[inst.toTopologicalSpace] s
⊢ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty

Tactic:
rw [mem_closure_iff_ball] at hx

Premises used: UniformSpace.mem_closure_iff_ball
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
h : ∀ (y : α) (hy : y ∈ ball x V₁) (hy' : y ∈ s), x ∈ s
⊢ x ∈ s

Tactic:
rcases hx V₁_in with ⟨y, hy, hy'⟩