rw [sum_comm]
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (∑ v in B, ∑ w in A, if Adj G v w then 1 else 0) = ∑ v in A, ∑ w in B, if Adj G v w then 1 else 0
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (∑ y in A, ∑ x in B, if Adj G x y then 1 else 0) = ∑ v in A, ∑ w in B, if Adj G v w then 1 else 0