no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.88389
inst✝ : UniformSpace α
t : Set (α × α)
⊢ (⋂ (V : Set (α × α)) (_ : V ∈ 𝓤 α), V ○ t ○ V) = ⋂ (V : Set (α × α)) (_ : V ∈ 𝓤 α), V ○ (t ○ V)
simp only [compRel_assoc]