no goals
α : Type u_1
β : Type ?u.1261185
γ : Type ?u.1261188
δ : Type ?u.1261191
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite μ
C : ℝ≥0∞
hC : C < ⊤
f : α → E
hf_meas : AEStronglyMeasurable f μ
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, ↑‖f x‖₊ ∂μ) ≤ C
⊢ SigmaFinite (Measure.trim μ (_ : m ≤ m))
rwa [@trim_eq_self _ m]