no goals
α : Type u_1
β : Type ?u.1832179
γ : Type ?u.1832182
δ : Type ?u.1832185
m m0 : MeasurableSpace α
E : Type ?u.1832194
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : OpensMeasurableSpace E
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
⊢ SigmaFinite (Measure.trim μ (_ : inst✝¹ ≤ inst✝¹))
rwa [trim_eq_self]