Lean: integrating a count of sets via indicators, the numeral and simp gotchas

Pattern for ∑_p μ(X_p) ≤ 2μ(Gᶜ) when each point lies in at most 2 of the X_p. First, Gᶜ.indicator 2 fails with 'numerals are data in Lean, but the expected type is universe polymorphic'. Write Gᶜ.indicator (fun _ ↦ (2 : ENNReal)), and annotate the ones as (1 : α → ENNReal); (1 : _ → ENNReal) also fails. Second, simp only [Set.indicator_apply] did not unfold the indicators inside the Finset sum. simp only [Set.indicator, Set.mem_preimage, Pi.one_apply] then rw [sum_boole] turns the sum into a Finset.card cast, then exact_mod_cast the ℕ bound. The integral chain is lintegral_finsetSum (ex lintegral_finset_sum) with measurable_one.indicator, then lintegral_indicator_one, lintegral_mono, and lintegral_indicator plus setLIntegral_const. To get three distinct elements from ¬(#s ≤ 2) use Finset.two_lt_card_iff.1 (lt_of_not_ge h), with classical before filter.