simp only [sum_const, Algebra.id.smul_eq_mul, mul_one, sum_boole, cast_id]
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ ∑ x in nbhdRes G x (A \ B), 1 = ∑ w in A \ B, if Adj G x w then 1 else 0
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ card (nbhdRes G x (A \ B)) = card (filter (fun x_1 => Adj G x x_1) (A \ B))