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
μ : 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∞)
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ ≤ (↑ε : ℝ)
Nx : (x : ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x) : (a : ι → ℝ) → E) x) (g x) ≤ (↑ε : ℝ)
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) :=
  fun (c : ℝ≥0) (x : ι → ℝ) ↦ Integrable.convergenceR (f := (⇑(f (Nx x)) : (a : ι → ℝ) → E)) ⋯ (↑(δ (Nx x)) : ℝ) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
n : ℕ
hn : Membership.mem (γ := Finset ℕ) (Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes) n
hNxn : ∀ J ∈ π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n, Nx (π.tag J) = n
hrn : ∀ J ∈ π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n, r c (π.tag J) = ⋯.convergenceR (↑(δ n) : ℝ) c (π.tag J)
this : l.MemBaseSet I c (⋯.convergenceR (↑(δ n) : ℝ) c) (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n)
J : Box ι
hJ : J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).boxes
⊢ Integrable.{v, u} (ε := E) (⇑(f (Nx (π.tag J))) : (a : ι → ℝ) → E) (μ.restrict (↑J : Set (ι → ℝ)))

Tactic:
(hfi _).mono_set (Prepartition.le_of_mem _ hJ)

Premises used: BoxIntegral.Prepartition.le_of_mem, MeasureTheory.IntegrableOn, MeasureTheory.IntegrableOn.mono_set
-- 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∞)
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ ≤ (↑ε : ℝ)
Nx : (x : ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x) : (a : ι → ℝ) → E) x) (g x) ≤ (↑ε : ℝ)
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) :=
  fun (c : ℝ≥0) (x : ι → ℝ) ↦ Integrable.convergenceR (f := (⇑(f (Nx x)) : (a : ι → ℝ) → E)) ⋯ (↑(δ (Nx x)) : ℝ) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
n : ℕ
hn : Membership.mem (γ := Finset ℕ) (Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes) n
hNxn : ∀ J ∈ π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n, Nx (π.tag J) = n
hrn : ∀ J ∈ π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n, r c (π.tag J) = ⋯.convergenceR (↑(δ n) : ℝ) c (π.tag J)
this : l.MemBaseSet I c (⋯.convergenceR (↑(δ n) : ℝ) c) (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n)
J : Box ι
hJ : J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).boxes
⊢ Integrable.{v, u} (ε := E) (⇑(f (Nx (π.tag J))) : (a : ι → ℝ) → E) (μ.restrict (↑J : Set (ι → ℝ)))

Tactic:
exact (hfi _).mono_set (Prepartition.le_of_mem _ hJ)

Premises used: BoxIntegral.Prepartition.le_of_mem, MeasureTheory.IntegrableOn.mono_set
-- 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∞)
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ ≤ (↑ε : ℝ)
Nx : (x : ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x) : (a : ι → ℝ) → E) x) (g x) ≤ (↑ε : ℝ)
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) :=
  fun (c : ℝ≥0) (x : ι → ℝ) ↦ Integrable.convergenceR (f := (⇑(f (Nx x)) : (a : ι → ℝ) → E)) ⋯ (↑(δ (Nx x)) : ℝ) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
⊢ dist.{v} (α := E) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
      (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
    (↑ε : ℝ)

Tactic:
le_trans ?_ hN₀

Premises used: le_trans
-- 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∞)
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ ≤ (↑ε : ℝ)
Nx : (x : ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x) : (a : ι → ℝ) → E) x) (g x) ≤ (↑ε : ℝ)
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) :=
  fun (c : ℝ≥0) (x : ι → ℝ) ↦ Integrable.convergenceR (f := (⇑(f (Nx x)) : (a : ι → ℝ) → E)) ⋯ (↑(δ (Nx x)) : ℝ) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
