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
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ g x = 0 x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  Eq (α := ℝ≥0∞)
                    ((fun (t : ℝ) ↦
                        HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞)
                          (ENNReal.ofReal (g t)))
                      x)
                    (0 x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (t : ℝ) (ht : g t = 0 t),
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) = 0 t
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ≥0∞)
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) 0

Tactic:
filter_upwards [H1] with t ht using by simp [ht]
-- 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
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ≥0∞)
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) 0

Tactic:
have : (fun t ↦ μ {a : α | t ≤ f a} * ENNReal.ofReal (g t))
        =ᵐ[volume.restrict (Ioi (0 : ℝ))] 0 := by
          filter_upwards [H1] with t ht using by simp [ht]
-- 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
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0
this :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ≥0∞)
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) 0
⊢ ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    0

Tactic:
simp [lintegral_congr_ae this]

Premises used: MeasureTheory.lintegral_congr_ae
-- 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
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0
⊢ ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    0

Tactic:
have B : ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) = 0 := by
      have : (fun t ↦ μ {a : α | t ≤ f a} * ENNReal.ofReal (g t))
        =ᵐ[volume.restrict (Ioi (0 : ℝ))] 0 := by
          filter_upwards [H1] with t ht using by simp [ht]
      simp [lintegral_congr_ae this]
-- 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
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0
B :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    0
pos :
  0 =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
pos₁ pos₂ : Eq (α := ℝ≥0∞) 0 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
pos :
  ∀
    (H2 :
      ∃ s > 0,
        LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t) ∧
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥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))
neg :
  ∀
    (H2 :
      ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥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))
⊢ ∫⁻ (ω : α), 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:
by_cases! H2 : ∃ s > 0, 0 < ∫ t in 0..s, g t ∧ μ {a : α | s < f a} = ∞
-- 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 > 0,
    LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  ∀ (s : ℝ) (s_pos : s > 0) (hs : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t))
    (h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥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))
⊢ ∫⁻ (ω : α), 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:
rcases H2 with ⟨s, s_pos, hs, h's⟩
-- 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 (∫ (t : ℝ) in 0..s, g t)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)

Tactic:
rw [intervalIntegral.integral_of_le s_pos.le] at 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 (∫ (t : ℝ) in 0..s, g t)
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₁ : LT.lt (α := ℝ) 0 (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [intervalIntegral.integral_of_le s_pos.le] at 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∞)
rw :
  ∞ ≤
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
⊢ ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (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∞)
rw : ENNReal.ofReal (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x) ≠ 0
rw₁ : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] g
⊢ ∫⁻ (a : ℝ) in Ioc 0 s, ENNReal.ofReal (g a) ≠ 0

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal (g_intble s s_pos).1]

Premises used: And.left, MeasureTheory.ofReal_integral_eq_lintegral_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∞)
⊢ ENNReal.ofReal (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 s)) fun (x : ℝ) ↦ g x) ≠ 0

Tactic:
simpa only [not_lt, ne_eq, ENNReal.ofReal_eq_zero, not_le] using hs

Premises used: not_le, ENNReal.ofReal_eq_zero, ne_eq, not_lt
-- 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 : ℝ
ht : t ∈ Ioc 0 s
⊢ 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∞)
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ Ioc 0 s) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 x ≤ g x) x} x}
      a
h₁ h₂ : ∀ (t : ℝ) (ht : t ∈ Ioc 0 s), 0 t ≤ g t
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 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 : ℝ) in Ioc 0 s, ENNReal.ofReal (g a) ≠ 0

Tactic:
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
-- 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∞)
I_pos : ∫⁻ (a : ℝ) in Ioc 0 s, ENNReal.ofReal (g a) ≠ 0
hf : Measurable (β := ℝ≥0∞) fun (t : ℝ) ↦ ENNReal.ofReal (g t)
⊢ ∞ = ∫⁻ (t : ℝ) in Ioc 0 s, ∞ * ENNReal.ofReal (g t)

Tactic:
rw [lintegral_const_mul, ENNReal.top_mul I_pos]

Premises used: ENNReal.top_mul, MeasureTheory.lintegral_const_mul
-- 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∞)
I_pos : ∫⁻ (a : ℝ) in Ioc 0 s, ENNReal.ofReal (g a) ≠ 0
⊢ Measurable (β := ℝ≥0∞) fun (t : ℝ) ↦ ENNReal.ofReal (g t)

Tactic:
ENNReal.measurable_ofReal.comp g_mble

Premises used: ENNReal.ofNNReal, Measurable.comp, ENNReal.ofReal, WithTop.some, ENNReal.measurable_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∞)
I_pos : ∫⁻ (a : ℝ) in Ioc 0 s, ENNReal.ofReal (g a) ≠ 0
⊢ Measurable (β := ℝ≥0∞) fun (t : ℝ) ↦ ENNReal.ofReal (g t)

Tactic:
exact ENNReal.measurable_ofReal.comp g_mble

Premises used: Measurable.comp, ENNReal.measurable_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∞)
apply :
  ∀ (x : ℝ) (hx : x ∈ Ioc 0 s),
    ∞ * ENNReal.ofReal (g x) ≤
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | x ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g x))
⊢ ∫⁻ (t : ℝ) in Ioc 0 s, ∞ * ENNReal.ofReal (g t) ≤
    ∫⁻ (t : ℝ) in Ioc 0 s,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))

Tactic:
apply setLIntegral_mono' measurableSet_Ioc (fun x hx ↦ ?_)

Premises used: measurableSet_Ioc, 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∞)
x : ℝ
hx : x ∈ Ioc 0 s
rw :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (ENNReal.ofReal (g x)) ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | x ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g x))
⊢ ∞ * ENNReal.ofReal (g x) ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | x ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g x))

Tactic:
rw [← h's]
-- 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∞)
x : ℝ
hx : x ∈ Ioc 0 s
bc : ∀ (a : α), s < f a → x ≤ f a
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (ENNReal.ofReal (g x)) ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | x ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g x))

Tactic:
gcongr
-- 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∞)
x : ℝ
hx : x ∈ Ioc 0 s
a : α
⊢ s < f a → x ≤ f a

Tactic:
fun ha ↦ hx.2.trans (le_of_lt ha)

Premises used: le_of_lt, And.right, LE.le.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∞)
x : ℝ
hx : x ∈ Ioc 0 s
a : α
⊢ s < f a → x ≤ f a

Tactic:
exact fun ha ↦ hx.2.trans (le_of_lt ha)

Premises used: le_of_lt, And.right, LE.le.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∞)
⊢ ∫⁻ (t : ℝ) in Ioc 0 s,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) ≤
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))

Tactic:
lintegral_mono_set Ioc_subset_Ioi_self

Premises used: Set.Ioc_subset_Ioi_self, MeasureTheory.lintegral_mono_set
-- 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 : ∞ = ∫⁻ (t : ℝ) in Ioc 0 s, ∞ * ENNReal.ofReal (g t)
t₁ :
  ∫⁻ (t : ℝ) in Ioc 0 s, ∞ * ENNReal.ofReal (g t) ≤
    ∫⁻ (t : ℝ) in Ioc 0 s,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
⊢ ∞ ≤
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))

Tactic:
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

Premises used: Set.Ioc, Set.Ioi, Set.Ioc_subset_Ioi_self, MeasureTheory.lintegral_mono_set, OfNat.ofNat