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 : 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 :
  dist (integralSum g μ.toBoxAdditive.toSMul π)
          (∑ J ∈ π.boxes,
            HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) +
        dist.{v} (α := E)
          (∑ J ∈ π.boxes,
            HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E))
          (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ) +
      dist.{v} (α := E) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
        (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
    (μ.real (↑I : Set (ι → ℝ)) + 1 + 1) * (↑ε : ℝ)
⊢ dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
    (μ.real (↑I : Set (ι → ℝ)) + 1 + 1) * (↑ε : ℝ)

Tactic:
refine (dist_triangle4 _ (∑ J ∈ π.boxes, μ.real J • f (Nx <| π.tag J) (π.tag J))
    (∑ J ∈ π.boxes, ∫ x in J, f (Nx <| π.tag J) x ∂μ) _).trans ?_

Premises used: BoxIntegral.Box.toSet, dist_triangle4, MeasureTheory.Measure.real, MeasureTheory.Measure.restrict, BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.TaggedPrepartition.tag, BoxIntegral.Prepartition.boxes, MeasureTheory.integral, HSMul.hSMul, LE.le.trans, DFunLike.coe, Finset.sum
-- 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
rw :
  dist (integralSum g μ.toBoxAdditive.toSMul π)
          (∑ J ∈ π.boxes,
            HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) +
        dist.{v} (α := E)
          (∑ J ∈ π.boxes,
            HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E))
          (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ) +
      dist.{v} (α := E) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
        (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
    μ.real (↑I : Set (ι → ℝ)) * (↑ε : ℝ) + (↑ε : ℝ) + (↑ε : ℝ)
⊢ dist (integralSum g μ.toBoxAdditive.toSMul π)
          (∑ J ∈ π.boxes,
            HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) +
        dist.{v} (α := E)
          (∑ J ∈ π.boxes,
            HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E))
          (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ) +
      dist.{v} (α := E) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
        (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
    (μ.real (↑I : Set (ι → ℝ)) + 1 + 1) * (↑ε : ℝ)

Tactic:
rw [add_mul, add_mul, one_mul]

Premises used: add_mul, one_mul
-- 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 (integralSum g μ.toBoxAdditive.toSMul π)
          (∑ J ∈ π.boxes,
            HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) +
        dist.{v} (α := E)
          (∑ J ∈ π.boxes,
            HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E))
          (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ) +
      dist.{v} (α := E) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
        (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
    μ.real (↑I : Set (ι → ℝ)) * (↑ε : ℝ) + (↑ε : ℝ) + (↑ε : ℝ)

Tactic:
add_le_add_three ?_ ?_ ?_

Premises used: add_le_add_three
-- 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_1 :
  dist (integralSum g μ.toBoxAdditive.toSMul π)
      (∑ J ∈ π.boxes,
        HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) ≤
    μ.real (↑I : Set (ι → ℝ)) * (↑ε : ℝ)
refine_2 :
  dist.{v} (α := E)
      (∑ J ∈ π.boxes,
        HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E))
      (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ) ≤
    (↑ε : ℝ)
refine_3 :
  dist.{v} (α := E) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
      (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
    (↑ε : ℝ)
⊢ dist (integralSum g μ.toBoxAdditive.toSMul π)
          (∑ J ∈ π.boxes,
            HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) +
        dist.{v} (α := E)
          (∑ J ∈ π.boxes,
            HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E))
          (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ) +
      dist.{v} (α := E) (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
        (∫ (a : ι → ℝ) in (↑I : Set (ι → ℝ)), g a ∂μ) ≤
    μ.real (↑I : Set (ι → ℝ)) * (↑ε : ℝ) + (↑ε : ℝ) + (↑ε : ℝ)

Tactic:
refine add_le_add_three ?_ ?_ ?_

Premises used: add_le_add_three
-- 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_1 :
  dist.{v} (α := E)
      (∑ J ∈ π.boxes, (((μ.toBoxAdditive.toSMul : (a : Box ι) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E) (g (π.tag J)))
      (∑ J ∈ π.boxes,
        HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) ≤
    ∑ i ∈ π.boxes, μ.real (↑i : Set (ι → ℝ)) * (↑ε : ℝ)
⊢ dist (integralSum g μ.toBoxAdditive.toSMul π)
      (∑ J ∈ π.boxes,
        HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) ≤
    μ.real (↑I : Set (ι → ℝ)) * (↑ε : ℝ)

Tactic:
rw [← hπp.iUnion_eq, π.measure_iUnion_toReal, sum_mul, integralSum]

Premises used: BoxIntegral.Prepartition.measure_iUnion_toReal, BoxIntegral.Prepartition.IsPartition.iUnion_eq, BoxIntegral.integralSum, BoxIntegral.TaggedPrepartition.toPrepartition, Finset.sum_mul
-- 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, (((μ.toBoxAdditive.toSMul : (a : Box ι) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E) (g (π.tag J)))
      (∑ J ∈ π.boxes,
        HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) ≤
    ∑ i ∈ π.boxes, μ.real (↑i : Set (ι → ℝ)) * (↑ε : ℝ)

Tactic:
dist_sum_sum_le_of_le _ fun J _ => ?_

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 : 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_1 :
  ∀ J ∈ π.boxes,
    dist ((((μ.toBoxAdditive.toSMul : (a : Box ι) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E) (g (π.tag J)))
        (HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) ≤
      μ.real (↑J : Set (ι → ℝ)) * (↑ε : ℝ)
⊢ dist.{v} (α := E)
      (∑ J ∈ π.boxes, (((μ.toBoxAdditive.toSMul : (a : Box ι) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E) (g (π.tag J)))
      (∑ J ∈ π.boxes,
        HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) ≤
    ∑ i ∈ π.boxes, μ.real (↑i : Set (ι → ℝ)) * (↑ε : ℝ)

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

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 : 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
J : Box ι
h : J ∈ π.boxes
refine_1 :
  dist (μ.real (↑J : Set (ι → ℝ)) • g (π.tag J))
      (HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) ≤
    μ.real (↑J : Set (ι → ℝ)) * (↑ε : ℝ)
⊢ dist ((((μ.toBoxAdditive.toSMul : (a : Box ι) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E) (g (π.tag J)))
      (HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) ≤
    μ.real (↑J : Set (ι → ℝ)) * (↑ε : ℝ)

Tactic:
dsimp
-- 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
J : Box ι
h : J ∈ π.boxes
refine_1 :
  μ.real (↑J : Set (ι → ℝ)) * ‖HSub.hSub (β := E) (g (π.tag J)) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)‖ ≤
    μ.real (↑J : Set (ι → ℝ)) * (↑ε : ℝ)
⊢ dist (μ.real (↑J : Set (ι → ℝ)) • g (π.tag J))
      (HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)) ≤
    μ.real (↑J : Set (ι → ℝ)) * (↑ε : ℝ)

Tactic:
rw [dist_eq_norm, ← smul_sub, norm_smul, Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]

Premises used: dist_eq_norm, norm_smul, MeasureTheory.measureReal_nonneg, smul_sub, abs_of_nonneg, Real.norm_eq_abs
-- 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
J : Box ι
h : J ∈ π.boxes
refine_1 : ‖HSub.hSub (β := E) (g (π.tag J)) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)‖ ≤ (↑ε : ℝ)
⊢ μ.real (↑J : Set (ι → ℝ)) * ‖HSub.hSub (β := E) (g (π.tag J)) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E)‖ ≤
    μ.real (↑J : Set (ι → ℝ)) * (↑ε : ℝ)

Tactic:
gcongr