Theorem: SimpleGraph.sum_degOn_comm (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Degree.lean)

State before:
α : 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
Tactic:
simp_rw [degOn, card_eq_sum_ones, ← sum_indicator_eq_sum_inter]
State after:
α : 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

State before:
α : 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
Tactic:
rw [sum_comm]
State after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s✝ t✝ : Finset α
a : α
s t : Finset α
⊢ ∑ y ∈ t, ∑ x ∈ s, (↑(G.neighborFinset x)).indicator (fun x => 1) y =
    ∑ x ∈ t, ∑ i ∈ s, (↑(G.neighborFinset x)).indicator (fun x => 1) i

State before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s✝ t✝ : Finset α
a : α
s t : Finset α
⊢ ∑ y ∈ t, ∑ x ∈ s, (↑(G.neighborFinset x)).indicator (fun x => 1) y =
    ∑ x ∈ t, ∑ i ∈ s, (↑(G.neighborFinset x)).indicator (fun x => 1) i
Tactic:
simp [Set.indicator_apply, adj_comm]
State after:
no goals