awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
b c : ι → α
B : α
hb : Tendsto b l (𝓝 B)
hc : Tendsto c l atBot
⊢ ∀ᵐ (x : α) ∂μ.restrict (Iio B), ∀ᶠ (i : ι) in l, x ∈ Ico (c i) (b i)
have refine : ∀ (_x : α) (hx : _x ∈ Iio B), ∀ᶠ (i : ι) in l, _x ∈ Ico (c i) (b i)
Tactic: refine (ae_restrict_mem measurableSet_Iio).mono fun _x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
b c : ι → α
B : α
hb : Tendsto b l (𝓝 B)
hc : Tendsto c l atBot
_x : α
hx : _x ∈ Iio B
⊢ ∀ᶠ (i : ι) in l, _x ∈ Ico (c i) (b i)
have simp : (∀ᶠ (x : ι) in l, c x ≤ _x) ∧ ∀ᶠ (x : ι) in l, _x < b x
Tactic: simp only [mem_Ico, eventually_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
d : ι → α
B : α
hd : Tendsto d l atTop
inst_5 : NoMaxOrder α
⊢ ∀ᵐ (x : α) ∂μ.restrict (Ici B), ∀ᶠ (i : ι) in l, x ∈ Ico B (d i)
have refine : ∀ (_x : α) (hx : _x ∈ Ici B), ∀ᶠ (i : ι) in l, _x ∈ Ico B (d i)
Tactic: refine (ae_restrict_mem measurableSet_Ici).mono fun _x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
d : ι → α
B : α
hd : Tendsto d l atTop
inst_5 : NoMaxOrder α
_x : α
hx : _x ∈ Ici B
⊢ ∀ᶠ (i : ι) in l, _x ∈ Ico B (d i)
have simp : (∀ᶠ (x : ι) in l, B ≤ _x) ∧ ∀ᶠ (x : ι) in l, _x < d x
Tactic: simp only [mem_Ico, eventually_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : l.IsCountablyGenerated
inst_3 : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))
⊢ AEMeasurable f μ
have obtain : ∀ (u : ℕ → ι) (hu : Tendsto u atTop l), AEMeasurable f μ
Tactic: obtain ⟨u, hu⟩ := l.exists_seq_tendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : l.IsCountablyGenerated
inst_3 : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
⊢ AEMeasurable f μ
have this : AEMeasurable f (μ.restrict (⋃ (i : ℕ), φ (u i)))
Tactic: have := aemeasurable_iUnion_iff.mpr fun n : ℕ => hfm (u n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : l.IsCountablyGenerated
inst_3 : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
this : AEMeasurable f (μ.restrict (⋃ (i : ℕ), φ (u i)))
⊢ AEMeasurable f μ
have hs : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x
Tactic: rwa [Measure.restrict_eq_self_of_ae_mem] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : l.IsCountablyGenerated
inst_3 : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
this : AEMeasurable f (μ.restrict (⋃ (i : ℕ), φ (u i)))
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ∀ᶠ (i : ι) in l, x ∈ φ i) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x) x} x}
    a
Tactic: filter_upwards [hφ.ae_eventually_mem] with x hx using
    mem_iUnion.mpr (hu.eventually hx).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : l.IsCountablyGenerated
inst_3 : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
this : AEMeasurable f (μ.restrict (⋃ (i : ℕ), φ (u i)))
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ∀ᶠ (i : ι) in l, x ∈ φ i) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x
have h₁ : ∀ (a : α), (∀ᶠ (i : ι) in l, a ∈ φ i) → Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) a
Tactic: filter_upwards [hφ.ae_eventually_mem] with x hx using
    mem_iUnion.mpr (hu.eventually hx).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : l.IsCountablyGenerated
inst_4 : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEStronglyMeasurable f (μ.restrict (φ i))
⊢ AEStronglyMeasurable f μ
have obtain : ∀ (u : ℕ → ι) (hu : Tendsto u atTop l), AEStronglyMeasurable f μ
Tactic: obtain ⟨u, hu⟩ := l.exists_seq_tendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : l.IsCountablyGenerated
inst_4 : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEStronglyMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
⊢ AEStronglyMeasurable f μ
have this : AEStronglyMeasurable f (μ.restrict (⋃ (i : ℕ), φ (u i)))
Tactic: have := aestronglyMeasurable_iUnion_iff.mpr fun n : ℕ => hfm (u n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : l.IsCountablyGenerated
inst_4 : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEStronglyMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
this : AEStronglyMeasurable f (μ.restrict (⋃ (i : ℕ), φ (u i)))
⊢ AEStronglyMeasurable f μ
have hs : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x
Tactic: rwa [Measure.restrict_eq_self_of_ae_mem] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : l.IsCountablyGenerated
inst_4 : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEStronglyMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
this : AEStronglyMeasurable f (μ.restrict (⋃ (i : ℕ), φ (u i)))
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ∀ᶠ (i : ι) in l, x ∈ φ i) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x) x} x}
    a
