pigeonhole

lemma pigeonhole {G : Type*} [MeasureSpace G] [IsProbabilityMeasure (ℙ : Measure G)] [Finite G]    [MeasurableSingletonClass G] (f : G → ℝ) : ∃ x, f x ≤ ∫ (z : G), f z ∧ ℙ {x} ≠ 0 := by  cases nonempty_fintype G  set I := ∫ (z : G), f z with hI  simp only [Integrable.of_finite, integral_fintype, smul_eq_mul] at hI  by_contra!  have hI': ∑ x, (ℙ:Measure G).real {x} * f x > ∑ x, (ℙ:Measure G).real {x} * I := by    apply Finset.sum_lt_sum    · intro i _      by_cases h : I ≤ f i      · gcongr      specialize this i (by order)      rw [←measureReal_eq_zero_iff] at this      simp [this]    have : ∑ x, (ℙ:Measure G).real {x} = 1 := by simp    replace : ∃ x, (ℙ:Measure G).real {x} ≠ 0 := by contrapose! this; simp [this]    obtain ⟨x, hx⟩ := this    use x, by simp    gcongr; contrapose! hx    specialize this x hx; simpa [measureReal_eq_zero_iff] using this  simp [←Finset.sum_mul, sum_measureReal_singleton] at hI'  order