-- Mathlib/Analysis/BoxIntegral/Integrability.lean
theorem ContinuousOn.hasBoxIntegral [CompleteSpace E] {f : (ι → ℝ) → E} (μ : Measure (ι → ℝ))
    [IsLocallyFiniteMeasure μ] {I : Box ι} (hc : ContinuousOn f (Box.Icc I))
    (l : IntegrationParams) :
    HasIntegral.{u, v, v} I l f μ.toBoxAdditive.toSMul (∫ x in I, f x ∂μ)

Proof state:
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f (Box.Icc I)
l : IntegrationParams
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)

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

Result:
case intro
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f (Box.Icc I)
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)

Proof state:
case h.e'_13
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f (Box.Icc I)
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ ∫ (x : ι → ℝ) in ↑I, f x ∂μ = y

Tactic:
have : IntegrableOn f I μ :=
  IntegrableOn.mono_set (hc.integrableOn_compact I.isCompact_Icc) Box.coe_subset_Icc

Result:
case h.e'_13
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f (Box.Icc I)
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this : IntegrableOn f (↑I) μ
⊢ ∫ (x : ι → ℝ) in ↑I, f x ∂μ = y

Proof state:
case h.e'_13
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f (Box.Icc I)
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this : IntegrableOn f (↑I) μ
⊢ ∫ (x : ι → ℝ) in ↑I, f x ∂μ = y

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

Result:
no goals

Proof state:
case intro
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f (Box.Icc I)
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)

Tactic:
convert hy

Result:
case h.e'_13
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f (Box.Icc I)
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ ∫ (x : ι → ℝ) in ↑I, f x ∂μ = y