awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hf : IntegrableOn f (↑I : Set (ι → ℝ)) μ
l : IntegrationParams
hl : l.bRiemann = false
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
hfg : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] g
⊢ SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)

Tactic:
haveI : SeparableSpace (range g ∪ {0} : Set E) := hg.separableSpace_range_union_singleton
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hf : IntegrableOn f (↑I : Set (ι → ℝ)) μ
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
hfg : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
rw : HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ)
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ)

Tactic:
rw [integral_congr_ae hfg]

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hf : IntegrableOn f (↑I : Set (ι → ℝ)) μ
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
hfg : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
⊢ IntegrableOn g (↑I : Set (ι → ℝ)) μ

Tactic:
have hgi : IntegrableOn g I μ := (integrable_congr hfg).1 hf
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hf : IntegrableOn f (↑I : Set (ι → ℝ)) μ
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
hfg : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ)

Tactic:
BoxIntegral.HasIntegral.congr_ae ?_ hfg.symm hl

Premises used: BoxIntegral.HasIntegral.congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hf : IntegrableOn f (↑I : Set (ι → ℝ)) μ
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
hfg : f =ᶠ[ae (μ.restrict (↑I : Set (ι → ℝ)))] g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
refine : HasIntegral I l g μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ)
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ)

Tactic:
refine BoxIntegral.HasIntegral.congr_ae ?_ hfg.symm hl

Premises used: BoxIntegral.HasIntegral.congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
⊢ 0 ∈ Set.range g ∪ {0}

Tactic:
simp
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
⊢ ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ

Tactic:
have hfi : ∀ n, IntegrableOn (f n) I μ :=
    SimpleFunc.integrable_approxOn_range hg.measurable hgi
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
⊢ ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul

Tactic:
have hfi' := fun n => ((f n).hasBoxIntegral μ I l hl).integrable
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
x : ι → ℝ
m n : ℕ
hmn : m ≤ n
rw : edist ((f n : (a : ι → ℝ) → E) x) (g x) ≤ edist ((f m : (a : ι → ℝ) → E) x) (g x)
⊢ ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
    ‖HSub.hSub (α := E) ((f m : (a : ι → ℝ) → E) x : E) (g x)‖

Tactic:
rw [← dist_eq_norm, ← dist_eq_norm, dist_nndist, dist_nndist, NNReal.coe_le_coe, ←
      ENNReal.coe_le_coe, ← edist_nndist, ← edist_nndist]

Premises used: dist_eq_norm, ENNReal.coe_le_coe, dist_nndist, edist_nndist, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
x : ι → ℝ
m n : ℕ
hmn : m ≤ n
⊢ edist ((f n : (a : ι → ℝ) → E) x) (g x) ≤ edist ((f m : (a : ι → ℝ) → E) x) (g x)

Tactic:
SimpleFunc.edist_approxOn_mono hg.measurable _ x hmn

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.SimpleFunc.edist_approxOn_mono
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
x : ι → ℝ
m n : ℕ
hmn : m ≤ n
⊢ edist ((f n : (a : ι → ℝ) → E) x) (g x) ≤ edist ((f m : (a : ι → ℝ) → E) x) (g x)

Tactic:
exact SimpleFunc.edist_approxOn_mono hg.measurable _ x hmn

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.SimpleFunc.edist_approxOn_mono
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
⊢ ∀ (x : ι → ℝ) {m n : ℕ},
    m ≤ n →
      ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
        ‖HSub.hSub (α := E) ((f m : (a : ι → ℝ) → E) x : E) (g x)‖

Tactic:
have hfg_mono : ∀ (x) {m n}, m ≤ n → ‖f n x - g x‖ ≤ ‖f m x - g x‖ := by
    intro x m n hmn
    rw [← dist_eq_norm, ← dist_eq_norm, dist_nndist, dist_nndist, NNReal.coe_le_coe, ←
      ENNReal.coe_le_coe, ← edist_nndist, ← edist_nndist]
    exact SimpleFunc.edist_approxOn_mono hg.measurable _ x hmn
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
hfg_mono :
  ∀ (x : ι → ℝ) {m n : ℕ},
    m ≤ n →
      ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
        ‖HSub.hSub (α := E) ((f m : (a : ι → ℝ) → E) x : E) (g x)‖
⊢ HasIntegral I l g μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ)

Tactic:
HasIntegral.of_mul (μ.real I + 1 + 1) fun ε ε0 => ?_

Premises used: BoxIntegral.Box.toSet, BoxIntegral.HasIntegral.of_mul, MeasureTheory.Measure.real, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
hfg_mono :
  ∀ (x : ι → ℝ) {m n : ℕ},
    m ≤ n →
      ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
        ‖HSub.hSub (α := E) ((f m : (a : ι → ℝ) → E) x : E) (g x)‖
refine :
  ∀ (ε : ℝ) (ε0 : 0 < ε),
    ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
      (∀ (c : ℝ≥0), l.RCond (r c)) ∧
        ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
          l.MemBaseSet I c (r c) π →
            π.IsPartition →
              dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
                (μ.real (↑I : Set (ι → ℝ)) + 1 + 1) * ε
