α : Type u_1
β : Type ?u.897639
γ : Type ?u.897642
δ : Type ?u.897645
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ (∑ x in SimpleFunc.range (pair f g), x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x})) ⊔
      ∑ x in SimpleFunc.range (pair f g), x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x}) ≤
    ∑ x in SimpleFunc.range (pair f g), (x.fst ⊔ x.snd) * ↑↑μ (↑(pair f g) ⁻¹' {x})
α : Type u_1
β : Type ?u.897639
γ : Type ?u.897642
δ : Type ?u.897645
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ lintegral (map Prod.fst (pair f g)) μ ⊔ lintegral (map Prod.snd (pair f g)) μ ≤
    ∑ x in SimpleFunc.range (pair f g), (x.fst ⊔ x.snd) * ↑↑μ (↑(pair f g) ⁻¹' {x})
rw [map_lintegral, map_lintegral]
case refine'_1
α : Type u_1
β : Type ?u.897639
γ : Type ?u.897642
δ : Type ?u.897645
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
a : ℝ≥0∞ × ℝ≥0∞
x✝ : a ∈ SimpleFunc.range (pair f g)
⊢ a.fst ≤ a.fst ⊔ a.snd

case refine'_2
α : Type u_1
β : Type ?u.897639
γ : Type ?u.897642
δ : Type ?u.897645
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
a : ℝ≥0∞ × ℝ≥0∞
x✝ : a ∈ SimpleFunc.range (pair f g)
⊢ a.snd ≤ a.fst ⊔ a.snd
α : Type u_1
β : Type ?u.897639
γ : Type ?u.897642
δ : Type ?u.897645
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ (∑ x in SimpleFunc.range (pair f g), x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x})) ⊔
      ∑ x in SimpleFunc.range (pair f g), x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x}) ≤
    ∑ x in SimpleFunc.range (pair f g), (x.fst ⊔ x.snd) * ↑↑μ (↑(pair f g) ⁻¹' {x})
refine' sup_le _ _ <;> refine' Finset.sum_le_sum fun a _ => mul_le_mul_right' _ _
case refine'_2
α : Type u_1
β : Type ?u.897639
γ : Type ?u.897642
δ : Type ?u.897645
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
a : ℝ≥0∞ × ℝ≥0∞
x✝ : a ∈ SimpleFunc.range (pair f g)
⊢ a.snd ≤ a.fst ⊔ a.snd
case refine'_1
α : Type u_1
β : Type ?u.897639
γ : Type ?u.897642
δ : Type ?u.897645
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
a : ℝ≥0∞ × ℝ≥0∞
x✝ : a ∈ SimpleFunc.range (pair f g)
⊢ a.fst ≤ a.fst ⊔ a.snd

case refine'_2
α : Type u_1
β : Type ?u.897639
γ : Type ?u.897642
δ : Type ?u.897645
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
a : ℝ≥0∞ × ℝ≥0∞
x✝ : a ∈ SimpleFunc.range (pair f g)
⊢ a.snd ≤ a.fst ⊔ a.snd
exact le_sup_left
no goals
case refine'_2
α : Type u_1
β : Type ?u.897639
γ : Type ?u.897642
δ : Type ?u.897645
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
a : ℝ≥0∞ × ℝ≥0∞
x✝ : a ∈ SimpleFunc.range (pair f g)
⊢ a.snd ≤ a.fst ⊔ a.snd
exact le_sup_right
no goals
α : Type u_1
β : Type ?u.897639
γ : Type ?u.897642
δ : Type ?u.897645
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (pair f g), (x.fst ⊔ x.snd) * ↑↑μ (↑(pair f g) ⁻¹' {x}) = lintegral (f ⊔ g) μ
rw [sup_eq_map₂, map_lintegral]