awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞

Tactic:
have A : ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) = ∞ := by
      rw [eq_top_iff]
      calc
      ∞ = ∫⁻ t in Ioc 0 s, ∞ * ENNReal.ofReal (g t) := by
          have I_pos : ∫⁻ (a : ℝ) in Ioc 0 s, ENNReal.ofReal (g a) ≠ 0 := by
            rw [← ofReal_integral_eq_lintegral_ofReal (g_intble s s_pos).1]
            · simpa only [not_lt, ne_eq, ENNReal.ofReal_eq_zero, not_le] using hs
            · filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht using g_nn _ ht.1
          rw [lintegral_const_mul, ENNReal.top_mul I_pos]
          exact ENNReal.measurable_ofReal.comp g_mble
      _ ≤ ∫⁻ t in Ioc 0 s, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) := by
          apply setLIntegral_mono' measurableSet_Ioc (fun x hx ↦ ?_)
          rw [← h's]
          gcongr
          exact fun ha ↦ hx.2.trans (le_of_lt ha)
      _ ≤ ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) :=
          lintegral_mono_set Ioc_subset_Ioi_self
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
rw : ∞ ≤ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∞

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
simp : ∞ = ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) * ∞
⊢ ∞ = ∫⁻ (x : α) in {a : α | s < f a}, ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) ∂μ

Tactic:
simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter,
            h's]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
rw : ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) ≠ 0
⊢ ∞ = ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) * ∞

Tactic:
rw [ENNReal.mul_top]

Premises used: ENNReal.mul_top
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) ≠ 0

Tactic:
simpa [intervalIntegral.integral_of_le s_pos.le] using hs

Premises used: LT.lt.le, intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
apply :
  ∀ (a : α) (ha : Membership.mem (γ := Set α) {a : α | s < f a} a),
    ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) ≤ ENNReal.ofReal (∫ (t : ℝ) in 0..f a, g t)
⊢ ∫⁻ (x : α) in {a : α | s < f a}, ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) ∂μ ≤
    ∫⁻ (ω : α) in {a : α | s < f a}, ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ

Tactic:
apply setLIntegral_mono' (measurableSet_lt measurable_const f_mble) (fun a ha ↦ ?_)

Premises used: measurableSet_lt, measurable_const, MeasureTheory.setLIntegral_mono'
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
a : α
ha : Membership.mem (γ := Set α) {a : α | s < f a} a
h : LE.le (α := ℝ) (∫ (t : ℝ) in 0..s, g t) (∫ (t : ℝ) in 0..f a, g t)
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) ≤ ENNReal.ofReal (∫ (t : ℝ) in 0..f a, g t)

Tactic:
apply ENNReal.ofReal_le_ofReal

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
a : α
ha : Membership.mem (γ := Set α) {a : α | s < f a} a
h : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f a)))] g
h₁ : IntervalIntegrable g volume 0 (f a)
⊢ LE.le (α := ℝ) (∫ (t : ℝ) in 0..s, g t) (∫ (t : ℝ) in 0..f a, g t)

Tactic:
apply intervalIntegral.integral_mono_interval le_rfl s_pos.le (le_of_lt ha)

Premises used: le_rfl, intervalIntegral.integral_mono_interval, le_of_lt, LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
a : α
ha : Membership.mem (γ := Set α) {a : α | s < f a} a
t : ℝ
ht : t ∈ Ioc 0 (f a)
⊢ 0 t ≤ g t

Tactic:
g_nn _ ht.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
a : α
ha : Membership.mem (γ := Set α) {a : α | s < f a} a
h :
  ∀ (a_1 : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ Ioc 0 (f a)) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 x ≤ g x) x} x}
      a_1
h₁ h₂ : ∀ (t : ℝ) (ht : t ∈ Ioc 0 (f a)), 0 t ≤ g t
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f a)))] g

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht using g_nn _ ht.1

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
a : α
ha : Membership.mem (γ := Set α) {a : α | s < f a} a
⊢ IntervalIntegrable g volume 0 (f a)

Tactic:
g_intble _ (s_pos.trans ha)

Premises used: LT.lt.trans
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
a : α
ha : Membership.mem (γ := Set α) {a : α | s < f a} a
⊢ IntervalIntegrable g volume 0 (f a)

Tactic:
exact g_intble _ (s_pos.trans ha)

Premises used: LT.lt.trans
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
⊢ ∫⁻ (ω : α) in {a : α | s < f a}, ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ ≤
    ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ

Tactic:
setLIntegral_le_lintegral _ _

Premises used: MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
_ : ∞ = ∫⁻ (x : α) in {a : α | s < f a}, ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) ∂μ
_₁ :
  ∫⁻ (x : α) in {a : α | s < f a}, ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) ∂μ ≤
    ∫⁻ (ω : α) in {a : α | s < f a}, ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ
