no goals
α : Type u_1
β : Type ?u.899767
γ : Type ?u.899770
δ : Type ?u.899773
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
hfg : f ≤ g
hμν : μ ≤ ν
⊢ lintegral (f ⊔ g) μ = lintegral g μ
rw [sup_of_le_right hfg]