simp only [←thickening_inter_eq_empty_comm hv, thickening_comp]
ι : 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 = ∅
ι : 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 = ∅