apply sum_le_sum _
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
⊢ ∑ v in C, degRes G v B ≤ ∑ v in C, degRes G v A
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
⊢ ∀ (i : α), i ∈ C → degRes G i B ≤ degRes G i A