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_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 (ι → ℝ)) μ
J : Box ι
hJ : J ∈ π.boxes
refine_3 :
  norm.{v} (E := E)
      (∫ (a : ι → ℝ) in (↑J : Set (ι → ℝ)), HSub.hSub (α := E) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) a : E) (g a) ∂μ) ≤
    ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ
⊢ 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)‖ ∂μ

Tactic:
rw [dist_eq_norm, ← integral_sub (hfi _ J hJ) (hgi J hJ)]

Premises used: dist_eq_norm, MeasureTheory.integral_sub
-- 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 (ι → ℝ)) μ
J : Box ι
hJ : J ∈ π.boxes
⊢ norm.{v} (E := E)
      (∫ (a : ι → ℝ) in (↑J : Set (ι → ℝ)), HSub.hSub (α := E) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) a : E) (g a) ∂μ) ≤
    ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ

Tactic:
norm_integral_le_of_norm_le (hfgi _ J hJ) (Eventually.of_forall fun x => ?_)

Premises used: MeasureTheory.norm_integral_le_of_norm_le, Filter.Eventually.of_forall
-- 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 (ι → ℝ)) μ
J : Box ι
hJ : J ∈ π.boxes
refine_3 :
  ∀ (x : ι → ℝ),
    ‖HSub.hSub (α := E) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
      ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖
⊢ norm.{v} (E := E)
      (∫ (a : ι → ℝ) in (↑J : Set (ι → ℝ)), HSub.hSub (α := E) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) a : E) (g a) ∂μ) ≤
    ∫ (x : ι → ℝ) in (↑J : Set (ι → ℝ)), ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖ ∂μ

Tactic:
refine norm_integral_le_of_norm_le (hfgi _ J hJ) (Eventually.of_forall fun x => ?_)

Premises used: MeasureTheory.norm_integral_le_of_norm_le, Filter.Eventually.of_forall
-- 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 (ι → ℝ)) μ
J : Box ι
hJ : J ∈ π.boxes
x : ι → ℝ
⊢ ‖HSub.hSub (α := E) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
    ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖

Tactic:
hfg_mono x (hNx (π.tag J))

Premises used: 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_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 (ι → ℝ)) μ
J : Box ι
hJ : J ∈ π.boxes
x : ι → ℝ
⊢ ‖HSub.hSub (α := E) ((f (Nx (π.tag J)) : (a : ι → ℝ) → E) x : E) (g x)‖ ≤
    ‖HSub.hSub (α := E) ((f N₀ : (a : ι → ℝ) → E) x : E) (g x)‖

Tactic:
exact hfg_mono x (hNx (π.tag J))

Premises used: 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
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
l : IntegrationParams
obtain :
  ∀ (y : E) (hy : HasIntegral I l f μ.toBoxAdditive.toSMul y),
    HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ)
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ)

Tactic:
obtain ⟨y, hy⟩ := BoxIntegral.integrable_of_continuousOn l hc μ

Premises used: BoxIntegral.integrable_of_continuousOn
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul y

Tactic:
hy
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
h : ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ = y
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ)

Tactic:
convert! hy
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ IntegrableOn f (↑I : Set (ι → ℝ)) μ

Tactic:
have : IntegrableOn f I μ :=
    IntegrableOn.mono_set (hc.integrableOn_compact I.isCompact_Icc) Box.coe_subset_Icc
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this : IntegrableOn f (↑I : Set (ι → ℝ)) μ
⊢ ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ = y

Tactic:
HasIntegral.unique (IntegrableOn.hasBoxIntegral this ⊥ rfl) (HasIntegral.mono hy bot_le)

Premises used: MeasureTheory.IntegrableOn.hasBoxIntegral, BoxIntegral.HasIntegral.mono, Bot.bot, BoxIntegral.HasIntegral.unique, bot_le, 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
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this : IntegrableOn f (↑I : Set (ι → ℝ)) μ
⊢ ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ = y

