awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : OpensMeasurableSpace α
a b : ι → α
A B : α
inst_5 : NoAtoms μ
ha : Tendsto a l (𝓝 A)
hb : Tendsto b l (𝓝 B)
⊢ AECover (μ.restrict (Icc A B)) l fun (i : ι) ↦ Ioo (a i) (b i)

Tactic:
(aecover_Ioo_of_Ioo ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Icc).ge

Premises used: Eq.ge, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioo_ae_eq_Icc, MeasureTheory.aecover_Ioo_of_Ioo, MeasureTheory.AECover.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ι → Set α
hφ : AECover μ l φ
s : Set α
⊢ AECover (μ.restrict s) l φ

Tactic:
hφ.mono Measure.restrict_le_self

Premises used: MeasureTheory.Measure.restrict_le_self, MeasureTheory.AECover.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
s : Set α
φ : ι → Set α
hs : MeasurableSet s
ae_eventually_mem : ∀ᵐ (x : α) ∂μ, x ∈ s → ∀ᶠ (n : ι) in l, x ∈ φ n
measurable : ∀ (n : ι), MeasurableSet (φ n)
rwa rwa₁ rwa₂ rwa₃ : ∀ᵐ (x : α) ∂μ, x ∈ s → ∀ᶠ (i : ι) in l, x ∈ φ i
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ∀ᶠ (i : ι) in l, x ∈ φ i

Tactic:
rwa [ae_restrict_iff' hs]

Premises used: MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ι → Set α
hφ : AECover μ l φ
s : Set α
hs : MeasurableSet s
⊢ AECover (μ.restrict s) l fun (i : ι) ↦ φ i ∩ s

Tactic:
aecover_restrict_of_ae_imp hs
    (hφ.ae_eventually_mem.mono fun _x hx hxs => hx.mono fun _i hi => ⟨hi, hxs⟩) fun i =>
    (hφ.measurableSet i).inter hs

Premises used: MeasureTheory.AECover.measurableSet, Filter.Eventually.mono, MeasureTheory.AECover.ae_eventually_mem, And.intro, MeasureTheory.aecover_restrict_of_ae_imp, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst_1 : Zero β
inst_2 : TopologicalSpace β
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ι) ↦ (φ i).indicator f x) l (𝓝 (f x))

Tactic:
hφ.ae_eventually_mem.mono fun _x hx =>
    tendsto_const_nhds.congr' <| hx.mono fun _n hn => (indicator_of_mem hn _).symm

Premises used: tendsto_const_nhds, Filter.Eventually.mono, Set.indicator_of_mem, MeasureTheory.AECover.ae_eventually_mem, Filter.Tendsto.congr', Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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))
obtain : ∀ (u : ℕ → ι) (hu : Tendsto u atTop l), AEMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
obtain ⟨u, hu⟩ := l.exists_seq_tendsto

Premises used: Filter.exists_seq_tendsto
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 (μ.restrict (⋃ (i : ℕ), φ (u i)))

Tactic:
have := aemeasurable_iUnion_iff.mpr fun n : ℕ => hfm (u n)
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)))
hs : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x
⊢ AEMeasurable f μ

Tactic:
rwa [Measure.restrict_eq_self_of_ae_mem] at this

Premises used: MeasureTheory.Measure.restrict_eq_self_of_ae_mem
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 : α
hx : ∀ᶠ (i : ι) in l, x ∈ φ i
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x

Tactic:
mem_iUnion.mpr (hu.eventually hx).exists

Premises used: Iff.mpr, Set.mem_iUnion, Filter.Eventually.exists, Filter.Tendsto.eventually
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
h₁ h₂ : ∀ (x : α) (hx : ∀ᶠ (i : ι) in l, x ∈ φ i), Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x

Tactic:
filter_upwards [hφ.ae_eventually_mem] with x hx using
    mem_iUnion.mpr (hu.eventually hx).exists

Premises used: MeasureTheory.AECover.ae_eventually_mem
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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))
obtain : ∀ (u : ℕ → ι) (hu : Tendsto u atTop l), AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f μ

Tactic:
obtain ⟨u, hu⟩ := l.exists_seq_tendsto

Premises used: Filter.exists_seq_tendsto
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 (μ.restrict (⋃ (i : ℕ), φ (u i)))

Tactic:
have := aestronglyMeasurable_iUnion_iff.mpr fun n : ℕ => hfm (u n)
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)))
hs : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x
⊢ AEStronglyMeasurable f μ

Tactic:
rwa [Measure.restrict_eq_self_of_ae_mem] at this

