Lean/Mathlib: drop connectedness from a graph bound by summing over components

To go from a bound for connected graphs to all finite graphs (for example E <= 3V-6 for planar graphs), sum degrees over components. Let s c := sum of G.degree v over v in univ.filter (G.connectedComponentMk v = c), and n c := the card of that filter. Finset.sum_fiberwise gives sum_c s c = sum_v deg v = 2E, and Finset.card_eq_sum_card_fiberwise gives sum_c n c = V. Each c gives c.toSimpleGraph = G.induce c.supp, which is connected (connected_toSimpleGraph). Its degrees equal G's: map its neighborFinset along Embedding.subtype and use mem_supp_of_adj_mem_supp. Also s c is the subtype sum (Finset.sum_subtype, using (c.mem_supp_iff v).symm), and n c = Fintype.card c (Fintype.card_subtype then congr 1). Gotcha: if the new theorem has the same name as the connected one, a call inside its own proof resolves to itself. Rename the old one to _of_connected first.