α : Type u_1
β : Type ?u.1029220
γ : Type ?u.1029223
δ : Type ?u.1029226
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ (∫⁻ (x : α), max (f x) (g x) ∂μ) = (∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ) + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ
α : Type u_1
β : Type ?u.1029220
γ : Type ?u.1029223
δ : Type ?u.1029226
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (∫⁻ (x : α), max (f x) (g x) ∂μ) = (∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ) + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ
have hm : MeasurableSet { x | f x ≤ g x } := measurableSet_le hf hg
α : Type u_1
β : Type ?u.1029220
γ : Type ?u.1029223
δ : Type ?u.1029226
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ((∫⁻ (x : α) in {x | f x ≤ g x}, max (f x) (g x) ∂μ) + ∫⁻ (x : α) in {x | f x ≤ g x}ᶜ, max (f x) (g x) ∂μ) =
    (∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ) + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ
α : Type u_1
β : Type ?u.1029220
γ : Type ?u.1029223
δ : Type ?u.1029226
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ (∫⁻ (x : α), max (f x) (g x) ∂μ) = (∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ) + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ
rw [← lintegral_add_compl (fun x => max (f x) (g x)) hm]
α : Type u_1
β : Type ?u.1029220
γ : Type ?u.1029223
δ : Type ?u.1029226
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ((∫⁻ (x : α) in {x | f x ≤ g x}, max (f x) (g x) ∂μ) + ∫⁻ (x : α) in {x | f x ≤ g x}ᶜ, max (f x) (g x) ∂μ) =
    (∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ) + ∫⁻ (x : α) in {a | f a ≤ g a}ᶜ, f x ∂μ
α : Type u_1
β : Type ?u.1029220
γ : Type ?u.1029223
δ : Type ?u.1029226
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ((∫⁻ (x : α) in {x | f x ≤ g x}, max (f x) (g x) ∂μ) + ∫⁻ (x : α) in {x | f x ≤ g x}ᶜ, max (f x) (g x) ∂μ) =
    (∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ) + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ
simp only [← compl_setOf, ← not_le]
no goals
case refine'_1
α : Type u_1
β : Type ?u.1029220
γ : Type ?u.1029223
δ : Type ?u.1029226
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≤ g x} → max (f x) (g x) = g x

case refine'_2
α : Type u_1
β : Type ?u.1029220
γ : Type ?u.1029223
δ : Type ?u.1029226
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≤ g x}ᶜ → max (f x) (g x) = f x
exacts [ae_of_all _ fun x => max_eq_right (a := f x) (b := g x),
  ae_of_all _ fun x (hx : ¬ f x ≤ g x) => max_eq_left (not_le.1 hx).le]