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 ω
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
Hg : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (⋃ (n : ℕ), Ioc 0 (↑n : ℝ)))] 0
⊢ Eq (α := Set ℝ) (⋃ (n : ℕ), Ioc 0 (↑n : ℝ)) (Ioi 0)

Tactic:
have : (⋃ (n : ℕ), (Ioc (0 : ℝ) n)) = Ioi 0 :=
      iUnion_Ioc_eq_Ioi_self_iff.2 (fun x _ ↦ exists_nat_ge x)
-- 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_1 : ∀ (n : ℕ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (↑n : ℝ)))] 0
Hg : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (⋃ (n : ℕ), Ioc 0 (↑n : ℝ)))] 0
this : Eq (α := Set ℝ) (⋃ (n : ℕ), Ioc 0 (↑n : ℝ)) (Ioi 0)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (Hg : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0)
    (this : Eq (α := Set ℝ) (⋃ (n : ℕ), Ioc 0 (↑n : ℝ)) (Ioi 0)),
    g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0

Tactic:
rwa [this] at Hg
-- 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∞)
⊢ BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}

Tactic:
have M_bdd : BddAbove {s : ℝ | g =ᵐ[volume.restrict (Ioc (0 : ℝ) s)] 0} := by
    contrapose H1
    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
    have Hg : g =ᵐ[volume.restrict (⋃ (n : ℕ), (Ioc (0 : ℝ) n))] 0 :=
      (ae_restrict_iUnion_iff _ _).2 this
    have : (⋃ (n : ℕ), (Ioc (0 : ℝ) n)) = Ioi 0 :=
      iUnion_Ioc_eq_Ioi_self_iff.2 (fun x _ ↦ exists_nat_ge x)
    rwa [this] at Hg
-- 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}
⊢ Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0

Tactic:
simpa using trivial

Premises used: trivial
-- 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}
⊢ Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0

Tactic:
have zero_mem : 0 ∈ {s : ℝ | g =ᵐ[volume.restrict (Ioc (0 : ℝ) s)] 0} := by simpa using trivial
-- 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
⊢ 0 ≤ M

Tactic:
have M_nonneg : 0 ≤ M := le_csSup M_bdd zero_mem
-- 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
rw : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 M))] 0
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0

Tactic:
rw [← restrict_Ioo_eq_restrict_Ioc]

Premises used: MeasureTheory.restrict_Ioo_eq_restrict_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
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
⊢ ∃ (u : ℕ → ℝ), StrictMono u ∧ (∀ (n : ℕ), u n < M) ∧ Tendsto u atTop (𝓝 M)

Tactic:
exists_seq_strictMono_tendsto M

Premises used: exists_seq_strictMono_tendsto
-- 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
obtain :
  ∀ (u : ℕ → ℝ) (uM : ∀ (n : ℕ), u n < M) (ulim : Tendsto u atTop (𝓝 M)),
    g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 M))] 0
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 M))] 0

Tactic:
obtain ⟨u, -, uM, ulim⟩ : ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < M) ∧ Tendsto u atTop (𝓝 M) :=
      exists_seq_strictMono_tendsto M

Premises used: exists_seq_strictMono_tendsto
-- 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
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
⊢ ∃ (s : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0 ∧ u n < s

Tactic:
exists_lt_of_lt_csSup (Set.nonempty_of_mem zero_mem) (uM n)

Premises used: Set.Mem, Filter.Eventually, Filter.EventuallyEq, exists_lt_of_lt_csSup, Set.nonempty_of_mem
-- 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
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
obtain :
  ∀ (s : ℝ) (hs : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0) (uns : u n < s),
    g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (u n)))] 0
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (u n)))] 0

Tactic:
obtain ⟨s, hs, uns⟩ : ∃ s, g =ᶠ[ae (Measure.restrict volume (Ioc 0 s))] 0 ∧ u n < s :=
        exists_lt_of_lt_csSup (Set.nonempty_of_mem zero_mem) (uM n)

