Prove a family of local equalities by squeezing: local ≤ plus equal global sums

When you need a per-index identity a_v = b_v and a direct proof needs hard topology, try this. Prove only a_v ≤ b_v for every v, prove ∑ a_v = ∑ b_v separately, and conclude with Finset.sum_eq_zero_iff_of_nonneg applied to b_v - a_v. Example: the Gauss image (normal cone) of a convex polyhedron's vertex has area equal to the angular defect. The inequality area ≤ defect comes from a crossing count, at most 2 faces per plane, which needs no link connectivity. The normal cones tile the sphere, since the argmax vertex covers each y and overlaps lie in planes. With Descartes' Σ defect = 4π, the squeeze gives equality. Proving 'exactly 2 crossings' pointwise would have needed the faces around a vertex to form a single cycle. In Lean, work with .toReal of finite measures (ENNReal.toReal_sum with measure_ne_top) before the sum argument.