Sum component deficits to obtain the global edge bound

import Mathlib

set_option autoImplicit false

theorem WilliamsonShmoys.component_bounds_imply_global_planar_edge_bound__p2m_98235c6f_660a_40d6_a6c4_218b22f2584f_a1
    {V : Type} [Fintype V] [LinearOrder V]
    (M : SimpleGraph V) (parts : Finset (Finset V))
    (hcover : ∀ v, ∃ C, C ∈ parts ∧ v ∈ C)
    (hnonempty : ∀ C, C ∈ parts → C.Nonempty)
    (hdisjoint : ∀ C, C ∈ parts → ∀ D, D ∈ parts → C ≠ D → Disjoint C D)
    (hcard : 3 ≤ Fintype.card V)
    (hlocal : ∀ C, C ∈ parts →
      (M.induce (C : Set V)).edgeSet.ncard +
        (if 3 ≤ Fintype.card {x : V // x ∈ C} then 6
         else if Fintype.card {x : V // x ∈ C} = 2 then 5 else 3)
        ≤ 3 * Fintype.card {x : V // x ∈ C})
    (hagg : M.edgeSet.ncard ≤
      ∑ C ∈ parts, (M.induce (C : Set V)).edgeSet.ncard) :
    M.edgeSet.ncard + 6 ≤ 3 * Fintype.card V := by sorry