-- Mathlib/Analysis/BoxIntegral/Integrability.lean
theorem AEContinuous.hasBoxIntegral [CompleteSpace E] {f : (ι → ℝ) → E} (μ : Measure (ι → ℝ))
    [IsLocallyFiniteMeasure μ] {I : Box ι} (hb : ∃ C : ℝ, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C)
    (hc : ∀ᵐ x ∂μ, ContinuousAt f x) (l : IntegrationParams) :
    HasIntegral.{u, v, v} I l f μ.toBoxAdditive.toSMul (∫ x in I, f x ∂μ)

Proof state:
case h.e'_13.left
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖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
⊢ μ.measureOf s = μ (s ∩ v)

Tactic:
refine measure_eq_measure_of_null_diff s.inter_subset_left ?_ |>.symm

Result:
case h.e'_13.left
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖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
⊢ μ (s \ (s ∩ v)) = 0

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 ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ IntegrableOn f (↑I) μ

Tactic:
constructor

Result:
case h.e'_13.left
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ AEStronglyMeasurable f (μ.restrict ↑I)

case h.e'_13.right
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ HasFiniteIntegral f (μ.restrict ↑I)

Proof state:
case h.e'_13.left
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ AEStronglyMeasurable f (μ.restrict ↑I)

Tactic:
let v := {x : (ι → ℝ) | ContinuousAt f x}

Result:
case h.e'_13.left
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖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 ↑I)

Proof state:
case h.e'_13.right
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this : IsFiniteMeasure (μ.restrict (Box.Icc I))
⊢ HasFiniteIntegral f (μ.restrict ↑I)

Tactic:
have : IsFiniteMeasure (μ.restrict I) :=
  isFiniteMeasure_of_le (μ.restrict (Box.Icc I))
                        (μ.restrict_mono Box.coe_subset_Icc (le_refl μ))

Result:
case h.e'_13.right
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this✝ : IsFiniteMeasure (μ.restrict (Box.Icc I))
this : IsFiniteMeasure (μ.restrict ↑I)
⊢ HasFiniteIntegral f (μ.restrict ↑I)

Proof state:
case h.e'_13.left
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖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
⊢ μ (s ∩ vᶜ) ≤ 0

Tactic:
exact le_trans (μ.mono s.inter_subset_right) (nonpos_iff_eq_zero.2 hc)

Result:
no goals

Proof state:
case h.e'_13.left
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖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 ↑I)

Tactic:
have : AEStronglyMeasurable f (μ.restrict v) :=
  (continuousOn_of_forall_continuousAt fun _ h ↦ h).aestronglyMeasurable
  (measurableSet_of_continuousAt f)

Result:
case h.e'_13.left
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖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)

Proof state:
case h.e'_13.right
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ HasFiniteIntegral f (μ.restrict ↑I)

Tactic:
have : IsFiniteMeasure (μ.restrict (Box.Icc I)) :=
  { measure_univ_lt_top := by simp [I.isCompact_Icc.measure_lt_top (μ := μ)] }

Result:
case h.e'_13.right
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this : IsFiniteMeasure (μ.restrict (Box.Icc I))
⊢ HasFiniteIntegral f (μ.restrict ↑I)