α : Type u_1
β : Type ?u.797130
γ : Type ?u.797133
δ : Type ?u.797136
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
⊢ ((⨆ (g : α →ₛ ℝ≥0∞) (_ : ↑g ≤ fun a => f a), SimpleFunc.lintegral g μ) +
      ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => g a), SimpleFunc.lintegral g_1 μ) ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f a + g a), SimpleFunc.lintegral g_1 μ
α : Type u_1
β : Type ?u.797130
γ : Type ?u.797133
δ : Type ?u.797136
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
⊢ ((∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), g a ∂μ) ≤ ∫⁻ (a : α), f a + g a ∂μ
simp only [lintegral]
α : Type u_1
β : Type ?u.797130
γ : Type ?u.797133
δ : Type ?u.797136
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
f' : α →ₛ ℝ≥0∞
hf' : (fun h => ↑h ≤ f) f'
g' : α →ₛ ℝ≥0∞
hg' : (fun h => ↑h ≤ g) g'
⊢ SimpleFunc.lintegral f' μ + SimpleFunc.lintegral g' μ ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f a + g a), SimpleFunc.lintegral g_1 μ
α : Type u_1
β : Type ?u.797130
γ : Type ?u.797133
δ : Type ?u.797136
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
⊢ ((⨆ (g : α →ₛ ℝ≥0∞) (_ : ↑g ≤ fun a => f a), SimpleFunc.lintegral g μ) +
      ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => g a), SimpleFunc.lintegral g_1 μ) ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f a + g a), SimpleFunc.lintegral g_1 μ
refine' ENNReal.biSup_add_biSup_le' (p := fun h : α →ₛ ℝ≥0∞ => h ≤ f)
  (q := fun h : α →ₛ ℝ≥0∞ => h ≤ g) ⟨0, zero_le f⟩ ⟨0, zero_le g⟩ fun f' hf' g' hg' => _
no goals
α : Type u_1
β : Type ?u.797130
γ : Type ?u.797133
δ : Type ?u.797136
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
f' : α →ₛ ℝ≥0∞
hf' : (fun h => ↑h ≤ f) f'
g' : α →ₛ ℝ≥0∞
hg' : (fun h => ↑h ≤ g) g'
⊢ SimpleFunc.lintegral f' μ + SimpleFunc.lintegral g' μ ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => f a + g a), SimpleFunc.lintegral g_1 μ
exact le_iSup₂_of_le (f' + g') (add_le_add hf' hg') (add_lintegral _ _).ge