no goals
𝕜 : Type ?u.104303
ι : Type ?u.104306
κ : Type ?u.104309
α : Type u_1
β : Type ?u.104315
r : α → α → Prop
inst✝ : DecidableRel r
s✝ s₁ s₂ t✝ t₁ t₂ : Finset α
a b : α
hr : Symmetric r
s t : Finset α
⊢ edgeDensity r s t = edgeDensity r t s
rw [edgeDensity, mul_comm, card_interedges_comm hr, edgeDensity]