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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
a : α
ha : M < f a
inr : ∀ (n : ℕ) (hn : u n < f a), Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | f a ≤ M} ∪ {a : α | u i < f a}) a
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | f a ≤ M} ∪ {a : α | u i < f a}) a

Tactic:
obtain ⟨n, hn⟩ : ∃ n, u n < f a := ((tendsto_order.1 ulim).2 _ ha).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.right, Iff.mp
-- 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∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
a : α
ha : M < f a
n : ℕ
hn : u n < f a
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | f a ≤ M} ∪ {a : α | u i < f a}) a

Tactic:
mem_iUnion.2 ⟨n, Or.inr hn⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro, Or.inr
-- 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∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
a : α
ha : M < f a
n : ℕ
hn : u n < f a
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | f a ≤ M} ∪ {a : α | u i < f a}) a

Tactic:
exact mem_iUnion.2 ⟨n, Or.inr hn⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- 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∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
s : ν.FiniteSpanningSetsIn univ :=
  FiniteSpanningSetsIn.mk (C := univ) (fun (n : ℕ) ↦ {a : α | f a ≤ M} ∪ {a : α | u n < f a}) ⋯ ⋯ ⋯
⊢ SigmaFinite ν

Tactic:
⟨⟨s⟩⟩

Premises used: Nonempty.intro, MeasureTheory.SigmaFinite.mk
-- 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∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
s : ν.FiniteSpanningSetsIn univ :=
  FiniteSpanningSetsIn.mk (C := univ) (fun (n : ℕ) ↦ {a : α | f a ≤ M} ∪ {a : α | u n < f a}) ⋯ ⋯ ⋯
⊢ SigmaFinite ν

Tactic:
exact ⟨⟨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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
⊢ SigmaFinite ν

Tactic:
have : SigmaFinite ν := by
    obtain ⟨u, -, uM, ulim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), M < u n) ∧ Tendsto u atTop (𝓝 M) :=
      exists_seq_strictAnti_tendsto M
    let s : ν.FiniteSpanningSetsIn univ :=
    { set := fun n ↦ {a | f a ≤ M} ∪ {a | u n < f a}
      set_mem := fun _ ↦ trivial
      finite := by
        intro n
        have I : ν {a | f a ≤ M} = 0 := by
          rw [Measure.restrict_apply (measurableSet_le f_mble measurable_const)]
          convert! measure_empty (μ := μ)
          rw [← disjoint_iff_inter_eq_empty]
          exact disjoint_left.mpr (fun a ha ↦ by simpa using ha)
        have J : μ {a | u n < f a} < ∞ := by
          rw [lt_top_iff_ne_top]
          apply H2 _ (M_nonneg.trans_lt (uM n))
          by_contra H3
          rw [not_lt, intervalIntegral.integral_of_le (M_nonneg.trans (uM n).le)] at H3
          have g_nn_ae : ∀ᵐ t ∂(volume.restrict (Ioc 0 (u n))), 0 ≤ g t := by
            filter_upwards [ae_restrict_mem measurableSet_Ioc] with s hs using g_nn _ hs.1
          have Ig : ∫ (t : ℝ) in Ioc 0 (u n), g t = 0 :=
            le_antisymm H3 (integral_nonneg_of_ae g_nn_ae)
          have J : ∀ᵐ t ∂(volume.restrict (Ioc 0 (u n))), g t = 0 :=
            (integral_eq_zero_iff_of_nonneg_ae g_nn_ae
              (g_intble (u n) (M_nonneg.trans_lt (uM n))).1).1 Ig
          have : u n ≤ M := le_csSup M_bdd J
          exact lt_irrefl _ (this.trans_lt (uM n))
        refine lt_of_le_of_lt (measure_union_le _ _) ?_
        rw [I, zero_add]
        apply lt_of_le_of_lt _ J
        exact restrict_le_self _
      spanning := by
        apply eq_univ_iff_forall.2 (fun a ↦ ?_)
        rcases le_or_gt (f a) M with ha | ha
        · exact mem_iUnion.2 ⟨0, Or.inl ha⟩
        · obtain ⟨n, hn⟩ : ∃ n, u n < f a := ((tendsto_order.1 ulim).2 _ ha).exists
          exact mem_iUnion.2 ⟨n, Or.inr hn⟩ }
    exact ⟨⟨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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
⊢ MeasurableSet.{u_1} (α := α) {a : α | M < f a}

Tactic:
have meas : MeasurableSet {a | M < f a} := measurableSet_lt measurable_const f_mble
-- 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∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
meas : MeasurableSet.{u_1} (α := α) {a : α | M < f a}
apply : ∀ (s : α) (hs : Membership.mem (γ := Set α) {a : α | M < f a}ᶜ s), ENNReal.ofReal (∫ (t : ℝ) in 0..f s, g t) = 0
⊢ ∫⁻ (ω : α) in {a : α | M < f a}ᶜ, ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (x : α) in {a : α | M < f a}ᶜ, 0 ∂μ

