-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem sup_mem_measurableLE {f g : α → ℝ≥0∞} (hf : f ∈ measurableLE μ ν)
    (hg : g ∈ measurableLE μ ν) : (fun a ↦ f a ⊔ g a) ∈ measurableLE μ ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ∫⁻ (x : α) in A ∩ {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in A ∩ {x | g x < f x}, f x ∂μ ≤ ν A

Tactic:
refine (add_le_add (hg.2 _ h₁) (hf.2 _ h₂)).trans_eq ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ν (A ∩ {a | f a ≤ g a}) + ν (A ∩ {a | g a < f a}) = ν A

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (x : α) in A, (fun a => f a ⊔ g a) x ∂μ ≤ ν A

Tactic:
have h₁ := hA.inter (measurableSet_le hf.1 hg.1)

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
⊢ ∫⁻ (x : α) in A, (fun a => f a ⊔ g a) x ∂μ ≤ ν A

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ν (A ∩ {a | f a ≤ g a}) + ν (A \ {a | f a ≤ g a}) = ν A

Tactic:
exact measure_inter_add_diff _ (measurableSet_le hf.1 hg.1)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
⊢ ∫⁻ (x : α) in A, (fun a => f a ⊔ g a) x ∂μ ≤ ν A

Tactic:
have h₂ := hA.inter (measurableSet_lt hg.1 hf.1)

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ∫⁻ (x : α) in A, (fun a => f a ⊔ g a) x ∂μ ≤ ν A

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ν (A ∩ {a | f a ≤ g a}) + ν (A ∩ {a | g a < f a}) = ν A

Tactic:
simp only [← not_le, ← compl_setOf, ← diff_eq]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ν (A ∩ {a | f a ≤ g a}) + ν (A \ {a | f a ≤ g a}) = ν A

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
⊢ (fun a => f a ⊔ g a) ∈ measurableLE μ ν

Tactic:
refine ⟨Measurable.max hf.1 hg.1, fun A hA ↦ ?_⟩

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (x : α) in A, (fun a => f a ⊔ g a) x ∂μ ≤ ν A

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ∫⁻ (x : α) in A, (fun a => f a ⊔ g a) x ∂μ ≤ ν A

Tactic:
rw [setLIntegral_max hf.1 hg.1]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ∫⁻ (x : α) in A ∩ {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in A ∩ {x | g x < f x}, f x ∂μ ≤ ν A