α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
have integrand_eq :
  ∀ ω, ENNReal.ofReal (∫ t in (0)..f ω, g t) = ∫⁻ t in Ioc 0 (f ω), ENNReal.ofReal (g t) := by
  intro ω
  have g_ae_nn : 0 ≤ᵐ[volume.restrict (Ioc 0 (f ω))] g := by
    filter_upwards [self_mem_ae_restrict (measurableSet_Ioc : MeasurableSet (Ioc 0 (f ω)))] with x
      hx using g_nn x hx.1
  rw [← ofReal_integral_eq_lintegral_ofReal (g_intble' (f ω) (f_nn ω)).1 g_ae_nn]
  congr
  exact intervalIntegral.integral_of_le (f_nn ω)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ (∫⁻ (ω : α), ∫⁻ (a : ℝ), indicator (Ioc 0 (f ω)) (fun t => ENNReal.ofReal (g t)) a ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
simp_rw [integrand_eq, ← lintegral_indicator (fun t => ENNReal.ofReal (g t)) measurableSet_Ioc]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ (∫⁻ (ω : α), ∫⁻ (a : ℝ), indicator (Ioc 0 (f ω)) (fun t => ENNReal.ofReal (g t)) a ∂μ) =
    ∫⁻ (a : ℝ), indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) a
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ (∫⁻ (ω : α), ∫⁻ (a : ℝ), indicator (Ioc 0 (f ω)) (fun t => ENNReal.ofReal (g t)) a ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
rw [← lintegral_indicator _ measurableSet_Ioi]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ (∫⁻ (y : ℝ), ∫⁻ (x : α), indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y ∂μ) =
    ∫⁻ (a : ℝ), indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) a

case hf
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ AEMeasurable (Function.uncurry fun ω a => indicator (Ioc 0 (f ω)) (fun t => ENNReal.ofReal (g t)) a)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ (∫⁻ (ω : α), ∫⁻ (a : ℝ), indicator (Ioc 0 (f ω)) (fun t => ENNReal.ofReal (g t)) a ∂μ) =
    ∫⁻ (a : ℝ), indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) a
rw [lintegral_lintegral_swap]
case hf
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd)
⊢ AEMeasurable (indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd))
case hf
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd)
⊢ AEMeasurable (Function.uncurry fun ω a => indicator (Ioc 0 (f ω)) (fun t => ENNReal.ofReal (g t)) a)
rw [aux₂]
case hf
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd)
mble : MeasurableSet {p | p.fst ∈ univ ∧ p.snd ∈ Ioc (OfNat.ofNat 0 p.fst) (f p.fst)}
⊢ AEMeasurable (indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd))
case hf
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd)
⊢ AEMeasurable (indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd))
have mble := measurableSet_region_between_oc measurable_zero f_mble MeasurableSet.univ
case hf
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd)
mble : MeasurableSet {p | p.snd ∈ Ioc 0 (f p.fst)}
⊢ AEMeasurable (indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd))
case hf
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd)
mble : MeasurableSet {p | p.fst ∈ univ ∧ p.snd ∈ Ioc (OfNat.ofNat 0 p.fst) (f p.fst)}
⊢ AEMeasurable (indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd))
simp_rw [mem_univ, Pi.zero_apply, true_and_iff] at mble
no goals
case hf
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd)
mble : MeasurableSet {p | p.snd ∈ Ioc 0 (f p.fst)}
⊢ AEMeasurable (indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd))
exact (ENNReal.measurable_ofReal.comp (g_mble.comp measurable_snd)).aemeasurable.indicator mble
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
t : ℝ
ht : 0 ≤ t
⊢ IntervalIntegrable g volume 0 t
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
⊢ ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
intro t ht
case inl
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
t : ℝ
ht : 0 ≤ t
h : 0 = t
⊢ IntervalIntegrable g volume 0 t