Premises used: exists_lt_of_lt_csSup, Set.nonempty_of_mem
-- 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
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
s : ℝ
hs : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0
uns : u n < s
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (u n)))] 0

Tactic:
ae_restrict_of_ae_restrict_of_subset (Ioc_subset_Ioc_right uns.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 ω
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
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
s : ℝ
hs : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0
uns : u n < s
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (u n)))] 0

Tactic:
exact ae_restrict_of_ae_restrict_of_subset (Ioc_subset_Ioc_right uns.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 ω
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
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
⊢ ∀ (n : ℕ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (u n)))] 0

Tactic:
have I : ∀ n, g =ᵐ[volume.restrict (Ioc (0 : ℝ) (u n))] 0 := by
      intro n
      obtain ⟨s, hs, uns⟩ : ∃ s, g =ᶠ[ae (Measure.restrict volume (Ioc 0 s))] 0 ∧ u n < s :=
        exists_lt_of_lt_csSup (Set.nonempty_of_mem zero_mem) (uM n)
      exact ae_restrict_of_ae_restrict_of_subset (Ioc_subset_Ioc_right uns.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 ω
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
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
I : ∀ (n : ℕ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (u n)))] 0
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (⋃ (n : ℕ), Ioc 0 (u n)))] 0

Tactic:
have : g =ᵐ[volume.restrict (⋃ n, Ioc (0 : ℝ) (u n))] 0 := (ae_restrict_iUnion_iff _ _).2 I
-- 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
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
I : ∀ (n : ℕ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (u n)))] 0
this : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (⋃ (n : ℕ), Ioc 0 (u n)))] 0
apply : Ioo 0 M ⊆ ⋃ (n : ℕ), Ioc 0 (u n)
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 M))] 0

Tactic:
apply ae_restrict_of_ae_restrict_of_subset _ this

Premises used: 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 ω
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
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
I : ∀ (n : ℕ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (u n)))] 0
this : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (⋃ (n : ℕ), Ioc 0 (u n)))] 0
x : ℝ
x_pos : 0 < x
xM : x < M
⊢ ∃ (n : ℕ), x < u n

Tactic:
((tendsto_order.1 ulim).1 _ xM).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.left, 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
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
I : ∀ (n : ℕ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (u n)))] 0
this : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (⋃ (n : ℕ), Ioc 0 (u n)))] 0
x : ℝ
x_pos : 0 < x
xM : x < M
obtain : ∀ (n : ℕ) (hn : x < u n), Membership.mem (γ := Set ℝ) (⋃ (n : ℕ), Ioc 0 (u n)) x
⊢ Membership.mem (γ := Set ℝ) (⋃ (n : ℕ), Ioc 0 (u n)) x

Tactic:
obtain ⟨n, hn⟩ : ∃ n, x < u n := ((tendsto_order.1 ulim).1 _ xM).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.left, 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
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
I : ∀ (n : ℕ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (u n)))] 0
this : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (⋃ (n : ℕ), Ioc 0 (u n)))] 0
x : ℝ
x_pos : 0 < x
xM : x < M
n : ℕ
hn : x < u n
⊢ Membership.mem (γ := Set ℝ) (⋃ (n : ℕ), Ioc 0 (u n)) x

Tactic:
mem_iUnion.2 ⟨n, ⟨x_pos, hn.le⟩⟩

Premises used: Iff.mpr, Set.mem_iUnion, LT.lt.le, And.intro, 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
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
I : ∀ (n : ℕ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (u n)))] 0
this : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (⋃ (n : ℕ), Ioc 0 (u n)))] 0
x : ℝ
x_pos : 0 < x
xM : x < M
n : ℕ
hn : x < u n
⊢ Membership.mem (γ := Set ℝ) (⋃ (n : ℕ), Ioc 0 (u n)) x

Tactic:
exact mem_iUnion.2 ⟨n, ⟨x_pos, hn.le⟩⟩