refine_3 :
  dist.{v} (α := E) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
      (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
    ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ
⊢ dist.{v} (α := E) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
      (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
    (↑ε : ℝ)

Tactic:
refine le_trans ?_ hN₀

Premises used: le_trans
-- 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∞)
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ ≤ (↑ε : ℝ)
Nx : (x : ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x) : (a : ι → ℝ) → E) x) (g x) ≤ (↑ε : ℝ)
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) :=
  fun (c : ℝ≥0) (x : ι → ℝ) ↦ Integrable.convergenceR (f := (⇑(f (Nx x)) : (a : ι → ℝ) → E)) ⋯ (↑(δ (Nx x)) : ℝ) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
⊢ ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑J : Set (ι → ℝ)) μ

Tactic:
have hfi : ∀ (n), ∀ J ∈ π, IntegrableOn (f n) (↑J) μ := fun n J hJ =>
      (hfi n).mono_set (π.le_of_mem' J hJ)
-- 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_1 : ∀ (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∞)
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ ≤ (↑ε : ℝ)
Nx : (x : ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x) : (a : ι → ℝ) → E) x) (g x) ≤ (↑ε : ℝ)
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) :=
  fun (c : ℝ≥0) (x : ι → ℝ) ↦ Integrable.convergenceR (f := (⇑(f (Nx x)) : (a : ι → ℝ) → E)) ⋯ (↑(δ (Nx x)) : ℝ) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
hfi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑J : Set (ι → ℝ)) μ
⊢ ∀ J ∈ π, IntegrableOn g (↑J : Set (ι → ℝ)) μ

Tactic:
have hgi : ∀ J ∈ π, IntegrableOn g (↑J) μ := fun J hJ => hgi.mono_set (π.le_of_mem' J hJ)
-- 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_1 : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi_1 : ∀ (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∞)
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ ≤ (↑ε : ℝ)
Nx : (x : ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x) : (a : ι → ℝ) → E) x) (g x) ≤ (↑ε : ℝ)
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) :=
  fun (c : ℝ≥0) (x : ι → ℝ) ↦ Integrable.convergenceR (f := (⇑(f (Nx x)) : (a : ι → ℝ) → E)) ⋯ (↑(δ (Nx x)) : ℝ) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
hfi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑J : Set (ι → ℝ)) μ
hgi : ∀ J ∈ π, IntegrableOn g (↑J : Set (ι → ℝ)) μ
⊢ ∀ (n : ℕ),
    ∀ J ∈ π,
      IntegrableOn (ε := ℝ) (fun (x : ι → ℝ) ↦ ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖)
        (↑J : Set (ι → ℝ)) μ

Tactic:
have hfgi : ∀ (n), ∀ J ∈ π, IntegrableOn (fun x => ‖f n x - g x‖) J μ := fun n J hJ =>
      ((hfi n J hJ).sub (hgi J hJ)).norm
-- 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_1 : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi_1 : ∀ (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∞)
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ ≤ (↑ε : ℝ)
Nx : (x : ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x) : (a : ι → ℝ) → E) x) (g x) ≤ (↑ε : ℝ)
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) :=
  fun (c : ℝ≥0) (x : ι → ℝ) ↦ Integrable.convergenceR (f := (⇑(f (Nx x)) : (a : ι → ℝ) → E)) ⋯ (↑(δ (Nx x)) : ℝ) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
hfi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑J : Set (ι → ℝ)) μ
hgi : ∀ J ∈ π, IntegrableOn g (↑J : Set (ι → ℝ)) μ
hfgi :
  ∀ (n : ℕ),
    ∀ J ∈ π,
      IntegrableOn (ε := ℝ) (fun (x : ι → ℝ) ↦ ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖)
        (↑J : Set (ι → ℝ)) μ
