ProbabilityTheory.integrable_of_finiteSupport

lemma integrable_of_finiteSupport (μ : Measure S) [FiniteSupport μ]    {β : Type*} [NormedAddCommGroup β] [IsFiniteMeasure μ] [Countable S]    {f : S → β} :    Integrable f μ := by  let A := μ.support  have hA : μ Aᶜ = 0 := measure_compl_support μ  by_cases hA' : A = ∅  · simp only [hA', Finset.coe_empty, compl_empty, Measure.measure_univ_eq_zero] at hA    rw [hA]    exact integrable_zero_measure  have : ∃ s₀, s₀ ∈ A := by    contrapose! hA'    ext s    simpa using hA' s  rcases this with ⟨s₀, hs₀⟩  let f' : A → β := fun a ↦ f a  classical  let g : S → A := fun s ↦ if h : s ∈ A then ⟨s, h⟩ else ⟨s₀, hs₀⟩  have : (f' ∘ g) =ᵐ[μ] f := by    apply Filter.eventuallyEq_of_mem (s := A) hA    intro a ha    simp at ha    simp [f', g, ha]  apply Integrable.congr _ this  apply Integrable.comp_measurable .of_finite  fun_prop