Tactic:
apply setLIntegral_congr_fun meas.compl (fun s hs ↦ ?_)

Premises used: MeasureTheory.setLIntegral_congr_fun, MeasurableSet.compl
-- 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∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
meas : MeasurableSet.{u_1} (α := α) {a : α | M < f a}
s : α
hs : Membership.mem (γ := Set α) {a : α | M < f a}ᶜ s
simp_rw :
  Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f s))) fun (t : ℝ) ↦ g t)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f s))) fun (t : ℝ) ↦ 0)
⊢ Eq (α := ℝ) (∫ (t : ℝ) in 0..f s, g t) (∫ (t : ℝ) in 0..f s, 0)

Tactic:
simp_rw [intervalIntegral.integral_of_le (f_nonneg s)]

Premises used: 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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
meas : MeasurableSet.{u_1} (α := α) {a : α | M < f a}
s : α
hs : Membership.mem (γ := Set α) {a : α | M < f a}ᶜ s
h : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f s)))] fun (a : ℝ) ↦ 0
⊢ Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f s))) fun (t : ℝ) ↦ g t)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f s))) fun (t : ℝ) ↦ 0)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
meas : MeasurableSet.{u_1} (α := α) {a : α | M < f a}
s : α
hs : Membership.mem (γ := Set α) {a : α | M < f a}ᶜ s
apply : Ioc 0 (f s) ⊆ Ioc 0 M
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f s)))] fun (a : ℝ) ↦ 0

Tactic:
apply ae_mono (restrict_mono ?_ le_rfl) hgM

Premises used: le_rfl, MeasureTheory.Measure.restrict_mono, MeasureTheory.ae_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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
meas : MeasurableSet.{u_1} (α := α) {a : α | M < f a}
s : α
hs : Membership.mem (γ := Set α) {a : α | M < f a}ᶜ s
h : f s ≤ M
⊢ Ioc 0 (f s) ⊆ Ioc 0 M

Tactic:
apply Ioc_subset_Ioc_right

Premises used: Set.Ioc_subset_Ioc_right
-- 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∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
meas : MeasurableSet.{u_1} (α := α) {a : α | M < f a}
s : α
hs : Membership.mem (γ := Set α) {a : α | M < f a}ᶜ s
⊢ f s ≤ M

Tactic:
simpa using 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 ω
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∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
meas : MeasurableSet.{u_1} (α := α) {a : α | M < f a}
s : α
hs : Membership.mem (γ := Set α) {a : α | M < f a}ᶜ s
⊢ Eq (α := ℝ) (∫ (t : ℝ) in 0..f s, g t) (∫ (t : ℝ) in 0..f s, 0)

Tactic:
have : ∫ (t : ℝ) in 0..f s, g t = ∫ (t : ℝ) in 0..f s, 0 := by
        simp_rw [intervalIntegral.integral_of_le (f_nonneg s)]
        apply integral_congr_ae
        apply ae_mono (restrict_mono ?_ le_rfl) hgM
        apply Ioc_subset_Ioc_right
        simpa using 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 ω
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∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this_1 : SigmaFinite ν
meas : MeasurableSet.{u_1} (α := α) {a : α | M < f a}
s : α
hs : Membership.mem (γ := Set α) {a : α | M < f a}ᶜ s
this : Eq (α := ℝ) (∫ (t : ℝ) in 0..f s, g t) (∫ (t : ℝ) in 0..f s, 0)
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..f s, g t) = 0

Tactic:
simp [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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
meas : MeasurableSet.{u_1} (α := α) {a : α | M < f a}
⊢ ∫⁻ (ω : α) in {a : α | M < f a}ᶜ, ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (x : α) in {a : α | M < f a}ᶜ, 0 ∂μ

Tactic:
have I : ∫⁻ ω in {a | M < f a}ᶜ, ENNReal.ofReal (∫ t in 0..f ω, g t) ∂μ
             = ∫⁻ _ in {a | M < f a}ᶜ, 0 ∂μ := by
      apply setLIntegral_congr_fun meas.compl (fun s hs ↦ ?_)
      have : ∫ (t : ℝ) in 0..f s, g t = ∫ (t : ℝ) in 0..f s, 0 := by
        simp_rw [intervalIntegral.integral_of_le (f_nonneg s)]
        apply integral_congr_ae
        apply ae_mono (restrict_mono ?_ le_rfl) hgM
        apply Ioc_subset_Ioc_right
        simpa using hs
      simp [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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
meas : MeasurableSet.{u_1} (α := α) {a : α | M < f a}
I :
  ∫⁻ (ω : α) in {a : α | M < f a}ᶜ, ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (x : α) in {a : α | M < f a}ᶜ, 0 ∂μ
⊢ ∫⁻ (ω : α) in {a : α | M < f a}ᶜ, ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0

Tactic:
simp only [lintegral_const, zero_mul] at I

Premises used: MeasureTheory.lintegral_const, MulZeroClass.zero_mul