Premises used: MeasureTheory.Measure.restrict_eq_self_of_ae_mem
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 : α
hx : ∀ᶠ (i : ι) in l, x ∈ φ i
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x

Tactic:
mem_iUnion.mpr (hu.eventually hx).exists

Premises used: Iff.mpr, Set.mem_iUnion, Filter.Eventually.exists, Filter.Tendsto.eventually
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
h₁ h₂ : ∀ (x : α) (hx : ∀ᶠ (i : ι) in l, x ∈ φ i), Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) (⋃ (i : ℕ), φ (u i)) x

Tactic:
filter_upwards [hφ.ae_eventually_mem] with x hx using mem_iUnion.mpr (hu.eventually hx).exists

Premises used: MeasureTheory.AECover.ae_eventually_mem
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : Countable ι
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : Preorder ι
φ : ι → Set α
hφ : AECover μ atTop φ
⊢ AECover μ atTop fun (n : ι) ↦ ⋃ k ∈ Iic n, φ k

Tactic:
hφ.superset (fun _ ↦ subset_biUnion_of_mem self_mem_Iic) fun _ ↦ .biUnion (to_countable _)
    fun _ _ ↦ (hφ.2 _)

Premises used: Set.self_mem_Iic, Set.subset_biUnion_of_mem, MeasureTheory.AECover.measurableSet, MeasureTheory.AECover.superset, Set.to_countable, MeasurableSet.biUnion, Set.Iic
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : Countable ι
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : Preorder ι
φ : ι → Set α
hφ : AECover μ atTop φ
x : α
h : ∀ᶠ (i : ι) in atTop, x ∈ φ i
⊢ ∀ᶠ (i : ι) in atTop, Membership.mem (γ := Set α) (⋂ k ∈ Ici i, φ k) x

Tactic:
simpa only [mem_iInter, mem_Ici, eventually_forall_ge_atTop]

Premises used: Set.mem_iInter, Set.mem_Ici, Filter.eventually_forall_ge_atTop
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
dsimp : (φ _i).indicator f x ≤ (φ _j).indicator f x
⊢ LE.le (α := ℝ≥0∞) ((fun (n : ℕ) ↦ F n x) _i) ((fun (n : ℕ) ↦ F n x) _j)

Tactic:
dsimp [F]
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
grw grw₁ : (φ _j).indicator f x ≤ (φ _j).indicator f x
⊢ (φ _i).indicator f x ≤ (φ _j).indicator f x

Tactic:
grw [(hmono hij).subset]

Premises used: LE.le.subset
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 (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
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 ∂μ))

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le lim₁ lim₂ (fun n ↦ ?_) fun n ↦ ?_

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 ∂μ
refine_2 : ∀ (n : ℕ), ∫⁻ (x : α) in φ n, f x ∂μ ≤ ∫⁻ (x : α) in ⋃ k ∈ Iic n, φ k, f x ∂μ
⊢ Tendsto (fun (x : ℕ) ↦ ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le lim₁ lim₂ (fun n ↦ ?_) fun n ↦ ?_

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 ∂μ))
n : ℕ
⊢ ∫⁻ (x : α) in ⋂ k ∈ Ici n, φ k, f x ∂μ ≤ ∫⁻ (x : α) in φ n, f x ∂μ

Tactic:
lintegral_mono_set (biInter_subset_of_mem self_mem_Ici)

Premises used: Set.biInter_subset_of_mem, MeasureTheory.lintegral_mono_set, Set.self_mem_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 ∂μ))
n : ℕ
⊢ ∫⁻ (x : α) in φ n, f x ∂μ ≤ ∫⁻ (x : α) in ⋃ k ∈ Iic n, φ k, f x ∂μ

Tactic:
lintegral_mono_set (subset_biUnion_of_mem self_mem_Iic)

Premises used: Set.self_mem_Iic, Set.subset_biUnion_of_mem, MeasureTheory.lintegral_mono_set
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 ∂μ))
n : ℕ
⊢ ∫⁻ (x : α) in ⋂ k ∈ Ici n, φ k, f x ∂μ ≤ ∫⁻ (x : α) in φ n, f x ∂μ

Tactic:
exacts [lintegral_mono_set (biInter_subset_of_mem self_mem_Ici),
    lintegral_mono_set (subset_biUnion_of_mem self_mem_Iic)]

Premises used: Set.self_mem_Iic, Set.subset_biUnion_of_mem, Set.biInter_subset_of_mem, MeasureTheory.lintegral_mono_set, Set.self_mem_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))

