[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
⊢ 𝓝ˢ (diagonal α) = 𝓤 α
[PROOFSTEP]
refine' nhdsSet_diagonal_le_uniformity.antisymm _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)
[PROOFSTEP]
have :
  (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U =>
    (fun p : (α × α) × α × α => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U :=
  by
  rw [uniformity_prod_eq_comap_prod]
  exact (𝓤 α).basis_sets.prod_self.comap _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
⊢ HasBasis (𝓤 (α × α)) (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U
[PROOFSTEP]
rw [uniformity_prod_eq_comap_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
⊢ HasBasis (Filter.comap (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) (𝓤 α ×ˢ 𝓤 α)) (fun U => U ∈ 𝓤 α)
    fun U => (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U
[PROOFSTEP]
exact (𝓤 α).basis_sets.prod_self.comap _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
this :
  HasBasis (𝓤 (α × α)) (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)
[PROOFSTEP]
refine' (isCompact_diagonal.nhdsSet_basis_uniformity this).ge_iff.2 fun U hU => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
this :
  HasBasis (𝓤 (α × α)) (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ⋃ (x : α × α) (_ : x ∈ diagonal α), ball x ((fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U) ∈
    𝓤 α
[PROOFSTEP]
exact mem_of_superset hU fun ⟨x, y⟩ hxy => mem_iUnion₂.2 ⟨(x, x), rfl, refl_mem_uniformity hU, hxy⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
⊢ u = u'
[PROOFSTEP]
refine uniformSpace_eq ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
⊢ 𝓤 γ = 𝓤 γ
[PROOFSTEP]
have : @CompactSpace γ u.toTopologicalSpace := by rwa [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
⊢ CompactSpace γ
[PROOFSTEP]
rwa [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this : CompactSpace γ
⊢ 𝓤 γ = 𝓤 γ
[PROOFSTEP]
have : @CompactSpace γ u'.toTopologicalSpace := by rwa [h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this : CompactSpace γ
⊢ CompactSpace γ
[PROOFSTEP]
rwa [h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this✝ : CompactSpace γ
this : CompactSpace γ
⊢ 𝓤 γ = 𝓤 γ
[PROOFSTEP]
rw [@compactSpace_uniformity _ u, compactSpace_uniformity, h, h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
⊢ (Filter.lift' (𝓝ˢ (diagonal γ)) fun s => s ○ s) ≤ 𝓝ˢ (diagonal γ)
[PROOFSTEP]
set 𝓝Δ :=
  𝓝ˢ
    (diagonal γ)
      -- The filter of neighborhoods of Δ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
⊢ (Filter.lift' 𝓝Δ fun s => s ○ s) ≤ 𝓝Δ
[PROOFSTEP]
set F := 𝓝Δ.lift' fun s : Set (γ × γ) => s ○ s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
⊢ F ≤ 𝓝Δ
[PROOFSTEP]
rw [le_iff_forall_inf_principal_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
⊢ ∀ (V : Set (γ × γ)), V ∈ 𝓝Δ → F ⊓ 𝓟 Vᶜ = ⊥
[PROOFSTEP]
intro V V_in
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
⊢ F ⊓ 𝓟 Vᶜ = ⊥
[PROOFSTEP]
by_contra H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
⊢ False
[PROOFSTEP]
haveI : NeBot (F ⊓ 𝓟 Vᶜ) :=
  ⟨H⟩
    -- Hence compactness would give us a cluster point (x, y) for F ⊓ 𝓟 Vᶜ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : NeBot (F ⊓ 𝓟 Vᶜ)
⊢ False
[PROOFSTEP]
obtain ⟨⟨x, y⟩, hxy⟩ : ∃ p : γ × γ, ClusterPt p (F ⊓ 𝓟 Vᶜ) :=
  cluster_point_of_compact
    _
      -- In particular (x, y) is a cluster point of 𝓟 Vᶜ, hence is not in the interior of V,
          -- and a fortiori not in Δ, so x ≠ y
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
⊢ False
[PROOFSTEP]
have clV : ClusterPt (x, y) (𝓟 <| Vᶜ) := hxy.of_inf_right
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
⊢ False
[PROOFSTEP]
have : (x, y) ∉ interior V :=
  by
  have : (x, y) ∈ closure Vᶜ := by rwa [mem_closure_iff_clusterPt]
  rwa [closure_compl] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
⊢ ¬(x, y) ∈ interior V
[PROOFSTEP]
have : (x, y) ∈ closure Vᶜ := by rwa [mem_closure_iff_clusterPt]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
⊢ (x, y) ∈ closure Vᶜ
[PROOFSTEP]
rwa [mem_closure_iff_clusterPt]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this : (x, y) ∈ closure Vᶜ
⊢ ¬(x, y) ∈ interior V
[PROOFSTEP]
rwa [closure_compl] at this 
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this : ¬(x, y) ∈ interior V
⊢ False
[PROOFSTEP]
have diag_subset : diagonal γ ⊆ interior V := subset_interior_iff_mem_nhdsSet.2 V_in
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
⊢ False
[PROOFSTEP]
have x_ne_y : x ≠ y := mt (@diag_subset (x, y)) this
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
⊢ False
[PROOFSTEP]
haveI : NormalSpace γ := normalOfCompactT2
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝¹ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this : NormalSpace γ
⊢ False
[PROOFSTEP]
obtain ⟨U₁, _, V₁, V₁_in, U₂, _, V₂, V₂_in, V₁_cl, V₂_cl, U₁_op, U₂_op, VU₁, VU₂, hU₁₂⟩ := disjoint_nested_nhds x_ne_y
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝¹ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
⊢ False
[PROOFSTEP]
let U₃ := (V₁ ∪ V₂)ᶜ
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝¹ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
⊢ False
[PROOFSTEP]
have U₃_op : IsOpen U₃ := (V₁_cl.union V₂_cl).isOpen_compl
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝¹ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
⊢ False
[PROOFSTEP]
let W := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝¹ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
⊢ False
[PROOFSTEP]
have W_in : W ∈ 𝓝Δ := by
  rw [mem_nhdsSet_iff_forall]
  rintro ⟨z, z'⟩ (rfl : z = z')
  refine' IsOpen.mem_nhds _ _
  · apply_rules [IsOpen.union, IsOpen.prod]
  · simp only [mem_union, mem_prod, and_self_iff]
    exact (_root_.em _).imp_left fun h => union_subset_union VU₁ VU₂ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝¹ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
⊢ W ∈ 𝓝Δ
[PROOFSTEP]
rw [mem_nhdsSet_iff_forall]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝¹ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
⊢ ∀ (x : γ × γ), x ∈ diagonal γ → W ∈ 𝓝 x
[PROOFSTEP]
rintro ⟨z, z'⟩ (rfl : z = z')
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝¹ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
z : γ
⊢ W ∈ 𝓝 (z, z)
[PROOFSTEP]
refine' IsOpen.mem_nhds _ _
[GOAL]
case mk.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝¹ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
z : γ
⊢ IsOpen W
[PROOFSTEP]
apply_rules [IsOpen.union, IsOpen.prod]
[GOAL]
case mk.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝¹ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
z : γ
⊢ (z, z) ∈ W
[PROOFSTEP]
simp only [mem_union, mem_prod, and_self_iff]
[GOAL]
case mk.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝¹ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
z : γ
⊢ (z ∈ U₁ ∨ z ∈ U₂) ∨ z ∈ (V₁ ∪ V₂)ᶜ
[PROOFSTEP]
exact (_root_.em _).imp_left fun h => union_subset_union VU₁ VU₂ h
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝¹ : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
W_in : W ∈ 𝓝Δ
⊢ False
[PROOFSTEP]
have : W ○ W ∈ F := @mem_lift' _ _ _ (fun s => s ○ s) _ W_in
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝² : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝¹ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this✝ : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
W_in : W ∈ 𝓝Δ
this : W ○ W ∈ F
⊢ False
[PROOFSTEP]
have hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y) := prod_mem_nhds V₁_in V₂_in
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝² : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝¹ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this✝ : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
W_in : W ∈ 𝓝Δ
this : W ○ W ∈ F
hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y)
⊢ False
[PROOFSTEP]
obtain ⟨⟨u, v⟩, ⟨u_in, v_in⟩, w, huw, hwv⟩ := clusterPt_iff.mp hxy.of_inf_left hV₁₂ this
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝² : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝¹ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this✝ : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
W_in : W ∈ 𝓝Δ
this : W ○ W ∈ F
hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y)
u v : γ
u_in : (u, v).fst ∈ V₁
v_in : (u, v).snd ∈ V₂
w : γ
huw : ((u, v).fst, w) ∈ W
hwv : (w, (u, v).snd) ∈ W
⊢ False
[PROOFSTEP]
have uw_in : (u, w) ∈ U₁ ×ˢ U₁ :=
  (huw.resolve_right fun h => h.1 <| Or.inl u_in).resolve_right fun h =>
    hU₁₂.le_bot
      ⟨VU₁ u_in, h.1⟩
        -- Similarly, because v ∈ V₂, (w ,v) ∈ W forces (w, v) ∈ U₂ ×ˢ U₂.
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝² : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝¹ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this✝ : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
W_in : W ∈ 𝓝Δ
this : W ○ W ∈ F
hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y)
u v : γ
u_in : (u, v).fst ∈ V₁
v_in : (u, v).snd ∈ V₂
w : γ
huw : ((u, v).fst, w) ∈ W
hwv : (w, (u, v).snd) ∈ W
uw_in : (u, w) ∈ U₁ ×ˢ U₁
⊢ False
[PROOFSTEP]
have wv_in : (w, v) ∈ U₂ ×ˢ U₂ :=
  (hwv.resolve_right fun h => h.2 <| Or.inr v_in).resolve_left fun h =>
    hU₁₂.le_bot
      ⟨h.2, VU₂ v_in⟩
        -- Hence w ∈ U₁ ∩ U₂ which is empty.
            -- So we have a contradiction
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := Filter.lift' 𝓝Δ fun s => s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this✝² : NeBot (F ⊓ 𝓟 Vᶜ)
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
this✝¹ : ¬(x, y) ∈ interior V
diag_subset : diagonal γ ⊆ interior V
x_ne_y : x ≠ y
this✝ : NormalSpace γ
U₁ : Set γ
left✝¹ : U₁ ∈ 𝓝 x
V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ : Set γ
left✝ : U₂ ∈ 𝓝 y
V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed V₁
V₂_cl : IsClosed V₂
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
W_in : W ∈ 𝓝Δ
this : W ○ W ∈ F
hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y)
u v : γ
u_in : (u, v).fst ∈ V₁
v_in : (u, v).snd ∈ V₂
w : γ
huw : ((u, v).fst, w) ∈ W
hwv : (w, (u, v).snd) ∈ W
uw_in : (u, w) ∈ U₁ ×ˢ U₁
wv_in : (w, v) ∈ U₂ ×ˢ U₂
⊢ False
[PROOFSTEP]
exact hU₁₂.le_bot ⟨uw_in.2, wv_in.1⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
⊢ ∀ (s : Set γ),
    IsOpen s ↔
      ∀ (x : γ),
        x ∈ s →
          {p | p.fst = x → p.snd ∈ s} ∈
            { uniformity := 𝓝ˢ (diagonal γ), refl := (_ : 𝓟 idRel ≤ 𝓝ˢ idRel),
                symm := (_ : Tendsto Prod.swap (𝓝ˢ (diagonal γ)) (𝓝ˢ (diagonal γ))),
                comp := (_ : (Filter.lift' (𝓝ˢ (diagonal γ)) fun s => s ○ s) ≤ 𝓝ˢ (diagonal γ)) }.uniformity
[PROOFSTEP]
suffices ∀ x : γ, Filter.comap (Prod.mk x) (𝓝ˢ (diagonal γ)) = 𝓝 x
  by
  intro s
  simp_rw [isOpen_iff_mem_nhds, ← mem_comap_prod_mk, this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
this : ∀ (x : γ), Filter.comap (Prod.mk x) (𝓝ˢ (diagonal γ)) = 𝓝 x
⊢ ∀ (s : Set γ),
    IsOpen s ↔
      ∀ (x : γ),
        x ∈ s →
          {p | p.fst = x → p.snd ∈ s} ∈
            { uniformity := 𝓝ˢ (diagonal γ), refl := (_ : 𝓟 idRel ≤ 𝓝ˢ idRel),
                symm := (_ : Tendsto Prod.swap (𝓝ˢ (diagonal γ)) (𝓝ˢ (diagonal γ))),
                comp := (_ : (Filter.lift' (𝓝ˢ (diagonal γ)) fun s => s ○ s) ≤ 𝓝ˢ (diagonal γ)) }.uniformity
[PROOFSTEP]
intro s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
this : ∀ (x : γ), Filter.comap (Prod.mk x) (𝓝ˢ (diagonal γ)) = 𝓝 x
s : Set γ
⊢ IsOpen s ↔
    ∀ (x : γ),
      x ∈ s →
        {p | p.fst = x → p.snd ∈ s} ∈
          { uniformity := 𝓝ˢ (diagonal γ), refl := (_ : 𝓟 idRel ≤ 𝓝ˢ idRel),
              symm := (_ : Tendsto Prod.swap (𝓝ˢ (diagonal γ)) (𝓝ˢ (diagonal γ))),
              comp := (_ : (Filter.lift' (𝓝ˢ (diagonal γ)) fun s => s ○ s) ≤ 𝓝ˢ (diagonal γ)) }.uniformity
[PROOFSTEP]
simp_rw [isOpen_iff_mem_nhds, ← mem_comap_prod_mk, this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
⊢ ∀ (x : γ), Filter.comap (Prod.mk x) (𝓝ˢ (diagonal γ)) = 𝓝 x
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
x : γ
⊢ Filter.comap (Prod.mk x) (𝓝ˢ (diagonal γ)) = 𝓝 x
[PROOFSTEP]
simp_rw [nhdsSet_diagonal, comap_iSup, nhds_prod_eq, comap_prod, (· ∘ ·), comap_id']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
x : γ
⊢ ⨆ (i : γ), Filter.comap (fun x_1 => x) (𝓝 i) ⊓ 𝓝 i = 𝓝 x
[PROOFSTEP]
rw [iSup_split_single _ x, comap_const_of_mem fun V => mem_of_mem_nhds]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
x : γ
⊢ ⊤ ⊓ 𝓝 x ⊔ ⨆ (i : γ) (_ : i ≠ x), Filter.comap (fun x_2 => x) (𝓝 i) ⊓ 𝓝 i = 𝓝 x
[PROOFSTEP]
suffices ∀ (y) (_ : y ≠ x), comap (fun _ : γ => x) (𝓝 y) ⊓ 𝓝 y ≤ 𝓝 x by simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
x : γ
this : ∀ (y : γ), y ≠ x → Filter.comap (fun x_2 => x) (𝓝 y) ⊓ 𝓝 y ≤ 𝓝 x
⊢ ⊤ ⊓ 𝓝 x ⊔ ⨆ (i : γ) (_ : i ≠ x), Filter.comap (fun x_2 => x) (𝓝 i) ⊓ 𝓝 i = 𝓝 x
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
x : γ
⊢ ∀ (y : γ), y ≠ x → Filter.comap (fun x_2 => x) (𝓝 y) ⊓ 𝓝 y ≤ 𝓝 x
[PROOFSTEP]
intro y hxy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : T2Space γ
x y : γ
hxy : y ≠ x
⊢ Filter.comap (fun x_1 => x) (𝓝 y) ⊓ 𝓝 y ≤ 𝓝 x
[PROOFSTEP]
simp [comap_const_of_not_mem (compl_singleton_mem_nhds hxy) (Classical.not_not.2 rfl)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
f : α → β
h : Continuous f
⊢ map (Prod.map f f) (𝓤 α) = map (Prod.map f f) (𝓝ˢ (diagonal α))
[PROOFSTEP]
rw [nhdsSet_diagonal_eq_uniformity]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ UniformContinuousOn f s
[PROOFSTEP]
rw [uniformContinuousOn_iff_restrict]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ UniformContinuous (restrict s f)
[PROOFSTEP]
rw [isCompact_iff_compactSpace] at hs 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : ContinuousOn f s
⊢ UniformContinuous (restrict s f)
[PROOFSTEP]
rw [continuousOn_iff_continuous_restrict] at hf 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : Continuous (restrict s f)
⊢ UniformContinuous (restrict s f)
[PROOFSTEP]
exact CompactSpace.uniformContinuous_of_continuous hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
⊢ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
[PROOFSTEP]
obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
⊢ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
[PROOFSTEP]
choose U hU T hT hb using fun a ha =>
  exists_mem_nhds_ball_subset_of_mem_nhds ((hf a ha).preimage_mem_nhds <| mem_nhds_left _ ht)
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
⊢ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
[PROOFSTEP]
obtain ⟨fs, hsU⟩ := hs.elim_nhds_subcover' U hU
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
⊢ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
[PROOFSTEP]
apply mem_of_superset ((biInter_finset_mem fs).2 fun a _ => hT a a.2)
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
⊢ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s) ⊆ {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ r}
[PROOFSTEP]
rintro ⟨a₁, a₂⟩ h h₁
[GOAL]
case intro.intro.intro.intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
⊢ (f (a₁, a₂).fst, f (a₁, a₂).snd) ∈ r
[PROOFSTEP]
obtain ⟨a, ha, haU⟩ := Set.mem_iUnion₂.1 (hsU h₁)
[GOAL]
case intro.intro.intro.intro.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).fst ∈ U ↑a (_ : ↑a ∈ s)
⊢ (f (a₁, a₂).fst, f (a₁, a₂).snd) ∈ r
[PROOFSTEP]
apply htr
[GOAL]
case intro.intro.intro.intro.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).fst ∈ U ↑a (_ : ↑a ∈ s)
⊢ (f (a₁, a₂).fst, f (a₁, a₂).snd) ∈ t ○ t
[PROOFSTEP]
refine' ⟨f a, htsymm.mk_mem_comm.1 (hb _ _ _ haU _), hb _ _ _ haU _⟩
[GOAL]
case intro.intro.intro.intro.mk.intro.intro.a.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).fst ∈ U ↑a (_ : ↑a ∈ s)
⊢ (a₁, a₂).fst ∈ ball (a₁, a₂).fst (T ↑a (_ : ↑a ∈ s))
case intro.intro.intro.intro.mk.intro.intro.a.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ (a : α), a ∈ s → ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s) (a' : α), a' ∈ U a ha → ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ (x : ↑s) (_ : x ∈ fs), U ↑x (_ : ↑x ∈ s)
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ (i : ↑s) (_ : i ∈ fs), T ↑i (_ : ↑i ∈ s)
h₁ : (a₁, a₂).fst ∈ s
a : ↑s
ha : a ∈ fs
haU : (a₁, a₂).fst ∈ U ↑a (_ : ↑a ∈ s)
⊢ (a₁, a₂).snd ∈ ball (a₁, a₂).fst (T ↑a (_ : ↑a ∈ s))
[PROOFSTEP]
exacts [mem_ball_self _ (hT a a.2), mem_iInter₂.1 h a ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
⊢ {x | (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
[PROOFSTEP]
obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
⊢ {x | (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
[PROOFSTEP]
obtain ⟨s, hs, hst⟩ := mem_cocompact.1 (hx <| mem_nhds_left _ ht)
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
⊢ {x | (f x.fst, f x.snd) ∈ r} ∈ 𝓤 α
[PROOFSTEP]
apply
  mem_of_superset
    (symmetrize_mem_uniformity <|
      (hs.uniformContinuousAt_of_continuousAt f fun _ _ => h_cont.continuousAt) <| symmetrize_mem_uniformity hr)
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
⊢ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r} ⊆ {x | (f x.fst, f x.snd) ∈ r}
[PROOFSTEP]
rintro ⟨b₁, b₂⟩ h
[GOAL]
case intro.intro.intro.intro.intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}
[PROOFSTEP]
by_cases h₁ : b₁ ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : b₁ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}
[PROOFSTEP]
exact (h.1 h₁).1
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : ¬b₁ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}
[PROOFSTEP]
by_cases h₂ : b₂ ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : ¬b₁ ∈ s
h₂ : b₂ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}
[PROOFSTEP]
exact (h.2 h₂).2
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : ¬b₁ ∈ s
h₂ : ¬b₂ ∈ s
⊢ (b₁, b₂) ∈ {x | (f x.fst, f x.snd) ∈ r}
[PROOFSTEP]
apply htr
[GOAL]
case neg.a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.fst ∈ s → (f x.fst, f x.snd) ∈ symmetrizeRel r}
h₁ : ¬b₁ ∈ s
h₂ : ¬b₂ ∈ s
⊢ (f (b₁, b₂).fst, f (b₁, b₂).snd) ∈ t ○ t
[PROOFSTEP]
exact ⟨x, htsymm.mk_mem_comm.1 (hst h₁), hst h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
⊢ Tendsto f (cocompact α) (𝓝 1)
[PROOFSTEP]
intro N hN
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ N ∈ map f (cocompact α)
[PROOFSTEP]
rw [mem_map, mem_cocompact']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ ∃ t, IsCompact t ∧ (f ⁻¹' N)ᶜ ⊆ t
[PROOFSTEP]
refine' ⟨mulTSupport f, h.isCompact, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ (f ⁻¹' N)ᶜ ⊆ mulTSupport f
[PROOFSTEP]
rw [compl_subset_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ (mulTSupport f)ᶜ ⊆ f ⁻¹' N
[PROOFSTEP]
intro v hv
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ (mulTSupport f)ᶜ
⊢ v ∈ f ⁻¹' N
[PROOFSTEP]
rw [mem_preimage, image_eq_one_of_nmem_mulTSupport hv]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ (mulTSupport f)ᶜ
⊢ 1 ∈ N
[PROOFSTEP]
exact mem_of_mem_nhds hN
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
⊢ TendstoUniformly f (f x) (𝓝 x)
[PROOFSTEP]
rcases LocallyCompactSpace.local_compact_nhds _ _ hxU with ⟨K, hxK, hKU, hK⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
⊢ TendstoUniformly f (f x) (𝓝 x)
[PROOFSTEP]
have : UniformContinuousOn (↿f) (K ×ˢ univ) :=
  IsCompact.uniformContinuousOn_of_continuous (hK.prod isCompact_univ) (h.mono <| prod_mono hKU Subset.rfl)
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
this : UniformContinuousOn (↿f) (K ×ˢ univ)
⊢ TendstoUniformly f (f x) (𝓝 x)
[PROOFSTEP]
exact this.tendstoUniformly hxK
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Equicontinuous F
⊢ UniformEquicontinuous F
[PROOFSTEP]
rw [equicontinuous_iff_continuous] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous (↑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformEquicontinuous F
[PROOFSTEP]
rw [uniformEquicontinuous_iff_uniformContinuous]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous (↑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformContinuous (↑UniformFun.ofFun ∘ Function.swap F)
[PROOFSTEP]
exact CompactSpace.uniformContinuous_of_continuous h