refine_3 :
  dist.{v} (α := E) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
      (∑ i ∈ π.boxes, ∫ (x : ι → ℝ) in (↑i : Set (ι → ℝ)), g x ∂μ) ≤
    ∑ i ∈ π.boxes, ∫ (x : ι → ℝ) in (↑i : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ
⊢ dist.{v} (α := E) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
      (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
    ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ

Tactic:
rw [← hπp.iUnion_eq, Prepartition.iUnion_def',
      integral_biUnion_finset π.boxes (fun J _ => J.measurableSet_coe) π.pairwiseDisjoint hgi,
      integral_biUnion_finset π.boxes (fun J _ => J.measurableSet_coe) π.pairwiseDisjoint (hfgi _)]

Premises used: BoxIntegral.Box.measurableSet_coe, BoxIntegral.Prepartition.IsPartition.iUnion_eq, MeasureTheory.integral_biUnion_finset, BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.Prepartition.boxes, BoxIntegral.Prepartition.pairwiseDisjoint, BoxIntegral.Prepartition.iUnion_def'
-- 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_1 : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi_1 : ∀ (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∞)
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ ≤ (↑ε : ℝ)
Nx : (x : ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x) : (a : ι → ℝ) → E) x) (g x) ≤ (↑ε : ℝ)
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) :=
  fun (c : ℝ≥0) (x : ι → ℝ) ↦ Integrable.convergenceR (f := (⇑(f (Nx x)) : (a : ι → ℝ) → E)) ⋯ (↑(δ (Nx x)) : ℝ) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
hfi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑J : Set (ι → ℝ)) μ
hgi : ∀ J ∈ π, IntegrableOn g (↑J : Set (ι → ℝ)) μ
hfgi :
  ∀ (n : ℕ),
    ∀ J ∈ π,
      IntegrableOn (ε := ℝ) (fun (x : ι → ℝ) ↦ ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖)
        (↑J : Set (ι → ℝ)) μ
⊢ dist.{v} (α := E) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
      (∑ i ∈ π.boxes, ∫ (x : ι → ℝ) in (↑i : Set (ι → ℝ)), g x ∂μ) ≤
    ∑ i ∈ π.boxes, ∫ (x : ι → ℝ) in (↑i : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ

Tactic:
dist_sum_sum_le_of_le _ fun J hJ => ?_

Premises used: dist_sum_sum_le_of_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_1 : IntegrableOn g (↑I : Set (ι → ℝ)) μ
f : ℕ → SimpleFunc.{u, v} (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi_1 : ∀ (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∞)
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ ≤ (↑ε : ℝ)
Nx : (x : ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x) : (a : ι → ℝ) → E) x) (g x) ≤ (↑ε : ℝ)
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c_1 : ℝ≥0
hδc : HasSum δ c_1
hcε : c_1 < ε
r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type) :=
  fun (c : ℝ≥0) (x : ι → ℝ) ↦ Integrable.convergenceR (f := (⇑(f (Nx x)) : (a : ι → ℝ) → E)) ⋯ (↑(δ (Nx x)) : ℝ) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
hfi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn.{u, v} (ε := E) (⇑(f n) : (a : ι → ℝ) → E) (↑J : Set (ι → ℝ)) μ
hgi : ∀ J ∈ π, IntegrableOn g (↑J : Set (ι → ℝ)) μ
hfgi :
  ∀ (n : ℕ),
    ∀ J ∈ π,
      IntegrableOn (ε := ℝ) (fun (x : ι → ℝ) ↦ ‖HSub.hSub (α := E) ((f n : (a : ι → ℝ) → E) x : E) (g x)‖)
        (↑J : Set (ι → ℝ)) μ
refine_3 :
  ∀ (J : Box ι) (hJ : J ∈ π.boxes),
    dist.{v} (α := E) (∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
        (∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), g x ∂μ) ≤
      ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ
⊢ dist.{v} (α := E) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
      (∑ i ∈ π.boxes, ∫ (x : ι → ℝ) in (↑i : Set (ι → ℝ)), g x ∂μ) ≤
    ∑ i ∈ π.boxes, ∫ (x : ι → ℝ) in (↑i : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ

Tactic:
refine dist_sum_sum_le_of_le _ fun J hJ => ?_

Premises used: dist_sum_sum_le_of_le