Tactic:
tendsto_of_seq_tendsto fun _u hu => (hφ.comp_tendsto hu).lintegral_tendsto_of_nat hfm

Premises used: MeasureTheory.AECover.comp_tendsto, Filter.tendsto_of_seq_tendsto, MeasureTheory.AECover.lintegral_tendsto_of_nat
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : l.NeBot
inst_2 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
I : ℝ≥0∞
hfm : AEMeasurable f μ
htendsto : Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 I)
⊢ ∫⁻ (x : α), f x ∂μ = I

Tactic:
tendsto_nhds_unique (hφ.lintegral_tendsto_of_countably_generated hfm) htendsto

Premises used: MeasureTheory.AECover.lintegral_tendsto_of_countably_generated, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 μ
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))

Tactic:
have := hφ.lintegral_tendsto_of_countably_generated hfm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 ∂μ

Tactic:
ciSup_eq_of_forall_le_of_forall_lt_exists_gt
    (fun i => lintegral_mono' Measure.restrict_le_self le_rfl) fun w hw => ?_

Premises used: le_rfl, ciSup_eq_of_forall_le_of_forall_lt_exists_gt, MeasureTheory.lintegral_mono', MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 ∂μ))
refine : ∀ (w : ℝ≥0∞) (hw : w < ∫⁻ (x : α), f x ∂μ), ∃ (i : ι), w < ∫⁻ (x : α) in φ i, f x ∂μ
⊢ ⨆ (i : ι), ∫⁻ (x : α) in φ i, f x ∂μ = ∫⁻ (x : α), 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 => ?_

Premises used: le_rfl, ciSup_eq_of_forall_le_of_forall_lt_exists_gt, MeasureTheory.lintegral_mono', MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 ∂μ))
w : ℝ≥0∞
hw : w < ∫⁻ (x : α), f x ∂μ
⊢ ∃ (i : ι), w < ∫⁻ (x : α) in φ i, f x ∂μ

Tactic:
(this.eventually_const_lt hw).exists

Premises used: Filter.Tendsto.eventually_const_lt, Filter.Eventually.exists
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 ∂μ))
w : ℝ≥0∞
hw : w < ∫⁻ (x : α), f x ∂μ
⊢ ∃ (i : ι), w < ∫⁻ (x : α) in φ i, f x ∂μ

Tactic:
exact (this.eventually_const_lt hw).exists

Premises used: Filter.Tendsto.eventually_const_lt, Filter.Eventually.exists
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 μ

Tactic:
⟨hfm, (le_of_tendsto ?_ hbounded).trans_lt ENNReal.ofReal_lt_top⟩

Premises used: ENNReal.ofReal_lt_top, MeasureTheory.Integrable, le_of_tendsto, And.intro, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
refine : Tendsto (fun (c : ι) ↦ ∫⁻ (x : α) in φ c, ‖f x‖ₑ ∂μ) l (𝓝 (∫⁻ (a : α), ‖f a‖ₑ ∂μ))
⊢ Integrable f μ

Tactic:
refine ⟨hfm, (le_of_tendsto ?_ hbounded).trans_lt ENNReal.ofReal_lt_top⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
⊢ Tendsto (fun (c : ι) ↦ ∫⁻ (x : α) in φ c, ‖f x‖ₑ ∂μ) l (𝓝 (∫⁻ (a : α), ‖f a‖ₑ ∂μ))

Tactic:
hφ.lintegral_tendsto_of_countably_generated hfm.enorm

Premises used: MeasureTheory.AECover.lintegral_tendsto_of_countably_generated, MeasureTheory.AEStronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
⊢ Tendsto (fun (c : ι) ↦ ∫⁻ (x : α) in φ c, ‖f x‖ₑ ∂μ) l (𝓝 (∫⁻ (a : α), ‖f a‖ₑ ∂μ))

Tactic:
exact hφ.lintegral_tendsto_of_countably_generated hfm.enorm

Premises used: MeasureTheory.AECover.lintegral_tendsto_of_countably_generated, MeasureTheory.AEStronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 μ

Tactic:
hφ.integrable_of_lintegral_enorm_bounded (max 1 (I + 1)) hfm ?_

Premises used: HAdd.hAdd, Max.max, MeasureTheory.AECover.integrable_of_lintegral_enorm_bounded, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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))
refine : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal (max 1 (I + 1))
⊢ Integrable f μ

Tactic:
refine hφ.integrable_of_lintegral_enorm_bounded (max 1 (I + 1)) hfm ?_

Premises used: HAdd.hAdd, Max.max, MeasureTheory.AECover.integrable_of_lintegral_enorm_bounded, OfNat.ofNat