⊢ HasIntegral I l g μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ)

Tactic:
refine HasIntegral.of_mul (μ.real I + 1 + 1) fun ε ε0 => ?_

Premises used: BoxIntegral.Box.toSet, BoxIntegral.HasIntegral.of_mul, MeasureTheory.Measure.real, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
hfg_mono :
  ∀ (x : ι → ℝ) {m n : ℕ},
    m ≤ n →
      ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
        ‖HSub.hSub (α := E) ((f m : (a : ι → ℝ) → E) x : E) (g x)‖
ε : ℝ
ε0 : 0 < ε
⊢ 0 ≤ ε

Tactic:
ε0.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
hfg_mono :
  ∀ (x : ι → ℝ) {m n : ℕ},
    m ≤ n →
      ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
        ‖HSub.hSub (α := E) ((f m : (a : ι → ℝ) → E) x : E) (g x)‖
ε : ℝ
ε0 : 0 < ε
lift :
  ∀ (ε : ℝ≥0) (ε0 : 0 < (↑ε : ℝ)),
    ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
      (∀ (c : ℝ≥0), l.RCond (r c)) ∧
        ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
          l.MemBaseSet I c (r c) π →
            π.IsPartition →
              dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
                (μ.real (↑I : Set (ι → ℝ)) + 1 + 1) * (↑ε : ℝ)
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
              (μ.real (↑I : Set (ι → ℝ)) + 1 + 1) * ε

Tactic:
lift ε to ℝ≥0 using ε0.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
hfg_mono :
  ∀ (x : ι → ℝ) {m n : ℕ},
    m ≤ n →
      ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
        ‖HSub.hSub (α := E) ((f m : (a : ι → ℝ) → E) x : E) (g x)‖
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
⊢ 0 < ε

Tactic:
rw [NNReal.coe_pos] at ε0

Premises used: NNReal.coe_pos
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
hfg_mono :
  ∀ (x : ι → ℝ) {m n : ℕ},
    m ≤ n →
      ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
        ‖HSub.hSub (α := E) ((f m : (a : ι → ℝ) → E) x : E) (g x)‖
ε : ℝ≥0
ε0 : 0 < ε
⊢ 0 < (↑ε : ℝ≥0∞)

Tactic:
have ε0' := ENNReal.coe_pos.2 ε0
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
hfg_mono :
  ∀ (x : ι → ℝ) {m n : ℕ},
    m ≤ n →
      ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
        ‖HSub.hSub (α := E) ((f m : (a : ι → ℝ) → E) x : E) (g x)‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < (↑ε : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), (↑‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖₊ : ℝ≥0∞) ∂μ)
    atTop (𝓝 0)

Tactic:
have : Tendsto (fun n => ∫⁻ x in I, ‖f n x - g x‖₊ ∂μ) atTop (𝓝 0) :=
      SimpleFunc.tendsto_approxOn_range_L1_enorm hg.measurable hgi
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this_3 : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
hfg_mono :
  ∀ (x : ι → ℝ) {m n : ℕ},
    m ≤ n →
      ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
        ‖HSub.hSub (α := E) ((f m : (a : ι → ℝ) → E) x : E) (g x)‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < (↑ε : ℝ≥0∞)
this :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), (↑‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖₊ : ℝ≥0∞) ∂μ)
    atTop (𝓝 0)
⊢ ∃ (N : ℕ),
    ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ ≤ (↑ε : ℝ)

Tactic:
(this.eventually (ge_mem_nhds ε0')).exists.imp fun N hN => ?_

Premises used: Exists.imp, Filter.Eventually.exists, ge_mem_nhds, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this_3 : SeparableSpace.{v} (↑(Set.range g ∪ {0}) : Type v)
hgi : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑I : Set (ι → ℝ)) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable.{u, v, v} (E := E) I l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul
hfg_mono :
  ∀ (x : ι → ℝ) {m n : ℕ},
    m ≤ n →
      ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
        ‖HSub.hSub (α := E) ((f m : (a : ι → ℝ) → E) x : E) (g x)‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < (↑ε : ℝ≥0∞)
this :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), (↑‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖₊ : ℝ≥0∞) ∂μ)
    atTop (𝓝 0)
refine :
  ∀ (N : ℕ)
    (hN :
      ∫⁻ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), (↑‖HSub.hSub (α := E) ((f N : (a : ι → ℝ) → E) x : E) (g x)‖₊ : ℝ≥0∞) ∂μ ≤
        (↑ε : ℝ≥0∞)),
    ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ ≤ (↑ε : ℝ)
⊢ ∃ (N : ℕ),
    ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ ≤ (↑ε : ℝ)

Tactic:
refine (this.eventually (ge_mem_nhds ε0')).exists.imp fun N hN => ?_

Premises used: Exists.imp, Filter.Eventually.exists, ge_mem_nhds, Filter.Tendsto.eventually