no goals
R : Type u_2
α : Type u_1
G : SimpleGraph α
inst✝³ : Fintype α
inst✝² : NonAssocSemiring R
a b : α
e : Sym2 α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
⊢ ∑ e : Sym2 α, incMatrix R G a e = ↑(degree G a)
simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset]