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
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)
⊢ l.MemBaseSet I c (⋯.convergenceR (↑(δ n) : ℝ) c) (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n)

Tactic:
have :
        l.MemBaseSet I c ((hfi' n).convergenceR (δ n) c) (π.filter fun J => Nx (π.tag J) = n) :=
      (hπ.filter _).mono' _ le_rfl le_rfl fun J hJ => (hrn J hJ).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_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)
⊢ dist.{v} (α := E)
      (integralSum (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n))
      (∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).boxes,
        BoxIntegral.integral J l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul) ≤
    (↑(δ n) : ℝ)

Tactic:
(hfi' n).dist_integralSum_sum_integral_le_of_memBaseSet (δ0 _) this

Premises used: BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet
-- 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)
h :
  Eq.{v + 1} (α := 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))
    (integralSum (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n))
h₁ :
  Eq.{v + 1} (α := E)
    (∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).boxes,
      ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
    (∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).boxes,
      BoxIntegral.integral J l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul)
⊢ 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) : ℝ)

Tactic:
convert! (hfi' n).dist_integralSum_sum_integral_le_of_memBaseSet (δ0 _) this using 2

Premises used: BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet
-- 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)
⊢ Eq.{v + 1} (α := 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))
    (integralSum (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n))

Tactic:
sum_congr rfl fun J hJ => ?_

Premises used: BoxIntegral.integralSum, Finset.sum_congr, 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_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)
h :
  ∀ (J : Box ι) (hJ : 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) =
      (((μ.toBoxAdditive.toSMul : (a : Box ι) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E)
        ((f n : (a : ι → ℝ) → E) ((π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).tag J) : E)
⊢ Eq.{v + 1} (α := 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))
    (integralSum (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n))

Tactic:
refine sum_congr rfl fun J hJ => ?_

Premises used: Finset.sum_congr, 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_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
⊢ HSMul.hSMul (β := E) (μ.real (↑J : Set (ι → ℝ))) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) (π.tag J) : E) =
    (((μ.toBoxAdditive.toSMul : (a : Box ι) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E)
      ((f n : (a : ι → ℝ) → E) ((π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).tag J) : E)

Tactic:
simp [hNxn 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_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)
⊢ Eq.{v + 1} (α := E)
    (∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).boxes,
      ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
    (∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).boxes,
      BoxIntegral.integral J l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul)

Tactic:
sum_congr rfl fun J hJ => ?_

Premises used: Finset.sum_congr, 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_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)
h :
  ∀ (J : Box ι) (hJ : J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).boxes),
    Eq.{v + 1} (α := E) (∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
      (BoxIntegral.integral J l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul)
⊢ Eq.{v + 1} (α := E)
    (∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).boxes,
      ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
    (∑ J ∈ (π.filter fun (J : Box ι) ↦ Nx (π.tag J) = n).boxes,
      BoxIntegral.integral J l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul)

Tactic:
refine sum_congr rfl fun J hJ => ?_

Premises used: Finset.sum_congr, 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_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
h : Integrable.{v, u} (ε := E) (⇑(f (Nx (π.tag J))) : (a : ι → ℝ) → E) (μ.restrict (↑J : Set (ι → ℝ)))
⊢ Eq.{v + 1} (α := E) (∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), (f (Nx (π.tag J)) : (a : ι → ℝ) → E) x ∂μ)
    (BoxIntegral.integral J l (⇑(f n) : (a : ι → ℝ) → E) μ.toBoxAdditive.toSMul)

Tactic:
rw [← SimpleFunc.integral_eq_integral, SimpleFunc.box_integral_eq_integral _ _ _ _ hl,
        hNxn J hJ]

Premises used: MeasureTheory.SimpleFunc.integral_eq_integral, MeasureTheory.SimpleFunc.box_integral_eq_integral