⊢ ∞ ≤ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ

Tactic:
calc
      ∞ = ∫⁻ _ in {a | s < f a}, ENNReal.ofReal (∫ t in 0..s, g t) ∂μ := by
          simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter,
            h's]
          rw [ENNReal.mul_top]
          simpa [intervalIntegral.integral_of_le s_pos.le] using hs
      _ ≤ ∫⁻ ω in {a | s < f a}, ENNReal.ofReal (∫ t in 0..f ω, g t) ∂μ := by
          apply setLIntegral_mono' (measurableSet_lt measurable_const f_mble) (fun a ha ↦ ?_)
          apply ENNReal.ofReal_le_ofReal
          apply intervalIntegral.integral_mono_interval le_rfl s_pos.le (le_of_lt ha)
          · filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht using g_nn _ ht.1
          · exact g_intble _ (s_pos.trans ha)
      _ ≤ ∫⁻ ω, ENNReal.ofReal (∫ t in 0..f ω, g t) ∂μ := setLIntegral_le_lintegral _ _

Premises used: ENNReal.ofReal, intervalIntegral, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∞

Tactic:
have B : ∫⁻ ω, ENNReal.ofReal (∫ t in 0..f ω, g t) ∂μ = ∞ := by
      rw [eq_top_iff]
      calc
      ∞ = ∫⁻ _ in {a | s < f a}, ENNReal.ofReal (∫ t in 0..s, g t) ∂μ := by
          simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter,
            h's]
          rw [ENNReal.mul_top]
          simpa [intervalIntegral.integral_of_le s_pos.le] using hs
      _ ≤ ∫⁻ ω in {a | s < f a}, ENNReal.ofReal (∫ t in 0..f ω, g t) ∂μ := by
          apply setLIntegral_mono' (measurableSet_lt measurable_const f_mble) (fun a ha ↦ ?_)
          apply ENNReal.ofReal_le_ofReal
          apply intervalIntegral.integral_mono_interval le_rfl s_pos.le (le_of_lt ha)
          · filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht using g_nn _ ht.1
          · exact g_intble _ (s_pos.trans ha)
      _ ≤ ∫⁻ ω, ENNReal.ofReal (∫ t in 0..f ω, g t) ∂μ := setLIntegral_le_lintegral _ _
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∞
B : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∞
pos : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∞
pos₁ pos₂ : Eq (α := ℝ≥0∞) ∞ ∞
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))

Tactic:
rw [A, B]
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
contrapose :
  ∀ (H1 : ¬BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}),
    g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
⊢ BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}

Tactic:
contrapose H1
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
H1 : ¬BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
n : ℕ
rcases :
  ∀ (s : ℝ)
    (hs : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} s)
    (ns : (↑n : ℝ) < s), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (↑n : ℝ)))] 0
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (↑n : ℝ)))] 0

Tactic:
rcases not_bddAbove_iff.1 H1 n with ⟨s, hs, ns⟩

Premises used: Nat.cast, Iff.mp, not_bddAbove_iff
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
H1 : ¬BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
n : ℕ
s : ℝ
hs : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} s
ns : (↑n : ℝ) < s
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (↑n : ℝ)))] 0

Tactic:
ae_restrict_of_ae_restrict_of_subset (Ioc_subset_Ioc_right ns.le) hs

Premises used: Set.Ioc_subset_Ioc_right, Filter.EventuallyEq, LT.lt.le, MeasureTheory.ae_restrict_of_ae_restrict_of_subset
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
H1 : ¬BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
n : ℕ
s : ℝ
hs : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} s
ns : (↑n : ℝ) < s
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (↑n : ℝ)))] 0

Tactic:
exact ae_restrict_of_ae_restrict_of_subset (Ioc_subset_Ioc_right ns.le) hs

Premises used: Set.Ioc_subset_Ioc_right, LT.lt.le, MeasureTheory.ae_restrict_of_ae_restrict_of_subset
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
H1 : ¬BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
⊢ ∀ (n : ℕ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (↑n : ℝ)))] 0

Tactic:
have : ∀ (n : ℕ), g =ᵐ[volume.restrict (Ioc (0 : ℝ) n)] 0 := by
      intro n
      rcases not_bddAbove_iff.1 H1 n with ⟨s, hs, ns⟩
      exact ae_restrict_of_ae_restrict_of_subset (Ioc_subset_Ioc_right ns.le) hs
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
H1 : ¬BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
this : ∀ (n : ℕ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (↑n : ℝ)))] 0
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (⋃ (n : ℕ), Ioc 0 (↑n : ℝ)))] 0

Tactic:
have Hg : g =ᵐ[volume.restrict (⋃ (n : ℕ), (Ioc (0 : ℝ) n))] 0 :=
      (ae_restrict_iUnion_iff _ _).2 this