awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X : Type u_5
Y : Type u_6
R : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
inst_5 : CompactSpace X
inst_6 : T2Space X
inst_7 : CompactSpace Y
inst_8 : T2Space Y
inst_9 : TotallyDisconnectedSpace X
this_1 : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this_2 : IsUniformAddGroup R := ⋯
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
this :
  Membership.mem (γ := Filter (C(X × Y, R) × C(X × Y, R))) (𝓤 C(X × Y, R))
    {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
J : Set (R × R)
hJu : J ∈ 𝓤 R
hJ' :
  Subset (α := Set (C(X × Y, R) × C(X × Y, R)))
    {fg : C(X × Y, R) × C(X × Y, R) |
      ∀ (x : X × Y), Membership.mem (α := R × R) J (((fg.1 : (a : X × Y) → R) x, (fg.2 : (a : X × Y) → R) x) : R × R)}
    {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
obtain :
  ∀ (n : ℕ) (g : Fin n → C(X, R)) (h : Fin n → C(Y, R))
    (hgh :
      ∀ (x : X) (y : Y),
        Membership.mem (α := R × R) J
          (((f : (a : X × Y) → R) (x, y),
              ∑ i : Fin n, HMul.hMul (α := R) (β := R) ((g i : (a : X) → R) x : R) ((h i : (a : Y) → R) y : R)) :
            R × R)),
    ∃ (x : C(X × Y, R)),
      x ∈
        U ∩
          Set.range (ι := C(X, R) ⊗[R] C(Y, R))
            (⇑(tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
⊢ ∃ (x : C(X × Y, R)),
    x ∈
      U ∩
        Set.range (ι := C(X, R) ⊗[R] C(Y, R))
          (⇑(tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))

Tactic:
obtain ⟨n, g, h, hgh⟩ := exists_finite_sum_mul_approximation_of_mem_uniformity f hJu

Premises used: ContinuousMap.exists_finite_sum_mul_approximation_of_mem_uniformity
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X : Type u_5
Y : Type u_6
R : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
inst_5 : CompactSpace X
inst_6 : T2Space X
inst_7 : CompactSpace Y
inst_8 : T2Space Y
inst_9 : TotallyDisconnectedSpace X
this_1 : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this_2 : IsUniformAddGroup R := ⋯
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
this :
  Membership.mem (γ := Filter (C(X × Y, R) × C(X × Y, R))) (𝓤 C(X × Y, R))
    {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
J : Set (R × R)
hJu : J ∈ 𝓤 R
hJ' :
  Subset (α := Set (C(X × Y, R) × C(X × Y, R)))
    {fg : C(X × Y, R) × C(X × Y, R) |
      ∀ (x : X × Y), Membership.mem (α := R × R) J (((fg.1 : (a : X × Y) → R) x, (fg.2 : (a : X × Y) → R) x) : R × R)}
    {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
n : ℕ
g : Fin n → C(X, R)
h : Fin n → C(Y, R)
hgh :
  ∀ (x : X) (y : Y),
    Membership.mem (α := R × R) J
      (((f : (a : X × Y) → R) (x, y),
          ∑ i : Fin n, HMul.hMul (α := R) (β := R) ((g i : (a : X) → R) x : R) ((h i : (a : Y) → R) y : R)) :
        R × R)
⊢ Membership.mem (γ := Set (C(X × Y, R) × C(X × Y, R)))
      {fg : C(X × Y, R) × C(X × Y, R) |
        ∀ (x : X × Y), Membership.mem (α := R × R) J (((fg.1 : (a : X × Y) → R) x, (fg.2 : (a : X × Y) → R) x) : R × R)}
      (f,
        ((tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
          (∑ i : Fin n, g i ⊗ₜ[R] h i)) →
    Membership.mem (γ := Set (C(X × Y, R) × C(X × Y, R))) {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
      (f,
        ((tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
          (∑ i : Fin n, g i ⊗ₜ[R] h i))

Tactic:
have hG := Set.mem_of_subset_of_mem hJ' (a := (f, tensorHom <| ∑ i, g i ⊗ₜ h i))
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X : Type u_5
Y : Type u_6
R : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
inst_5 : CompactSpace X
inst_6 : T2Space X
inst_7 : CompactSpace Y
inst_8 : T2Space Y
inst_9 : TotallyDisconnectedSpace X
this_1 : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this_2 : IsUniformAddGroup R := ⋯
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
this :
  Membership.mem (γ := Filter (C(X × Y, R) × C(X × Y, R))) (𝓤 C(X × Y, R))
    {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
J : Set (R × R)
hJu : J ∈ 𝓤 R
hJ' :
  Subset (α := Set (C(X × Y, R) × C(X × Y, R)))
    {fg : C(X × Y, R) × C(X × Y, R) |
      ∀ (x : X × Y), Membership.mem (α := R × R) J (((fg.1 : (a : X × Y) → R) x, (fg.2 : (a : X × Y) → R) x) : R × R)}
    {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
n : ℕ
g : Fin n → C(X, R)
h : Fin n → C(Y, R)
hgh :
  ∀ (x : X) (y : Y),
    Membership.mem (α := R × R) J
      (((f : (a : X × Y) → R) (x, y),
          ∑ i : Fin n, HMul.hMul (α := R) (β := R) ((g i : (a : X) → R) x : R) ((h i : (a : Y) → R) y : R)) :
        R × R)
hG :
  Membership.mem (γ := Set (C(X × Y, R) × C(X × Y, R)))
      {fg : C(X × Y, R) × C(X × Y, R) |
        ∀ (x : X × Y), Membership.mem (α := R × R) J (((fg.1 : (a : X × Y) → R) x, (fg.2 : (a : X × Y) → R) x) : R × R)}
      (f,
        ((tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
          (∑ i : Fin n, g i ⊗ₜ[R] h i)) →
    Membership.mem (γ := Set (C(X × Y, R) × C(X × Y, R))) {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
      (f,
        ((tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
          (∑ i : Fin n, g i ⊗ₜ[R] h i))
⊢ (∀ (a : X) (b : Y),
      Membership.mem (α := R × R) J
        (((f : (a : X × Y) → R) (a, b),
            (((tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
                  (∑ i : Fin n, g i ⊗ₜ[R] h i) :
                (a : X × Y) → R)
              (a, b)) :
          R × R)) →
    ((tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
        (∑ i : Fin n, g i ⊗ₜ[R] h i) ∈
      U

Tactic:
simp only [Prod.forall, Set.mem_setOf_eq, forall_const] at hG

Premises used: Set.mem_setOf_eq, Prod.forall, forall_const
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X : Type u_5
Y : Type u_6
R : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
inst_5 : CompactSpace X
inst_6 : T2Space X
inst_7 : CompactSpace Y
inst_8 : T2Space Y
inst_9 : TotallyDisconnectedSpace X
this_1 : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this_2 : IsUniformAddGroup R := ⋯
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
this :
  Membership.mem (γ := Filter (C(X × Y, R) × C(X × Y, R))) (𝓤 C(X × Y, R))
    {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
J : Set (R × R)
hJu : J ∈ 𝓤 R
hJ' :
  Subset (α := Set (C(X × Y, R) × C(X × Y, R)))
    {fg : C(X × Y, R) × C(X × Y, R) |
      ∀ (x : X × Y), Membership.mem (α := R × R) J (((fg.1 : (a : X × Y) → R) x, (fg.2 : (a : X × Y) → R) x) : R × R)}
    {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
n : ℕ
g : Fin n → C(X, R)
h : Fin n → C(Y, R)
hgh :
  ∀ (x : X) (y : Y),
    Membership.mem (α := R × R) J
      (((f : (a : X × Y) → R) (x, y),
          ∑ i : Fin n, HMul.hMul (α := R) (β := R) ((g i : (a : X) → R) x : R) ((h i : (a : Y) → R) y : R)) :
        R × R)
hG :
  (∀ (a : X) (b : Y),
      Membership.mem (α := R × R) J
        (((f : (a : X × Y) → R) (a, b),
            (((tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
                  (∑ i : Fin n, g i ⊗ₜ[R] h i) :
                (a : X × Y) → R)
              (a, b)) :
          R × R)) →
    ((tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
        (∑ i : Fin n, g i ⊗ₜ[R] h i) ∈
      U
⊢ ∀ (a : X) (b : Y),
    Membership.mem (α := R × R) J
      (((f : (a : X × Y) → R) (a, b),
          (((tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
                (∑ i : Fin n, g i ⊗ₜ[R] h i) :
              (a : X × Y) → R)
            (a, b)) :
        R × R)

Tactic:
simpa [tensorHom] using hgh

Premises used: ContinuousMap.tensorHom
-- Module: Mathlib.Topology.UniformSpace.ProdApproximation
Goal:
X : Type u_5
Y : Type u_6
R : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
inst_5 : CompactSpace X
inst_6 : T2Space X
inst_7 : CompactSpace Y
inst_8 : T2Space Y
inst_9 : TotallyDisconnectedSpace X
this_1 : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this_2 : IsUniformAddGroup R := ⋯
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
this :
  Membership.mem (γ := Filter (C(X × Y, R) × C(X × Y, R))) (𝓤 C(X × Y, R))
    {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
J : Set (R × R)
hJu : J ∈ 𝓤 R
hJ' :
  Subset (α := Set (C(X × Y, R) × C(X × Y, R)))
    {fg : C(X × Y, R) × C(X × Y, R) |
      ∀ (x : X × Y), Membership.mem (α := R × R) J (((fg.1 : (a : X × Y) → R) x, (fg.2 : (a : X × Y) → R) x) : R × R)}
    {p : C(X × Y, R) × C(X × Y, R) | p.1 = f → p.2 ∈ U}
n : ℕ
g : Fin n → C(X, R)
h : Fin n → C(Y, R)
hgh :
  ∀ (x : X) (y : Y),
    Membership.mem (α := R × R) J
      (((f : (a : X × Y) → R) (x, y),
          ∑ i : Fin n, HMul.hMul (α := R) (β := R) ((g i : (a : X) → R) x : R) ((h i : (a : Y) → R) y : R)) :
        R × R)
hG :
  (∀ (a : X) (b : Y),
      Membership.mem (α := R × R) J
        (((f : (a : X × Y) → R) (a, b),
            (((tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
                  (∑ i : Fin n, g i ⊗ₜ[R] h i) :
                (a : X × Y) → R)
              (a, b)) :
          R × R)) →
    ((tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))
        (∑ i : Fin n, g i ⊗ₜ[R] h i) ∈
      U
⊢ ∃ (x : C(X × Y, R)),
    x ∈
      U ∩
        Set.range (ι := C(X, R) ⊗[R] C(Y, R))
          (⇑(tensorHom : C(X, R) ⊗[R] C(Y, R) →ₗ[R] C(X × Y, R)) : (a : C(X, R) ⊗[R] C(Y, R)) → C(X × Y, R))

Tactic:
simpa using ⟨_, hG <| by simpa [tensorHom] using hgh⟩
-- Module: Mathlib.Topology.UniformSpace.Real
Goal:
a : ∀ (u : ℕ → ℝ), CauchySeq u → ∃ (a : ℝ), Tendsto u atTop (nhds a)
⊢ CompleteSpace ℝ

Tactic:
apply complete_of_cauchySeq_tendsto

Premises used: Metric.complete_of_cauchySeq_tendsto
-- Module: Mathlib.Topology.UniformSpace.Real
Goal:
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) u ⋯
⊢ ∃ (a : ℝ), Tendsto u atTop (nhds a)

Tactic:
⟨c.lim, fun s h => ?_⟩

Premises used: CauSeq.lim, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Real
Goal:
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) u ⋯
a : ∀ (s : Set ℝ) (h : s ∈ nhds c.lim), s ∈ map u atTop
⊢ ∃ (a : ℝ), Tendsto u atTop (nhds a)

Tactic:
refine ⟨c.lim, fun s h => ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Real
Goal:
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) u ⋯
s : Set ℝ
h : s ∈ nhds c.lim
a : ∀ (ε : ℝ) (ε0 : ε > 0) (hε : ball c.lim ε ⊆ s), s ∈ map u atTop
⊢ s ∈ map u atTop

Tactic:
rcases Metric.mem_nhds_iff.1 h with ⟨ε, ε0, hε⟩

Premises used: Metric.mem_nhds_iff, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Real
Goal:
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) u ⋯
s : Set ℝ
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
⊢ ∃ (i : ℕ), ∀ j ≥ i, |(↑(c - CauSeq.const abs c.lim) : ℕ → ℝ) j| < ε

Tactic:
have := c.equiv_lim ε ε0
-- Module: Mathlib.Topology.UniformSpace.Real
Goal:
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) u ⋯
s : Set ℝ
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
this : ∃ (i : ℕ), ∀ j ≥ i, |(↑(c - CauSeq.const abs c.lim) : ℕ → ℝ) j| < ε
a : ∃ (a : ℕ), ∀ b ≥ a, b ∈ u ⁻¹' s
⊢ s ∈ map u atTop

Tactic:
simp only [mem_map, mem_atTop_sets]

Premises used: Filter.mem_atTop_sets, Filter.mem_map
-- Module: Mathlib.Topology.UniformSpace.Real
Goal:
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) u ⋯
s : Set ℝ
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
this : ∃ (i : ℕ), ∀ j ≥ i, |(↑(c - CauSeq.const abs c.lim) : ℕ → ℝ) j| < ε
⊢ ∃ (a : ℕ), ∀ b ≥ a, b ∈ u ⁻¹' s

Tactic:
this.imp fun N hN n hn => hε (hN n hn)

Premises used: Exists.imp
-- Module: Mathlib.Topology.UniformSpace.Real
Goal:
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) u ⋯
s : Set ℝ
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
this : ∃ (i : ℕ), ∀ j ≥ i, |(↑(c - CauSeq.const abs c.lim) : ℕ → ℝ) j| < ε
⊢ ∃ (a : ℕ), ∀ b ≥ a, b ∈ u ⁻¹' s

Tactic:
exact this.imp fun N hN n hn => hε (hN n hn)

Premises used: Exists.imp
-- Module: Mathlib.Topology.UniformSpace.Real
Goal:
⊢ CompleteSpace ℝ≥0

Tactic:
isClosed_Ici.completeSpace_coe

Premises used: Set.Ici, Set.Mem, NNReal, IsClosed.completeSpace_coe
-- Module: Mathlib.Topology.UniformSpace.Real
Goal:
⊢ Continuous toReal

Tactic:
continuous_subtype_val

Premises used: continuous_subtype_val, NNReal, NNReal.toReal
-- Module: Mathlib.Topology.UniformSpace.Real
Goal:
⊢ Eq (α := ℝ) ((ContinuousMap.coeNNRealReal : (a : ℝ≥0) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
⊢ RegularSpace α

Tactic:
.of_hasBasis
    (fun _ ↦ nhds_basis_uniformity' uniformity_hasBasis_closed)
    fun a _V hV ↦ isClosed_ball a hV.2

Premises used: uniformity_hasBasis_closed, nhds_basis_uniformity', RegularSpace.of_hasBasis, And.right, UniformSpace.isClosed_ball
-- 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
b : Bool
x : (↑(S b) : Type u)
⊢ Disjoint (S b) (closure[inst.toTopologicalSpace] (S !b))

Tactic:
have hST : Disjoint (S b) (closure (S !b)) := b.casesOn (false := hsT) (true := hSt.symm)
-- 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
b : Bool
x : (↑(S b) : Type u)
hST : Disjoint (S b) (closure[inst.toTopologicalSpace] (S !b))
⊢ (S !b)ᶜ ∈ 𝓝ˢ (S b)

Tactic:
rw [← disjoint_nhdsSet_principal, disjoint_principal_right] at hST

Premises used: disjoint_nhdsSet_principal, Filter.disjoint_principal_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
b : Bool
x : (↑(S b) : Type u)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
obtain :
  ∀ (U : Set (α × α)) (hUu : U ∈ 𝓤 α) (hU : ball (↑x : α) U ⊆ (S !b)ᶜ),
    ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
⊢ ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)

Tactic:
obtain ⟨U, hUu, hU⟩ := UniformSpace.mem_nhds_iff.1 (nhds_le_nhdsSet x.2 hST)

Premises used: nhds_le_nhdsSet, UniformSpace.mem_nhds_iff, Iff.mp, 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
b : Bool
x : (↑(S b) : Type u)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x : α) U ⊆ (S !b)ᶜ
obtain :
  ∀ (V : SetRel α α) (hV : V ∈ 𝓤 α) (hVs : V.IsSymm) (hVU : V.comp V ⊆ U),
    ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
⊢ ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)

Tactic:
obtain ⟨(V : SetRel α α), hV, hVs, hVU⟩ := comp_symm_mem_uniformity_sets hUu

Premises used: SetRel, comp_symm_mem_uniformity_sets
-- 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
b : Bool
x : (↑(S b) : Type u)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x : α) U ⊆ (S !b)ᶜ
V : SetRel α α
hV : V ∈ 𝓤 α
hVs : V.IsSymm
hVU : V.comp V ⊆ U
obtain : ∀ (i : ι) (hi : B i ⊆ V), ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
⊢ ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)

Tactic:
obtain ⟨i, hi⟩ := hB.mem_iff.1 hV

Premises used: Filter.HasAntitoneBasis.mem_iff, Iff.mp
-- 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
b : Bool
x : (↑(S b) : Type u)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x : α) U ⊆ (S !b)ᶜ
V : SetRel α α
hV : V ∈ 𝓤 α
hVs : V.IsSymm
hVU : V.comp V ⊆ U
i : ι
hi : B i ⊆ V
⊢ ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)

Tactic:
⟨i, subset_compl_iff_disjoint_right.1 (subset_trans (ball_mono ?_ x.1) hU)⟩

Premises used: Set.subset_compl_iff_disjoint_right, subset_trans, UniformSpace.ball_mono, Exists.intro, Iff.mp, Subtype.val
-- 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
b : Bool
x : (↑(S b) : Type u)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x : α) U ⊆ (S !b)ᶜ
V : SetRel α α
hV : V ∈ 𝓤 α
hVs : V.IsSymm
hVU : V.comp V ⊆ U
i : ι
hi : B i ⊆ V
refine : (B i).comp (B i).inv ⊆ U
⊢ ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)

Tactic:
refine ⟨i, subset_compl_iff_disjoint_right.1 (subset_trans (ball_mono ?_ x.1) hU)⟩
-- 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
b : Bool
x : (↑(S b) : Type u)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x : α) U ⊆ (S !b)ᶜ
V : SetRel α α
hV : V ∈ 𝓤 α
hVs : V.IsSymm
hVU : V.comp V ⊆ U
i : ι
hi : B i ⊆ V
⊢ (B i).comp (B i).inv ⊆ U

Tactic:
subset_trans (SetRel.comp_subset_comp hi (V.inv_eq_self ▸ (SetRel.inv_mono hi))) hVU

Premises used: SetRel.comp_subset_comp, subset_trans
-- 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
b : Bool
x : (↑(S b) : Type u)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x : α) U ⊆ (S !b)ᶜ
V : SetRel α α
hV : V ∈ 𝓤 α
hVs : V.IsSymm
hVU : V.comp V ⊆ U
i : ι
hi : B i ⊆ V
⊢ (B i).comp (B i).inv ⊆ U

Tactic:
exact subset_trans (SetRel.comp_subset_comp hi (V.inv_eq_self ▸ (SetRel.inv_mono hi))) hVU

Premises used: SetRel.comp_subset_comp, subset_trans
-- 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
⊢ ∀ (b : Bool) (x : (↑(S b) : Type u)), ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)

Tactic:
have hx (b : Bool) (x : S b) : ∃ i, Disjoint (ball x.1 ((B i).comp (B i).inv)) (S (!b)) := by
      have hST : Disjoint (S b) (closure (S !b)) := b.casesOn (false := hsT) (true := hSt.symm)
      rw [← disjoint_nhdsSet_principal, disjoint_principal_right] at hST
      obtain ⟨U, hUu, hU⟩ := UniformSpace.mem_nhds_iff.1 (nhds_le_nhdsSet x.2 hST)
      obtain ⟨(V : SetRel α α), hV, hVs, hVU⟩ := comp_symm_mem_uniformity_sets hUu
      obtain ⟨i, hi⟩ := hB.mem_iff.1 hV
      refine ⟨i, subset_compl_iff_disjoint_right.1 (subset_trans (ball_mono ?_ x.1) hU)⟩
      exact subset_trans (SetRel.comp_subset_comp hi (V.inv_eq_self ▸ (SetRel.inv_mono hi))) hVU
-- 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
hx : ∀ (b : Bool) (x : (↑(S b) : Type u)), ∃ (i : ι), Disjoint (ball (↑x : α) ((B i).comp (B i).inv)) (S !b)
choose :
  ∀ (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)),
    Disjoint (𝓝ˢ s) (𝓝ˢ t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
choose U hU using 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)
b : Bool
rw : ∀ x ∈ S b, ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝 x
⊢ ⋃ (x : (↑(S b) : Type u)), ball (↑x : α) (B (U b x)) ∈ 𝓝ˢ (S b)

Tactic:
rw [mem_nhdsSet_iff_forall]

Premises used: mem_nhdsSet_iff_forall