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

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hv : SymmetricRel v
hvu : v ○ v ⊆ u
hST : thickening u s ∩ t = ∅
⊢ thickening v s ∩ thickening v t = ∅
Tactic:
simp only [←thickening_inter_eq_empty_comm hv, thickening_comp]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hv : SymmetricRel v
hvu : v ○ v ⊆ u
hST : thickening u s ∩ t = ∅
⊢ thickening (v ○ v) s ∩ t = ∅

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hv : SymmetricRel v
hvu : v ○ v ⊆ u
hST : thickening u s ∩ t = ∅
⊢ thickening (v ○ v) s ∩ t = ∅
Tactic:
exact subset_eq_empty (inter_subset_inter_left _ (monotone_thickening hvu)) hST
State after:
no goals