α : Type u_1
β : Type ?u.898603
γ : Type ?u.898606
δ : Type ?u.898609
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
⊢ (∫⁻ (a : α), f a + g a ∂μ) ≤ (∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), g a ∂μ
α : Type u_1
β : Type ?u.898603
γ : Type ?u.898606
δ : Type ?u.898609
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
⊢ (∫⁻ (a : α), f a + g a ∂μ) = (∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), g a ∂μ
refine' le_antisymm _ (le_lintegral_add _ _)
case intro.intro.intro
α : Type u_1
β : Type ?u.898603
γ : Type ?u.898606
δ : Type ?u.898609
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ fun a => f a + g a
hφ_eq : (∫⁻ (a : α), f a + g a ∂μ) = ∫⁻ (a : α), φ a ∂μ
⊢ (∫⁻ (a : α), f a + g a ∂μ) ≤ (∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), g a ∂μ
α : Type u_1
β : Type ?u.898603
γ : Type ?u.898606
δ : Type ?u.898609
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
⊢ (∫⁻ (a : α), f a + g a ∂μ) ≤ (∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), g a ∂μ
rcases exists_measurable_le_lintegral_eq μ fun a => f a + g a with ⟨φ, hφm, hφ_le, hφ_eq⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.898603
γ : Type ?u.898606
δ : Type ?u.898609
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ fun a => f a + g a
hφ_eq : (∫⁻ (a : α), f a + g a ∂μ) = ∫⁻ (a : α), φ a ∂μ
⊢ (∫⁻ (a : α), f a + g a ∂μ) ≤ (∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), g a ∂μ
calc
  (∫⁻ a, f a + g a ∂μ) = ∫⁻ a, φ a ∂μ := hφ_eq
  _ ≤ ∫⁻ a, f a + (φ a - f a) ∂μ := (lintegral_mono fun a => le_add_tsub)
  _ = (∫⁻ a, f a ∂μ) + ∫⁻ a, φ a - f a ∂μ := (lintegral_add_aux hf (hφm.sub hf))
  _ ≤ (∫⁻ a, f a ∂μ) + ∫⁻ a, g a ∂μ :=
    add_le_add_left (lintegral_mono fun a => tsub_le_iff_left.2 <| hφ_le a) _