α : Type u_1
β : Type ?u.1032041
γ : Type ?u.1032044
δ : Type ?u.1032047
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet {x | g x < f x}

α : Type u_1
β : Type ?u.1032041
γ : Type ?u.1032044
δ : Type ?u.1032047
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet {x | f x ≤ g x}
α : Type u_1
β : Type ?u.1032041
γ : Type ?u.1032044
δ : Type ?u.1032047
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ (∫⁻ (x : α) in s, max (f x) (g x) ∂μ) =
    (∫⁻ (x : α) in s ∩ {x | f x ≤ g x}, g x ∂μ) + ∫⁻ (x : α) in s ∩ {x | g x < f x}, f x ∂μ
rw [lintegral_max hf hg, restrict_restrict, restrict_restrict, inter_comm s, inter_comm s]
no goals
α : Type u_1
β : Type ?u.1032041
γ : Type ?u.1032044
δ : Type ?u.1032047
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet {x | g x < f x}

α : Type u_1
β : Type ?u.1032041
γ : Type ?u.1032044
δ : Type ?u.1032047
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet {x | f x ≤ g x}
exacts [measurableSet_lt hg hf, measurableSet_le hf hg]