Tactic:
exact HasIntegral.unique (IntegrableOn.hasBoxIntegral this ⊥ rfl) (HasIntegral.mono hy bot_le)

Premises used: MeasureTheory.IntegrableOn.hasBoxIntegral, BoxIntegral.HasIntegral.mono, Bot.bot, BoxIntegral.HasIntegral.unique, bot_le, 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
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
obtain :
  ∀ (y : E) (hy : HasIntegral I l f μ.toBoxAdditive.toSMul y),
    HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ)
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ)

Tactic:
obtain ⟨y, hy⟩ := integrable_of_bounded_and_ae_continuous l hb μ hc

Premises used: BoxIntegral.integrable_of_bounded_and_ae_continuous
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul y

Tactic:
hy
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
h : ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ = y
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ)

Tactic:
convert! hy
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ = y

Tactic:
HasIntegral.unique (IntegrableOn.hasBoxIntegral ?_ ⊥ rfl) (HasIntegral.mono hy bot_le)

Premises used: MeasureTheory.IntegrableOn.hasBoxIntegral, BoxIntegral.HasIntegral.mono, Bot.bot, BoxIntegral.HasIntegral.unique, bot_le, 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
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
h : IntegrableOn f (↑I : Set (ι → ℝ)) μ
⊢ ∫ (x : ι → ℝ) in (↑I : Set (ι → ℝ)), f x ∂μ = y

Tactic:
refine HasIntegral.unique (IntegrableOn.hasBoxIntegral ?_ ⊥ rfl) (HasIntegral.mono hy bot_le)

Premises used: MeasureTheory.IntegrableOn.hasBoxIntegral, BoxIntegral.HasIntegral.mono, Bot.bot, BoxIntegral.HasIntegral.unique, bot_le, 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
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
h : AEStronglyMeasurable f (μ.restrict (↑I : Set (ι → ℝ)))
h₁ : HasFiniteIntegral f (μ.restrict (↑I : Set (ι → ℝ)))
⊢ IntegrableOn f (↑I : Set (ι → ℝ)) μ

Tactic:
constructor
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x : ι → ℝ | ContinuousAt f x}
⊢ AEStronglyMeasurable f (μ.restrict v)

Tactic:
have : AEStronglyMeasurable f (μ.restrict v) :=
      (continuousOn_of_forall_continuousAt fun _ h ↦ h).aestronglyMeasurable
      (measurableSet_of_continuousAt f)
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x : ι → ℝ | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
⊢ AEStronglyMeasurable f (μ.restrict (↑I : Set (ι → ℝ)))

Tactic:
this.mono_measure (Measure.le_iff.2 fun s hs ↦ ?_)

Premises used: Iff.mpr, MeasureTheory.AEStronglyMeasurable.mono_measure, MeasureTheory.Measure.le_iff
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x : ι → ℝ | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
h :
  ∀ (s : Set (ι → ℝ)) (hs : MeasurableSet s),
    LE.le (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ.restrict v : (a : Set (ι → ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ AEStronglyMeasurable f (μ.restrict (↑I : Set (ι → ℝ)))

Tactic:
refine this.mono_measure (Measure.le_iff.2 fun s hs ↦ ?_)

Premises used: Iff.mpr, MeasureTheory.AEStronglyMeasurable.mono_measure, MeasureTheory.Measure.le_iff
-- Module: Mathlib.Analysis.BoxIntegral.Integrability
Goal:
ι : Type u
E : Type v
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
I : Box ι
hb :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x : ι → ℝ | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
h :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (s ∩ (↑I : Set (ι → ℝ))) : ℝ≥0∞)
    ((μ.restrict v : (a : Set (ι → ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.restrict (↑I : Set (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.restrict v : (a : Set (ι → ℝ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [μ.restrict_apply hs]

Premises used: MeasureTheory.Measure.restrict_apply