case inr
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
t : ℝ
ht : 0 ≤ t
h : 0 < t
⊢ IntervalIntegrable g volume 0 t
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
t : ℝ
ht : 0 ≤ t
⊢ IntervalIntegrable g volume 0 t
cases' eq_or_lt_of_le ht with h h
no goals
case inl
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
t : ℝ
ht : 0 ≤ t
h : 0 = t
⊢ IntervalIntegrable g volume 0 t
simp [← h]
no goals
case inr
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
t : ℝ
ht : 0 ≤ t
h : 0 < t
⊢ IntervalIntegrable g volume 0 t
exact g_intble t h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
⊢ ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
intro ω
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᵐ[Measure.restrict volume (Ioc 0 (f ω))] g
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
have g_ae_nn : 0 ≤ᵐ[volume.restrict (Ioc 0 (f ω))] g := by
  filter_upwards [self_mem_ae_restrict (measurableSet_Ioc : MeasurableSet (Ioc 0 (f ω)))] with x
    hx using g_nn x hx.1
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᵐ[Measure.restrict volume (Ioc 0 (f ω))] g
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ENNReal.ofReal (∫ (x : ℝ) in Ioc 0 (f ω), g x)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᵐ[Measure.restrict volume (Ioc 0 (f ω))] g
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
rw [← ofReal_integral_eq_lintegral_ofReal (g_intble' (f ω) (f_nn ω)).1 g_ae_nn]
case e_r
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᵐ[Measure.restrict volume (Ioc 0 (f ω))] g
⊢ (∫ (t : ℝ) in 0 ..f ω, g t) = ∫ (x : ℝ) in Ioc 0 (f ω), g x
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᵐ[Measure.restrict volume (Ioc 0 (f ω))] g
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ENNReal.ofReal (∫ (x : ℝ) in Ioc 0 (f ω), g x)
congr
no goals
case e_r
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᵐ[Measure.restrict volume (Ioc 0 (f ω))] g
⊢ (∫ (t : ℝ) in 0 ..f ω, g t) = ∫ (x : ℝ) in Ioc 0 (f ω), g x
exact intervalIntegral.integral_of_le (f_nn ω)
no goals
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
⊢ 0 ≤ᵐ[Measure.restrict volume (Ioc 0 (f ω))] g
filter_upwards [self_mem_ae_restrict (measurableSet_Ioc : MeasurableSet (Ioc 0 (f ω)))] with x
  hx using g_nn x hx.1
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ (fun y => ∫⁻ (x : α), indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y ∂μ) = fun a =>
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) a
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ (∫⁻ (y : ℝ), ∫⁻ (x : α), indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y ∂μ) =
    ∫⁻ (a : ℝ), indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) a
apply congr_arg
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
⊢ (∫⁻ (x : α), indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ (fun y => ∫⁻ (x : α), indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y ∂μ) = fun a =>
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) a
funext s
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (∫⁻ (x : α), ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x) ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (∫⁻ (x : α), indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
simp_rw [aux₁]
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α), indicator (Ici s) (fun x => 1) (f a) ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s

case h.h.hr
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s ≠ ⊤
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (∫⁻ (x : α), ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x) ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
rw [lintegral_const_mul']
case h.h.hr
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s ≠ ⊤

case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α), indicator (Ici s) (fun x => 1) (f a) ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α), indicator (Ici s) (fun x => 1) (f a) ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s

case h.h.hr
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s ≠ ⊤
swap
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α), indicator {a | s ≤ f a} (fun x => 1) a ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α), indicator (Ici s) (fun x => 1) (f a) ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
simp_rw [show
    (fun a => (Ici s).indicator (fun _ : ℝ => (1 : ℝ≥0∞)) (f a)) = fun a =>
      {a : α | s ≤ f a}.indicator (fun _ => 1) a
    by funext a; by_cases s ≤ f a <;> simp [h]]
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α) in {a | s ≤ f a}, 1 ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s

case h.h.hs
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ MeasurableSet {a | s ≤ f a}
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α), indicator {a | s ≤ f a} (fun x => 1) a ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
rw [lintegral_indicator]
case h.h.hs
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ MeasurableSet {a | s ≤ f a}

case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α) in {a | s ≤ f a}, 1 ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α) in {a | s ≤ f a}, 1 ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s

case h.h.hs
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ MeasurableSet {a | s ≤ f a}
swap
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun _x => 1 * ↑↑μ {a | s ≤ f a}) s =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a}) s * ENNReal.ofReal (g s)
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α) in {a | s ≤ f a}, 1 ∂μ) =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
rw [lintegral_one, Measure.restrict_apply MeasurableSet.univ, univ_inter, indicator_mul_left,
  mul_assoc,
  show
    (Ioi 0).indicator (fun _x : ℝ => (1 : ℝ≥0∞)) s * μ {a : α | s ≤ f a} =
      (Ioi 0).indicator (fun _x : ℝ => 1 * μ {a : α | s ≤ f a}) s
    by by_cases 0 < s <;> simp [h]]
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun _x => ↑↑μ {a | s ≤ f a}) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a}) s
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun _x => 1 * ↑↑μ {a | s ≤ f a}) s =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a}) s * ENNReal.ofReal (g s)
simp_rw [mul_comm _ (ENNReal.ofReal _), one_mul]
no goals
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun _x => ↑↑μ {a | s ≤ f a}) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a}) s
rfl
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
⊢ (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
funext a
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h : s ∈ Ioc 0 (f a)
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)

