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

Tactic:
rw [← dist_eq_norm']

Premises used: dist_eq_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 : 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
⊢ dist ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J)) (g (π.tag J)) ≤ (↑ε : ℝ)

Tactic:
hNxε _
-- 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
⊢ dist ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J)) (g (π.tag J)) ≤ (↑ε : ℝ)

Tactic:
exact hNxε _
-- 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_2 :
  dist.{v} (α := E)
      (∑ y ∈ Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes,
        ∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = y).boxes,
          HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E))
      (∑ y ∈ Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes,
        ∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = y).boxes,
          ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ) ≤
    (↑ε : ℝ)
⊢ 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 ∂μ) ≤
    (↑ε : ℝ)

Tactic:
rw [← π.sum_fiberwise fun J => Nx (π.tag J), ← π.sum_fiberwise fun J => Nx (π.tag J)]

Premises used: BoxIntegral.Prepartition.sum_fiberwise, BoxIntegral.TaggedPrepartition.toPrepartition, BoxIntegral.TaggedPrepartition.tag
-- 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_2 :
  dist.{v} (α := E)
      (∑ y ∈ Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes,
        ∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = y).boxes,
          HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E))
      (∑ y ∈ Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes,
        ∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = y).boxes,
          ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ) ≤
    (↑c_1 : ℝ)
⊢ dist.{v} (α := E)
      (∑ y ∈ Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes,
        ∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = y).boxes,
          HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E))
      (∑ y ∈ Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes,
        ∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = y).boxes,
          ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ) ≤
    (↑ε : ℝ)

Tactic:
grw [← hcε]
-- 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)
      (∑ y ∈ Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes,
        ∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = y).boxes,
          HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E))
      (∑ y ∈ Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes,
        ∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = y).boxes,
          ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ) ≤
    (↑c_1 : ℝ)

Tactic:
(dist_sum_sum_le_of_le _ fun n hn => ?_).trans
        (sum_le_hasSum _ (fun n _ => (δ n).2) (NNReal.hasSum_coe.2 hδc))

Premises used: Iff.mpr, sum_le_hasSum, dist_sum_sum_le_of_le, LE.le.trans, NNReal.hasSum_coe, Subtype.property
-- 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_2 :
  ∀ (n : ℕ) (hn : Membership.mem (γ := Finset ℕ) (Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes) n),
    dist.{v} (α := E)
        (∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).boxes,
          HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E))
        (∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).boxes,
          ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ) ≤
      (↑(δ n) : ℝ)
⊢ dist.{v} (α := E)
      (∑ y ∈ Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes,
        ∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = y).boxes,
          HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E))
      (∑ y ∈ Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes,
        ∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = y).boxes,
          ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ) ≤
    (↑c_1 : ℝ)

Tactic:
refine
      (dist_sum_sum_le_of_le _ fun n hn => ?_).trans
        (sum_le_hasSum _ (fun n _ => (δ n).2) (NNReal.hasSum_coe.2 hδc))

Premises used: Iff.mpr, sum_le_hasSum, dist_sum_sum_le_of_le, LE.le.trans, NNReal.hasSum_coe, Subtype.property
-- 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 : ℕ
hn : Membership.mem (γ := Finset ℕ) (Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes) n
⊢ ∀ J ∈ π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n, Nx (π.tag J) = n

Tactic:
have hNxn : ∀ J ∈ π.filter fun J => Nx (π.tag J) = n, Nx (π.tag J) = n := fun J hJ =>
      (π.mem_filter.1 hJ).2
-- 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 : ℕ
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
J : Box ι
hJ : J ∈ π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n
obtain :
  ∀ (hn : Membership.mem (γ := Finset ℕ) (Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes) (Nx (π.tag J)))
    (hNxn : ∀ J_1 ∈ π.filter fun (J_2 : Box ι) ↦ Nx (π.tag J_2) = Nx (π.tag J), Nx (π.tag J_1) = Nx (π.tag J))
    (hJ : J ∈ π.filter fun (J_1 : Box ι) ↦ Nx (π.tag J_1) = Nx (π.tag J)),
    r c (π.tag J) =
      Integrable.convergenceR (f := (⇑(f (Nx (π.tag J))) : (a : ι → ℝ) → E)) ⋯ (↑(δ (Nx (π.tag J))) : ℝ) c (π.tag J)
⊢ r c (π.tag J) = ⋯.convergenceR (↑(δ n) : ℝ) c (π.tag J)

Tactic:
obtain rfl := hNxn J hJ

Premises used: rfl
-- 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 ι
hn : Membership.mem (γ := Finset ℕ) (Finset.image (fun (J : Box ι) ↦ Nx (π.tag J)) π.boxes) (Nx (π.tag J))
hNxn : ∀ J_1 ∈ π.filter fun (J_2 : Box ι) ↦ Nx (π.tag J_2) = Nx (π.tag J), Nx (π.tag J_1) = Nx (π.tag J)
hJ : J ∈ π.filter fun (J_1 : Box ι) ↦ Nx (π.tag J_1) = Nx (π.tag J)
⊢ r c (π.tag J) =
    Integrable.convergenceR (f := (⇑(f (Nx (π.tag J))) : (a : ι → ℝ) → E)) ⋯ (↑(δ (Nx (π.tag J))) : ℝ) c (π.tag J)

Tactic:
rfl
-- 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 : ℕ
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
⊢ ∀ J ∈ π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n, r c (π.tag J) = ⋯.convergenceR (↑(δ n) : ℝ) c (π.tag J)

Tactic:
have hrn : ∀ J ∈ π.filter fun J => Nx (π.tag J) = n,
        r c (π.tag J) = (hfi' n).convergenceR (δ n) c (π.tag J) := fun J hJ ↦ by
      obtain rfl := hNxn J hJ
      rfl