Theorem: UniformSpace.uniform_nhds_inf_uniform_nhds_eq_bot (RMT4/uniform.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
h : 𝓝ᵘ s ⊓ 𝓟 t = ⊥
⊢ 𝓝ᵘ s ⊓ 𝓝ᵘ t = ⊥
Tactic:
simp_rw [inf_principal_eq_bot, inf_eq_bot_iff, mem_uniform_nhds_set_iff] at h ⊢
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
h : ∃ u ∈ 𝓤 α, thickening u s ⊆ tᶜ
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
h : ∃ u ∈ 𝓤 α, thickening u s ⊆ tᶜ
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅
Tactic:
obtain ⟨u, hu, hsu⟩ := h
State after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅

State before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅
Tactic:
obtain ⟨v, hv, hvs, hvu⟩ := comp_symm_of_uniformity hu
State after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅

State before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅
Tactic:
refine ⟨_, ⟨v, hv, subset_rfl⟩, _, ⟨v, hv, subset_rfl⟩, ?h⟩
State after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ thickening v s ∩ thickening v t = ∅

State before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ thickening v s ∩ thickening v t = ∅
Tactic:
apply thickening_inter_thickening_eq_empty_of_comp (symmetricRel_of hvs) hvu
State after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ thickening u s ∩ t = ∅

State before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ thickening u s ∩ t = ∅
Tactic:
exact (subset_compl_iff_disjoint_right.mp hsu).inter_eq
State after:
no goals