[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a : α
⊢ HasBasis (𝓝 a) (?m.55 a) (?m.56 a)
[PROOFSTEP]
rw [nhds_eq_comap_uniformity]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a : α
⊢ HasBasis (Filter.comap (Prod.mk a) (𝓤 α)) (?m.55 a) (?m.56 a)
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ α → Sort ?u.51
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ (a : α) → ?m.54 a → Prop
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ (a : α) → ?m.54 a → Set α
[PROOFSTEP]
exact uniformity_hasBasis_closed.comap _
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a : α
V : Set (α × α)
hV : V ∈ 𝓤 α ∧ IsClosed V
⊢ IsClosed (Prod.mk a ⁻¹' id V)
[PROOFSTEP]
exact hV.2.preimage <| continuous_const.prod_mk continuous_id
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a b : α
⊢ (a, b) ∈ 𝓢 α ↔ a ⤳ b
[PROOFSTEP]
simp only [(𝓤 α).basis_sets.mem_separationRel, id, mem_setOf_eq,
  (nhds_basis_uniformity (𝓤 α).basis_sets).specializes_iff]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
⊢ SeparatedSpace α ↔ ∀ (x y : α), (∀ (r : Set (α × α)), r ∈ 𝓤 α → (x, y) ∈ r) → x = y
[PROOFSTEP]
simp only [separatedSpace_iff, Set.ext_iff, Prod.forall, mem_idRel, separationRel, mem_sInter]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
⊢ (∀ (a b : α), (∀ (t : Set (α × α)), t ∈ (𝓤 α).sets → (a, b) ∈ t) ↔ a = b) ↔
    ∀ (x y : α), (∀ (r : Set (α × α)), r ∈ 𝓤 α → (x, y) ∈ r) → x = y
[PROOFSTEP]
exact forall₂_congr fun _ _ => ⟨Iff.mp, fun h => ⟨h, fun H U hU => H ▸ refl_mem_uniformity hU⟩⟩
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
x y : α
⊢ (∀ (r : Set (α × α)), r ∈ 𝓤 α → (x, y) ∈ r) → x = y ↔ x ≠ y → ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
[PROOFSTEP]
rw [← not_imp_not]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
x y : α
⊢ (¬x = y → ¬∀ (r : Set (α × α)), r ∈ 𝓤 α → (x, y) ∈ r) ↔ x ≠ y → ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
[PROOFSTEP]
simp [not_forall]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α✝
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
x y : α
h : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SymmetricRel V → (x, y) ∈ V
⊢ ∀ {i : Set (α × α)}, i ∈ 𝓤 α ∧ SymmetricRel i → (x, y) ∈ id i
[PROOFSTEP]
simpa [and_imp]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
⊢ idRel ⊆ 𝓢 α
[PROOFSTEP]
unfold separationRel
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
⊢ idRel ⊆ ⋂₀ (𝓤 α).sets
[PROOFSTEP]
rw [idRel_subset]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
⊢ ∀ (a : α), (a, a) ∈ ⋂₀ (𝓤 α).sets
[PROOFSTEP]
intro x
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
x : α
⊢ (x, x) ∈ ⋂₀ (𝓤 α).sets
[PROOFSTEP]
suffices ∀ t ∈ 𝓤 α, (x, x) ∈ t by simpa only [refl_mem_uniformity]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
x : α
this : ∀ (t : Set (α × α)), t ∈ 𝓤 α → (x, x) ∈ t
⊢ (x, x) ∈ ⋂₀ (𝓤 α).sets
[PROOFSTEP]
simpa only [refl_mem_uniformity]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
x : α
⊢ ∀ (t : Set (α × α)), t ∈ 𝓤 α → (x, x) ∈ t
[PROOFSTEP]
exact fun t => refl_mem_uniformity
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : inst✝² = UniformSpace.comap f inst✝¹
⊢ 𝓢 α = Prod.map f f ⁻¹' 𝓢 β
[PROOFSTEP]
subst h
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ 𝓢 α = Prod.map f f ⁻¹' 𝓢 β
[PROOFSTEP]
dsimp [separationRel]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ ⋂₀ (𝓤 α).sets = Prod.map f f ⁻¹' ⋂₀ (𝓤 β).sets
[PROOFSTEP]
simp_rw [uniformity_comap, (Filter.comap_hasBasis (Prod.map f f) (𝓤 β)).sInter_sets, ← preimage_iInter,
  sInter_eq_biInter]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ Prod.map f f ⁻¹' ⋂ (i : Set (β × β)) (_ : i ∈ 𝓤 β), i = Prod.map f f ⁻¹' ⋂ (i : Set (β × β)) (_ : i ∈ (𝓤 β).sets), i
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
ι : Sort u_1
p : ι → Prop
s : ι → Set (α × α)
h : HasBasis (𝓤 α) p s
⊢ 𝓢 α = ⋂ (i : ι) (_ : p i), s i
[PROOFSTEP]
unfold separationRel
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
ι : Sort u_1
p : ι → Prop
s : ι → Set (α × α)
h : HasBasis (𝓤 α) p s
⊢ ⋂₀ (𝓤 α).sets = ⋂ (i : ι) (_ : p i), s i
[PROOFSTEP]
rw [h.sInter_sets]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ 𝓢 α = ⋂₀ (closure '' (𝓤 α).sets)
[PROOFSTEP]
simp [uniformity_hasBasis_closure.separationRel]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ IsClosed (𝓢 α)
[PROOFSTEP]
rw [separationRel_eq_inter_closure]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ IsClosed (⋂₀ (closure '' (𝓤 α).sets))
[PROOFSTEP]
apply isClosed_sInter
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ ∀ (t : Set (α × α)), t ∈ closure '' (𝓤 α).sets → IsClosed t
[PROOFSTEP]
rintro _ ⟨t, -, rfl⟩
[GOAL]
case a.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
t : Set (α × α)
⊢ IsClosed (closure t)
[PROOFSTEP]
exact isClosed_closure
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ SeparatedSpace α ↔ T2Space α
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ SeparatedSpace α → T2Space α
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ T2Space α → SeparatedSpace α
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : SeparatedSpace α
⊢ T2Space α
[PROOFSTEP]
rw [t2_iff_isClosed_diagonal, ← show 𝓢 α = diagonal α from h.1]
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : SeparatedSpace α
⊢ IsClosed (𝓢 α)
[PROOFSTEP]
exact isClosed_separationRel
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : T2Space α
⊢ SeparatedSpace α
[PROOFSTEP]
rw [separated_def']
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : T2Space α
⊢ ∀ (x y : α), x ≠ y → ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
[PROOFSTEP]
intro x y hxy
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h : T2Space α
x y : α
hxy : x ≠ y
⊢ ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
[PROOFSTEP]
rcases t2_separation hxy with ⟨u, v, uo, -, hx, hy, h⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h✝ : T2Space α
x y : α
hxy : x ≠ y
u v : Set α
uo : IsOpen u
hx : x ∈ u
hy : y ∈ v
h : Disjoint u v
⊢ ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
[PROOFSTEP]
rcases isOpen_iff_ball_subset.1 uo x hx with ⟨r, hrU, hr⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
h✝ : T2Space α
x y : α
hxy : x ≠ y
u v : Set α
uo : IsOpen u
hx : x ∈ u
hy : y ∈ v
h : Disjoint u v
r : Set (α × α)
hrU : r ∈ 𝓤 α
hr : ball x r ⊆ u
⊢ ∃ r, r ∈ 𝓤 α ∧ ¬(x, y) ∈ r
[PROOFSTEP]
exact ⟨r, hrU, fun H => h.le_bot ⟨hr H, hy⟩⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
⊢ IsClosed s
[PROOFSTEP]
rcases comp_symm_mem_uniformity_sets V₀_in with ⟨V₁, V₁_in, V₁_symm, h_comp⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
⊢ IsClosed s
[PROOFSTEP]
apply isClosed_of_closure_subset
[GOAL]
case intro.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
⊢ closure s ⊆ s
[PROOFSTEP]
intro x hx
[GOAL]
case intro.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : x ∈ closure s
⊢ x ∈ s
[PROOFSTEP]
rw [mem_closure_iff_ball] at hx 
[GOAL]
case intro.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
⊢ x ∈ s
[PROOFSTEP]
rcases hx V₁_in with ⟨y, hy, hy'⟩
[GOAL]
case intro.intro.intro.h.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ x ∈ s
[PROOFSTEP]
suffices x = y by rwa [this]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
this : x = y
⊢ x ∈ s
[PROOFSTEP]
rwa [this]
[GOAL]
case intro.intro.intro.h.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ x = y
[PROOFSTEP]
apply eq_of_forall_symmetric
[GOAL]
case intro.intro.intro.h.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SymmetricRel V → (x, y) ∈ V
[PROOFSTEP]
intro V V_in _
[GOAL]
case intro.intro.intro.h.intro.intro.h
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
⊢ (x, y) ∈ V
[PROOFSTEP]
rcases hx (inter_mem V₁_in V_in) with ⟨z, hz, hz'⟩
[GOAL]
case intro.intro.intro.h.intro.intro.h.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
⊢ (x, y) ∈ V
[PROOFSTEP]
obtain rfl : z = y := by
  by_contra hzy
  exact hs hz' hy' hzy (h_comp <| mem_comp_of_mem_ball V₁_symm (ball_inter_left x _ _ hz) hy)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
⊢ z = y
[PROOFSTEP]
by_contra hzy
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
hzy : ¬z = y
⊢ False
[PROOFSTEP]
exact hs hz' hy' hzy (h_comp <| mem_comp_of_mem_ball V₁_symm (ball_inter_left x _ _ hz) hy)
[GOAL]
case intro.intro.intro.h.intro.intro.h.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : Set.Pairwise s fun x y => ¬(x, y) ∈ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
hy : z ∈ ball x V₁
hy' : z ∈ s
⊢ (x, z) ∈ V
[PROOFSTEP]
exact ball_inter_right x _ _ hz
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
ι : Type u_1
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
f : ι → α
hf : Pairwise fun x y => ¬(f x, f y) ∈ V₀
⊢ Set.Pairwise (range f) fun x y => ¬(x, y) ∈ V₀
[PROOFSTEP]
rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ h
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
ι : Type u_1
inst✝ : SeparatedSpace α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
f : ι → α
hf : Pairwise fun x y => ¬(f x, f y) ∈ V₀
x y : ι
h : f x ≠ f y
⊢ ¬(f x, f y) ∈ V₀
[PROOFSTEP]
exact hf (ne_of_apply_ne f h)
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
⊢ 𝓟 idRel ≤ map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (𝓟 idRel)
[PROOFSTEP]
simp [Quotient.exists_rep]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
s : Set (Quotient (separationSetoid α) × Quotient (separationSetoid α))
hs : s ∈ map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (𝓤 α)
⊢ s ∈
    Filter.lift' (map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (𝓤 α))
      fun s => s ○ s
[PROOFSTEP]
rcases comp_open_symm_mem_uniformity_sets hs with ⟨U, hU, hUo, -, hUs⟩
[GOAL]
case intro.intro.intro.intro
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
s : Set (Quotient (separationSetoid α) × Quotient (separationSetoid α))
hs : s ∈ map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (𝓤 α)
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen U
hUs : U ○ U ⊆ (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) ⁻¹' s
⊢ s ∈
    Filter.lift' (map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (𝓤 α))
      fun s => s ○ s
[PROOFSTEP]
refine' mem_of_superset (mem_lift' <| image_mem_map hU) ?_
[GOAL]
case intro.intro.intro.intro
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
s : Set (Quotient (separationSetoid α) × Quotient (separationSetoid α))
hs : s ∈ map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (𝓤 α)
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen U
hUs : U ○ U ⊆ (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) ⁻¹' s
⊢ (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) '' U ○
      (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) '' U ⊆
    s
[PROOFSTEP]
simp only [subset_def, Prod.forall, mem_compRel, mem_image, Prod.ext_iff]
[GOAL]
case intro.intro.intro.intro
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
s : Set (Quotient (separationSetoid α) × Quotient (separationSetoid α))
hs : s ∈ map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (𝓤 α)
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen U
hUs : U ○ U ⊆ (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) ⁻¹' s
⊢ ∀ (a b : Quotient (separationSetoid α)),
    (∃ z,
        (∃ x, x ∈ U ∧ Quotient.mk (separationSetoid α) x.fst = a ∧ Quotient.mk (separationSetoid α) x.snd = z) ∧
          ∃ x, x ∈ U ∧ Quotient.mk (separationSetoid α) x.fst = z ∧ Quotient.mk (separationSetoid α) x.snd = b) →
      (a, b) ∈ s
[PROOFSTEP]
rintro _ _ ⟨_, ⟨⟨x, y⟩, hxyU, rfl, rfl⟩, ⟨⟨y', z⟩, hyzU, hy, rfl⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.mk.intro.intro.intro.mk.intro.intro
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
s : Set (Quotient (separationSetoid α) × Quotient (separationSetoid α))
hs : s ∈ map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (𝓤 α)
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen U
hUs : U ○ U ⊆ (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) ⁻¹' s
x y : α
hxyU : (x, y) ∈ U
y' z : α
hyzU : (y', z) ∈ U
hy : Quotient.mk (separationSetoid α) (y', z).fst = Quotient.mk (separationSetoid α) (x, y).snd
⊢ (Quotient.mk (separationSetoid α) (x, y).fst, Quotient.mk (separationSetoid α) (y', z).snd) ∈ s
[PROOFSTEP]
have : y' ⤳ y := separationRel_iff_specializes.1 (Quotient.exact hy)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.mk.intro.intro.intro.mk.intro.intro
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
s : Set (Quotient (separationSetoid α) × Quotient (separationSetoid α))
hs : s ∈ map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (𝓤 α)
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen U
hUs : U ○ U ⊆ (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) ⁻¹' s
x y : α
hxyU : (x, y) ∈ U
y' z : α
hyzU : (y', z) ∈ U
hy : Quotient.mk (separationSetoid α) (y', z).fst = Quotient.mk (separationSetoid α) (x, y).snd
this : y' ⤳ y
⊢ (Quotient.mk (separationSetoid α) (x, y).fst, Quotient.mk (separationSetoid α) (y', z).snd) ∈ s
[PROOFSTEP]
exact @hUs (x, z) ⟨y', this.mem_open (UniformSpace.isOpen_ball _ hUo) hxyU, hyzU⟩
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
s : Set (Quotient (separationSetoid α))
⊢ IsOpen (Quotient.mk' ⁻¹' s) ↔
    ∀ (x : Quotient (separationSetoid α)),
      x ∈ s →
        {p | p.fst = x → p.snd ∈ s} ∈
          {
              uniformity :=
                map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (𝓤 α),
              refl :=
                (_ :
                  𝓟 idRel ≤
                    map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd))
                      (𝓤 α)),
              symm :=
                (_ :
                  Tendsto Prod.swap
                    (map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd))
                      (𝓤 α))
                    (map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd))
                      (𝓤 α))),
              comp :=
                (_ :
                  ∀ (s : Set (Quotient (separationSetoid α) × Quotient (separationSetoid α))),
                    s ∈
                        map (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd))
                          (𝓤 α) →
                      s ∈
                        Filter.lift'
                          (map
                            (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd))
                            (𝓤 α))
                          fun s => s ○ s) }.uniformity
[PROOFSTEP]
simp only [_root_.isOpen_uniformity, forall_quotient_iff, mem_map', mem_setOf_eq]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
s : Set (Quotient (separationSetoid α))
⊢ (∀ (x : α), x ∈ Quotient.mk' ⁻¹' s → {p | p.fst = x → p.snd ∈ Quotient.mk' ⁻¹' s} ∈ 𝓤 α) ↔
    ∀ (a : α),
      Quotient.mk (separationSetoid α) a ∈ s →
        {x |
            Quotient.mk (separationSetoid α) x.fst = Quotient.mk (separationSetoid α) a →
              Quotient.mk (separationSetoid α) x.snd ∈ s} ∈
          𝓤 α
[PROOFSTEP]
refine forall₂_congr fun x _ => ⟨fun h => ?_, fun h => mem_of_superset h ?_⟩
[GOAL]
case refine_1
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
s : Set (Quotient (separationSetoid α))
x : α
x✝ : x ∈ Quotient.mk' ⁻¹' s
h : {p | p.fst = x → p.snd ∈ Quotient.mk' ⁻¹' s} ∈ 𝓤 α
⊢ {x_1 |
      Quotient.mk (separationSetoid α) x_1.fst = Quotient.mk (separationSetoid α) x →
        Quotient.mk (separationSetoid α) x_1.snd ∈ s} ∈
    𝓤 α
[PROOFSTEP]
rcases comp_mem_uniformity_sets h with ⟨t, ht, hts⟩
[GOAL]
case refine_1.intro.intro
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
s : Set (Quotient (separationSetoid α))
x : α
x✝ : x ∈ Quotient.mk' ⁻¹' s
h : {p | p.fst = x → p.snd ∈ Quotient.mk' ⁻¹' s} ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : t ○ t ⊆ {p | p.fst = x → p.snd ∈ Quotient.mk' ⁻¹' s}
⊢ {x_1 |
      Quotient.mk (separationSetoid α) x_1.fst = Quotient.mk (separationSetoid α) x →
        Quotient.mk (separationSetoid α) x_1.snd ∈ s} ∈
    𝓤 α
[PROOFSTEP]
refine mem_of_superset ht fun (y, z) hyz hyx => @hts (x, z) ⟨y, ?_, hyz⟩ rfl
[GOAL]
case refine_1.intro.intro
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
s : Set (Quotient (separationSetoid α))
x : α
x✝¹ : x ∈ Quotient.mk' ⁻¹' s
h : {p | p.fst = x → p.snd ∈ Quotient.mk' ⁻¹' s} ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : t ○ t ⊆ {p | p.fst = x → p.snd ∈ Quotient.mk' ⁻¹' s}
x✝ : α × α
y z : α
hyz : (y, z) ∈ t
hyx : Quotient.mk (separationSetoid α) (y, z).fst = Quotient.mk (separationSetoid α) x
⊢ ((x, z).fst, y) ∈ t
[PROOFSTEP]
exact Quotient.exact hyx.symm _ ht
[GOAL]
case refine_2
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
s : Set (Quotient (separationSetoid α))
x : α
x✝ : x ∈ Quotient.mk' ⁻¹' s
h :
  {x_1 |
      Quotient.mk (separationSetoid α) x_1.fst = Quotient.mk (separationSetoid α) x →
        Quotient.mk (separationSetoid α) x_1.snd ∈ s} ∈
    𝓤 α
⊢ {x_1 |
      Quotient.mk (separationSetoid α) x_1.fst = Quotient.mk (separationSetoid α) x →
        Quotient.mk (separationSetoid α) x_1.snd ∈ s} ⊆
    {p | p.fst = x → p.snd ∈ Quotient.mk' ⁻¹' s}
[PROOFSTEP]
exact fun y hy hyx => hy <| congr_arg _ hyx
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β → γ
h : ∀ (a : α) (c : β) (b : α) (d : β), (a, b) ∈ 𝓢 α → (c, d) ∈ 𝓢 β → f a c = f b d
hf : UniformContinuous fun p => f p.fst p.snd
⊢ UniformContinuous fun p => Quotient.lift₂ f h p.fst p.snd
[PROOFSTEP]
rw [UniformContinuous, uniformity_prod_eq_prod, uniformity_quotient, uniformity_quotient, Filter.prod_map_map_eq,
  Filter.tendsto_map'_iff, Filter.tendsto_map'_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β → γ
h : ∀ (a : α) (c : β) (b : α) (d : β), (a, b) ∈ 𝓢 α → (c, d) ∈ 𝓢 β → f a c = f b d
hf : UniformContinuous fun p => f p.fst p.snd
⊢ Tendsto
    (((fun x => (Quotient.lift₂ f h x.fst.fst x.fst.snd, Quotient.lift₂ f h x.snd.fst x.snd.snd)) ∘ fun p =>
        ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ∘
      fun p =>
      ((Quotient.mk (separationSetoid α) p.fst.fst, Quotient.mk (separationSetoid α) p.fst.snd),
        Quotient.mk (separationSetoid β) p.snd.fst, Quotient.mk (separationSetoid β) p.snd.snd))
    (𝓤 α ×ˢ 𝓤 β) (𝓤 γ)
[PROOFSTEP]
rwa [UniformContinuous, uniformity_prod_eq_prod, Filter.tendsto_map'_iff] at hf 
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
U : Set (α × α)
hU : U ∈ 𝓤 α ∧ IsOpen U
x✝¹ : α × α
x y : α
x✝ :
  (x, y) ∈
    (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) ⁻¹'
      ((fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) '' id U)
x' y' : α
hx' : (x', y') ∈ id U
h :
  (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (x', y') =
    (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (x, y)
⊢ (x, y) ∈ id U
[PROOFSTEP]
simp only [Prod.ext_iff, Quotient.eq] at h 
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
U : Set (α × α)
hU : U ∈ 𝓤 α ∧ IsOpen U
x✝¹ : α × α
x y : α
x✝ :
  (x, y) ∈
    (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) ⁻¹'
      ((fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) '' id U)
x' y' : α
hx' : (x', y') ∈ id U
h : x' ≈ x ∧ y' ≈ y
⊢ (x, y) ∈ id U
[PROOFSTEP]
exact (((separationRel_iff_inseparable.1 h.1).prod (separationRel_iff_inseparable.1 h.2)).mem_open_iff hU.2).1 hx'
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
x✝ : Quotient (separationSetoid α) × Quotient (separationSetoid α)
a✝ b✝ : Quotient (separationSetoid α)
a b : α
h : (Quotient.mk (separationSetoid α) a, Quotient.mk (separationSetoid α) b) ∈ 𝓢 (Quotient (separationSetoid α))
s : Set (α × α)
hs : s ∈ (𝓤 α).sets
this :
  s ∈
    Filter.comap (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd))
      (𝓤 (Quotient (separationSetoid α)))
t : Set (Quotient (separationSetoid α) × Quotient (separationSetoid α))
ht : t ∈ 𝓤 (Quotient (separationSetoid α))
hts : (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) ⁻¹' t ⊆ s
⊢ (a, b) ∈ (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) ⁻¹' t
[PROOFSTEP]
dsimp [preimage]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
x✝ : Quotient (separationSetoid α) × Quotient (separationSetoid α)
a✝ b✝ : Quotient (separationSetoid α)
a b : α
h : (Quotient.mk (separationSetoid α) a, Quotient.mk (separationSetoid α) b) ∈ 𝓢 (Quotient (separationSetoid α))
s : Set (α × α)
hs : s ∈ (𝓤 α).sets
this :
  s ∈
    Filter.comap (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd))
      (𝓤 (Quotient (separationSetoid α)))
t : Set (Quotient (separationSetoid α) × Quotient (separationSetoid α))
ht : t ∈ 𝓤 (Quotient (separationSetoid α))
hts : (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) ⁻¹' t ⊆ s
⊢ (Quotient.mk (separationSetoid α) a, Quotient.mk (separationSetoid α) b) ∈ t
[PROOFSTEP]
exact h t ht
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
x y : α
H : UniformContinuous f
h : x ≈ y
⊢ SeparatedSpace β
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ lift f (Quotient.mk (separationSetoid α) a) = f a
[PROOFSTEP]
rw [lift, dif_pos h]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → f x = f x_1) (Quotient.mk (separationSetoid α) a) = f a
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
⊢ UniformContinuous (lift f)
[PROOFSTEP]
by_cases hf : UniformContinuous f
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (lift f)
[PROOFSTEP]
rw [lift, dif_pos hf]
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → f x = f x_1))
[PROOFSTEP]
exact uniformContinuous_quotient_lift hf
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (lift f)
[PROOFSTEP]
rw [lift, dif_neg hf]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x => f (Nonempty.some (_ : Nonempty α))
[PROOFSTEP]
exact uniformContinuous_of_const fun a _ => rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : UniformContinuous f
a : α
⊢ map f (Quotient.mk (separationSetoid α) a) = Quotient.mk (separationSetoid β) (f a)
[PROOFSTEP]
rw [map, lift_mk (uniformContinuous_quotient_mk'.comp h)]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : UniformContinuous f
a : α
⊢ (Quotient.mk' ∘ f) a = Quotient.mk (separationSetoid β) (f a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : Quotient.mk (separationSetoid β) ∘ f = g ∘ Quotient.mk (separationSetoid α)
⊢ map f = g
[PROOFSTEP]
ext ⟨a⟩
[GOAL]
case h.mk
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : Quotient.mk (separationSetoid β) ∘ f = g ∘ Quotient.mk (separationSetoid α)
x✝ : SeparationQuotient α
a : α
⊢ map f (Quot.mk Setoid.r a) = g (Quot.mk Setoid.r a)
[PROOFSTEP]
calc
  map f ⟦a⟧ = ⟦f a⟧ := map_mk hf a
  _ = g ⟦a⟧ := congr_fun comm a
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
⊢ Quotient.mk (separationSetoid γ) ∘ g ∘ f = (map g ∘ map f) ∘ Quotient.mk (separationSetoid α)
[PROOFSTEP]
simp only [Function.comp, map_mk, hf, hg]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ≈ (a₂, b₂) ↔ a₁ ≈ a₂ ∧ b₁ ≈ b₂
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ≈ (a₂, b₂) → a₁ ≈ a₂ ∧ b₁ ≈ b₂
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a₁ a₂ : α
b₁ b₂ : β
h : (a₁, b₁) ≈ (a₂, b₂)
⊢ a₁ ≈ a₂ ∧ b₁ ≈ b₂
[PROOFSTEP]
exact ⟨separated_of_uniformContinuous uniformContinuous_fst h, separated_of_uniformContinuous uniformContinuous_snd h⟩
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a₁ a₂ : α
b₁ b₂ : β
⊢ a₁ ≈ a₂ ∧ b₁ ≈ b₂ → (a₁, b₁) ≈ (a₂, b₂)
[PROOFSTEP]
rintro ⟨eqv_α, eqv_β⟩ r r_in
[GOAL]
case mpr.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a₁ a₂ : α
b₁ b₂ : β
eqv_α : a₁ ≈ a₂
eqv_β : b₁ ≈ b₂
r : Set ((α × β) × α × β)
r_in : r ∈ (𝓤 (α × β)).sets
⊢ ((a₁, b₁), a₂, b₂) ∈ r
[PROOFSTEP]
rw [uniformity_prod] at r_in 
[GOAL]
case mpr.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a₁ a₂ : α
b₁ b₂ : β
eqv_α : a₁ ≈ a₂
eqv_β : b₁ ≈ b₂
r : Set ((α × β) × α × β)
r_in :
  r ∈ (Filter.comap (fun p => (p.fst.fst, p.snd.fst)) (𝓤 α) ⊓ Filter.comap (fun p => (p.fst.snd, p.snd.snd)) (𝓤 β)).sets
⊢ ((a₁, b₁), a₂, b₂) ∈ r
[PROOFSTEP]
rcases r_in with ⟨t_α, ⟨r_α, r_α_in, h_α⟩, t_β, ⟨r_β, r_β_in, h_β⟩, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a₁ a₂ : α
b₁ b₂ : β
eqv_α : a₁ ≈ a₂
eqv_β : b₁ ≈ b₂
t_α : Set ((α × β) × α × β)
r_α : Set (α × α)
r_α_in : r_α ∈ 𝓤 α
h_α : (fun p => (p.fst.fst, p.snd.fst)) ⁻¹' r_α ⊆ t_α
t_β : Set ((α × β) × α × β)
r_β : Set (β × β)
r_β_in : r_β ∈ 𝓤 β
h_β : (fun p => (p.fst.snd, p.snd.snd)) ⁻¹' r_β ⊆ t_β
⊢ ((a₁, b₁), a₂, b₂) ∈ t_α ∩ t_β
[PROOFSTEP]
let p_α := fun p : (α × β) × α × β => (p.1.1, p.2.1)
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a₁ a₂ : α
b₁ b₂ : β
eqv_α : a₁ ≈ a₂
eqv_β : b₁ ≈ b₂
t_α : Set ((α × β) × α × β)
r_α : Set (α × α)
r_α_in : r_α ∈ 𝓤 α
h_α : (fun p => (p.fst.fst, p.snd.fst)) ⁻¹' r_α ⊆ t_α
t_β : Set ((α × β) × α × β)
r_β : Set (β × β)
r_β_in : r_β ∈ 𝓤 β
h_β : (fun p => (p.fst.snd, p.snd.snd)) ⁻¹' r_β ⊆ t_β
p_α : (α × β) × α × β → α × α := fun p => (p.fst.fst, p.snd.fst)
⊢ ((a₁, b₁), a₂, b₂) ∈ t_α ∩ t_β
[PROOFSTEP]
let p_β := fun p : (α × β) × α × β => (p.1.2, p.2.2)
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a₁ a₂ : α
b₁ b₂ : β
eqv_α : a₁ ≈ a₂
eqv_β : b₁ ≈ b₂
t_α : Set ((α × β) × α × β)
r_α : Set (α × α)
r_α_in : r_α ∈ 𝓤 α
h_α : (fun p => (p.fst.fst, p.snd.fst)) ⁻¹' r_α ⊆ t_α
t_β : Set ((α × β) × α × β)
r_β : Set (β × β)
r_β_in : r_β ∈ 𝓤 β
h_β : (fun p => (p.fst.snd, p.snd.snd)) ⁻¹' r_β ⊆ t_β
p_α : (α × β) × α × β → α × α := fun p => (p.fst.fst, p.snd.fst)
p_β : (α × β) × α × β → β × β := fun p => (p.fst.snd, p.snd.snd)
⊢ ((a₁, b₁), a₂, b₂) ∈ t_α ∩ t_β
[PROOFSTEP]
have key_α : p_α ((a₁, b₁), (a₂, b₂)) ∈ r_α := by simp [eqv_α r_α r_α_in]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a₁ a₂ : α
b₁ b₂ : β
eqv_α : a₁ ≈ a₂
eqv_β : b₁ ≈ b₂
t_α : Set ((α × β) × α × β)
r_α : Set (α × α)
r_α_in : r_α ∈ 𝓤 α
h_α : (fun p => (p.fst.fst, p.snd.fst)) ⁻¹' r_α ⊆ t_α
t_β : Set ((α × β) × α × β)
r_β : Set (β × β)
r_β_in : r_β ∈ 𝓤 β
h_β : (fun p => (p.fst.snd, p.snd.snd)) ⁻¹' r_β ⊆ t_β
p_α : (α × β) × α × β → α × α := fun p => (p.fst.fst, p.snd.fst)
p_β : (α × β) × α × β → β × β := fun p => (p.fst.snd, p.snd.snd)
⊢ p_α ((a₁, b₁), a₂, b₂) ∈ r_α
[PROOFSTEP]
simp [eqv_α r_α r_α_in]
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a₁ a₂ : α
b₁ b₂ : β
eqv_α : a₁ ≈ a₂
eqv_β : b₁ ≈ b₂
t_α : Set ((α × β) × α × β)
r_α : Set (α × α)
r_α_in : r_α ∈ 𝓤 α
h_α : (fun p => (p.fst.fst, p.snd.fst)) ⁻¹' r_α ⊆ t_α
t_β : Set ((α × β) × α × β)
r_β : Set (β × β)
r_β_in : r_β ∈ 𝓤 β
h_β : (fun p => (p.fst.snd, p.snd.snd)) ⁻¹' r_β ⊆ t_β
p_α : (α × β) × α × β → α × α := fun p => (p.fst.fst, p.snd.fst)
p_β : (α × β) × α × β → β × β := fun p => (p.fst.snd, p.snd.snd)
key_α : p_α ((a₁, b₁), a₂, b₂) ∈ r_α
⊢ ((a₁, b₁), a₂, b₂) ∈ t_α ∩ t_β
[PROOFSTEP]
have key_β : p_β ((a₁, b₁), (a₂, b₂)) ∈ r_β := by simp [eqv_β r_β r_β_in]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a₁ a₂ : α
b₁ b₂ : β
eqv_α : a₁ ≈ a₂
eqv_β : b₁ ≈ b₂
t_α : Set ((α × β) × α × β)
r_α : Set (α × α)
r_α_in : r_α ∈ 𝓤 α
h_α : (fun p => (p.fst.fst, p.snd.fst)) ⁻¹' r_α ⊆ t_α
t_β : Set ((α × β) × α × β)
r_β : Set (β × β)
r_β_in : r_β ∈ 𝓤 β
h_β : (fun p => (p.fst.snd, p.snd.snd)) ⁻¹' r_β ⊆ t_β
p_α : (α × β) × α × β → α × α := fun p => (p.fst.fst, p.snd.fst)
p_β : (α × β) × α × β → β × β := fun p => (p.fst.snd, p.snd.snd)
key_α : p_α ((a₁, b₁), a₂, b₂) ∈ r_α
⊢ p_β ((a₁, b₁), a₂, b₂) ∈ r_β
[PROOFSTEP]
simp [eqv_β r_β r_β_in]
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a₁ a₂ : α
b₁ b₂ : β
eqv_α : a₁ ≈ a₂
eqv_β : b₁ ≈ b₂
t_α : Set ((α × β) × α × β)
r_α : Set (α × α)
r_α_in : r_α ∈ 𝓤 α
h_α : (fun p => (p.fst.fst, p.snd.fst)) ⁻¹' r_α ⊆ t_α
t_β : Set ((α × β) × α × β)
r_β : Set (β × β)
r_β_in : r_β ∈ 𝓤 β
h_β : (fun p => (p.fst.snd, p.snd.snd)) ⁻¹' r_β ⊆ t_β
p_α : (α × β) × α × β → α × α := fun p => (p.fst.fst, p.snd.fst)
p_β : (α × β) × α × β → β × β := fun p => (p.fst.snd, p.snd.snd)
key_α : p_α ((a₁, b₁), a₂, b₂) ∈ r_α
key_β : p_β ((a₁, b₁), a₂, b₂) ∈ r_β
⊢ ((a₁, b₁), a₂, b₂) ∈ t_α ∩ t_β
[PROOFSTEP]
exact ⟨h_α key_α, h_β key_β⟩