case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h : ¬s ∈ Ioc 0 (f a)
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
by_cases s ∈ Ioc (0 : ℝ) (f a)
no goals
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h : s ∈ Ioc 0 (f a)
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
simp only [h, show s ∈ Ioi (0 : ℝ) from h.1, show f a ∈ Ici s from h.2, indicator_of_mem,
  mul_one]
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h h_copy : ¬s ∈ Ioc 0 (f a)
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h : ¬s ∈ Ioc 0 (f a)
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
have h_copy := h
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : ¬s ∈ Ioc 0 (f a)
h : 0 < s → f a < s
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h h_copy : ¬s ∈ Ioc 0 (f a)
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
simp only [mem_Ioc, not_and, not_le] at h
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : ¬s ∈ Ioc 0 (f a)
h : 0 < s → f a < s
h' : 0 < s
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)

case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : ¬s ∈ Ioc 0 (f a)
h : 0 < s → f a < s
h' : ¬0 < s
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : ¬s ∈ Ioc 0 (f a)
h : 0 < s → f a < s
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
by_cases h' : 0 < s
no goals
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : ¬s ∈ Ioc 0 (f a)
h : 0 < s → f a < s
h' : 0 < s
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
simp only [h_copy, h h', indicator_of_not_mem, not_false_iff, mem_Ici, not_le,
  MulZeroClass.mul_zero]
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : ¬s ∈ Ioc 0 (f a)
h : 0 < s → f a < s
h' : ¬0 < s
this : ¬s ∈ Ioi 0
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : ¬s ∈ Ioc 0 (f a)
h : 0 < s → f a < s
h' : ¬0 < s
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
have : s ∉ Ioi (0 : ℝ) := h'
no goals
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : ¬s ∈ Ioc 0 (f a)
h : 0 < s → f a < s
h' : ¬0 < s
this : ¬s ∈ Ioi 0
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
simp only [this, h', indicator_of_not_mem, not_false_iff, MulZeroClass.mul_zero,
  MulZeroClass.zero_mul, mem_Ioc, false_and_iff]
case h.h.hr
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ indicator (Ioi 0) (fun x => 1) s ≠ ⊤
case h.h.hr
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s ≠ ⊤
apply ENNReal.mul_ne_top ENNReal.ofReal_ne_top
no goals
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
h : ¬0 < s
⊢ indicator (Ioi 0) (fun x => 1) s ≠ ⊤
simp [indicator_apply, h]
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
a : α
⊢ indicator (Ici s) (fun x => 1) (f a) = indicator {a | s ≤ f a} (fun x => 1) a
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (fun a => indicator (Ici s) (fun x => 1) (f a)) = fun a => indicator {a | s ≤ f a} (fun x => 1) a
funext a
no goals
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
a : α
⊢ indicator (Ici s) (fun x => 1) (f a) = indicator {a | s ≤ f a} (fun x => 1) a
by_cases s ≤ f a <;> simp [h]
no goals
case h.h.hs
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ MeasurableSet {a | s ≤ f a}
exact f_mble measurableSet_Ici
no goals
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s✝ : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ indicator (Ioi 0) (fun _x => 1) s * ↑↑μ {a | s ≤ f a} = indicator (Ioi 0) (fun _x => 1 * ↑↑μ {a | s ≤ f a}) s
by_cases 0 < s <;> simp [h]
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p : α × ℝ
⊢ Function.uncurry (fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) p =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) p
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ (Function.uncurry fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd)
funext p
case h.mk
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
⊢ Function.uncurry (fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) (p_fst, p_snd) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p : α × ℝ
⊢ Function.uncurry (fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) p =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) p
cases p with | mk p_fst p_snd => ?_
case h.mk
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
case h.mk
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
⊢ Function.uncurry (fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) (p_fst, p_snd) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
rw [Function.uncurry_apply_pair]
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : p_snd ∈ Ioc 0 (f p_fst)
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)

case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : ¬p_snd ∈ Ioc 0 (f p_fst)
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
case h.mk
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
by_cases p_snd ∈ Ioc 0 (f p_fst)
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : p_snd ∈ Ioc 0 (f p_fst)
h' : (p_fst, p_snd) ∈ {p | p.snd ∈ Ioc 0 (f p.fst)}
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : p_snd ∈ Ioc 0 (f p_fst)
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
have h' : (p_fst, p_snd) ∈ {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := h
no goals
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : p_snd ∈ Ioc 0 (f p_fst)
h' : (p_fst, p_snd) ∈ {p | p.snd ∈ Ioc 0 (f p.fst)}
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
rw [Set.indicator_of_mem h', Set.indicator_of_mem h]
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : ¬p_snd ∈ Ioc 0 (f p_fst)
h' : ¬(p_fst, p_snd) ∈ {p | p.snd ∈ Ioc 0 (f p.fst)}
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : ¬p_snd ∈ Ioc 0 (f p_fst)
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
have h' : (p_fst, p_snd) ∉ {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := h
no goals
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : ¬p_snd ∈ Ioc 0 (f p_fst)
h' : ¬(p_fst, p_snd) ∈ {p | p.snd ∈ Ioc 0 (f p.fst)}
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
rw [Set.indicator_of_not_mem h', Set.indicator_of_not_mem h]