simp_rw [degOn, card_eq_sum_ones, ← sum_indicator_eq_sum_inter]
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s✝ t✝ : Finset α
a : α
s t : Finset α
⊢ ∑ a ∈ s, G.degOn t a = ∑ a ∈ t, G.degOn s a
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s✝ t✝ : Finset α
a : α
s t : Finset α
⊢ ∑ x ∈ s, ∑ i ∈ t, (↑(G.neighborFinset x)).indicator (fun x => 1) i =
    ∑ x ∈ t, ∑ i ∈ s, (↑(G.neighborFinset x)).indicator (fun x => 1) i