Tactic: filter_upwards [hφ.ae_eventually_mem] with x hx using mem_iUnion.mpr (hu.eventually hx).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : l.IsCountablyGenerated
inst_4 : l.NeBot
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEStronglyMeasurable f (μ.restrict (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
this : AEStronglyMeasurable f (μ.restrict (⋃ (i : ℕ), φ (u i)))
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ∀ᶠ (i : ι) in l, x ∈ φ i) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x
have h₁ : ∀ (a : α), (∀ᶠ (i : ι) in l, a ∈ φ i) → Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) a
Tactic: filter_upwards [hφ.ae_eventually_mem] with x hx using mem_iUnion.mpr (hu.eventually hx).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
φ : ℕ → Set α
hφ : AECover μ atTop φ
hmono : Monotone φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
F : (n : ℕ) → (x : α) → ℝ≥0∞ := fun (n : ℕ) ↦ (φ n).indicator f
key₁ : ∀ (n : ℕ), AEMeasurable (F n) μ
x : α
_i _j : ℕ
hij : _i ≤ _j
⊢ (φ _i).indicator f x ≤ (φ _j).indicator f x
have h₁ : 0 ≤ f x
Tactic: grw [(hmono hij).subset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
φ : ℕ → Set α
hφ : AECover μ atTop φ
hmono : Monotone φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
F : (n : ℕ) → (x : α) → ℝ≥0∞ := fun (n : ℕ) ↦ (φ n).indicator f
key₁ : ∀ (n : ℕ), AEMeasurable (F n) μ
x : α
_i _j : ℕ
hij : _i ≤ _j
h₁ : 0 ≤ f x
⊢ (φ _i).indicator f x ≤ (φ _j).indicator f x
have grw : (φ _j).indicator f x ≤ (φ _j).indicator f x
Tactic: grw [(hmono hij).subset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
⊢ Tendsto (fun (x : ℕ) ↦ ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
have lim₁ : Tendsto (fun (i : ℕ) ↦ ∫⁻ (x : α) in ⋂ k ∈ Ici i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
Tactic: have lim₁ := lintegral_tendsto_of_monotone_of_nat hφ.biInter_Ici_aecover
    (fun i j hij => biInter_subset_biInter_left (Ici_subset_Ici.mpr hij)) hfm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
lim₁ : Tendsto (fun (i : ℕ) ↦ ∫⁻ (x : α) in ⋂ k ∈ Ici i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ Tendsto (fun (x : ℕ) ↦ ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
have lim₂ : Tendsto (fun (i : ℕ) ↦ ∫⁻ (x : α) in ⋃ k ∈ Iic i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
Tactic: have lim₂ := lintegral_tendsto_of_monotone_of_nat hφ.biUnion_Iic_aecover
    (fun i j hij => biUnion_subset_biUnion_left (Iic_subset_Iic.mpr hij)) hfm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
lim₁ : Tendsto (fun (i : ℕ) ↦ ∫⁻ (x : α) in ⋂ k ∈ Ici i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
lim₂ : Tendsto (fun (i : ℕ) ↦ ∫⁻ (x : α) in ⋃ k ∈ Iic i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ Tendsto (fun (x : ℕ) ↦ ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
have refine_1 : ∀ (n : ℕ), ∫⁻ (x : α) in ⋂ k ∈ Ici n, φ k, f x ∂μ ≤ ∫⁻ (x : α) in φ n, f x ∂μ
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le lim₁ lim₂ (fun n ↦ ?_) fun n ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
lim₁ : Tendsto (fun (i : ℕ) ↦ ∫⁻ (x : α) in ⋂ k ∈ Ici i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
lim₂ : Tendsto (fun (i : ℕ) ↦ ∫⁻ (x : α) in ⋃ k ∈ Iic i, φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
refine_1 : ∀ (n : ℕ), ∫⁻ (x : α) in ⋂ k ∈ Ici n, φ k, f x ∂μ ≤ ∫⁻ (x : α) in φ n, f x ∂μ
⊢ Tendsto (fun (x : ℕ) ↦ ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
have refine_2 : ∀ (n : ℕ), ∫⁻ (x : α) in φ n, f x ∂μ ≤ ∫⁻ (x : α) in ⋃ k ∈ Iic n, φ k, f x ∂μ
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le lim₁ lim₂ (fun n ↦ ?_) fun n ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : Nonempty ι
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
⊢ ⨆ (i : ι), ∫⁻ (x : α) in φ i, f x ∂μ = ∫⁻ (x : α), f x ∂μ
have this : Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
Tactic: have := hφ.lintegral_tendsto_of_countably_generated hfm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : Nonempty ι
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
this : Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ ⨆ (i : ι), ∫⁻ (x : α) in φ i, f x ∂μ = ∫⁻ (x : α), f x ∂μ
have refine : ∀ (w : ℝ≥0∞) (hw : w < ∫⁻ (x : α), f x ∂μ), ∃ (i : ι), w < ∫⁻ (x : α) in φ i, f x ∂μ
Tactic: refine ciSup_eq_of_forall_le_of_forall_lt_exists_gt
    (fun i => lintegral_mono' Measure.restrict_le_self le_rfl) fun w hw => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I
⊢ Integrable f μ
have refine : Tendsto (fun (c : ι) ↦ ∫⁻ (x : α) in φ c, ‖f x‖ₑ ∂μ) l (𝓝 (∫⁻ (a : α), ‖f a‖ₑ ∂μ))
Tactic: refine ⟨hfm, (le_of_tendsto ?_ hbounded).trans_lt ENNReal.ofReal_lt_top⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (𝓝 (ENNReal.ofReal I))
⊢ Integrable f μ
have refine : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal (max 1 (I + 1))
Tactic: refine hφ.integrable_of_lintegral_enorm_bounded (max 1 (I + 1)) hfm ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (𝓝 (ENNReal.ofReal I))
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal (max 1 (I + 1))
have refine : ENNReal.ofReal I < ENNReal.ofReal (max 1 (I + 1))
Tactic: refine htendsto.eventually (ge_mem_nhds ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (𝓝 (ENNReal.ofReal I))
⊢ ENNReal.ofReal I < ENNReal.ofReal (max 1 (I + 1))
have refine : I < max 1 (I + 1)
Tactic: refine (ENNReal.ofReal_lt_ofReal_iff (lt_max_of_lt_left zero_lt_one)).2 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
⊢ Integrable f μ
have hfm : AEStronglyMeasurable f μ
Tactic: have hfm : AEStronglyMeasurable f μ :=
    hφ.aestronglyMeasurable fun i => (hfi i).aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
hfm : AEStronglyMeasurable f μ
⊢ Integrable f μ
have refine : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I
Tactic: refine hφ.integrable_of_lintegral_enorm_bounded I hfm ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
| ∫ (x : α) in φ i, ‖f x‖ ∂μ
have rw : (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ).toReal
Tactic: rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun x => @norm_nonneg E _ (f x))
        hfm.norm.restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
hfm : AEStronglyMeasurable f μ
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I
have hbounded₁ : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ).toReal ≤ I
Tactic: conv at hbounded in integral _ _ =>
    rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun x => @norm_nonneg E _ (f x))
        hfm.norm.restrict]
Cleared hypotheses: hbounded, hfm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
a : α
| ENNReal.ofReal ‖f a‖
have rw : (↑‖f a‖₊ : ℝ≥0∞)
Tactic: rw [← coe_nnnorm, ENNReal.ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I
have hbounded₁ : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I
Tactic: conv at hbounded in ENNReal.ofReal _ =>
    rw [← coe_nnnorm, ENNReal.ofReal_coe_nnreal]
Cleared hypotheses: hbounded, hfm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I
have refine : ∀ (i : ι) (hi : (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I), ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I
Tactic: refine hbounded.mono fun i hi => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
hi : (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I
⊢ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I
have rw : ENNReal.ofReal (∫⁻ (a : α) in φ i, ‖f a‖ₑ ∂μ).toReal ≤ ENNReal.ofReal I
Tactic: rw [← ENNReal.ofReal_toReal <| ne_top_of_lt <| hasFiniteIntegral_iff_enorm.mp (hfi i).2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f μ
h : Tendsto.{u_2, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
⊢ Tendsto.{u_2, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : α) in φ i, f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
have h₁ : ∀ (x : ι), Eq.{u_3 + 1} (α := E) (∫ (x : α) in φ x, f x ∂μ) (∫ (x_1 : α), (φ x).indicator f x_1 ∂μ)
Tactic: convert! h using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f μ
h : Tendsto.{u_2, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
x : ι
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in φ x, f x ∂μ) (∫ (x_1 : α), (φ x).indicator f x_1 ∂μ)
have h₁ : Eq.{u_3 + 1} (α := E) (∫ (x : α) in φ x, f x ∂μ) (∫ (x : α) in φ x, f x ∂μ)
Tactic: rw [integral_indicator (hφ.measurableSet _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
⊢ Integrable f μ
have hφ : AECover μ l fun (i : ι) ↦ Ioc (a i) (b i)
Tactic: have hφ : AECover μ l _ := aecover_Ioc ha hb