Summing the two-step height change across translation

theorem MagnitudeConjecture.HeightArrowCount.boundary_height_difference {V : Type u} [Fintype V] (P I : V → Prop) [DecidablePred P] [DecidablePred I] (e : { x : V // ¬P x } ≃ { x : V // ¬I x }) (h : V → ℤ) (he : ∀ (x : { x : V // ¬P x }), h ↑x = h ↑(e x) + 2) : ∑ x : { x : V // I x }, h ↑x - ∑ x : { x : V // P x }, h ↑x = 2 * (↑(Fintype.card V) - ↑(Fintype.card { x : V // P x }))

Translation identifies the two complementary boundary sets. Summing its height change gives the difference of boundary height sums.