-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem integrable_of_continuousOn [CompleteSpace E] {I : Box ι} {f : ℝⁿ → E}
    (hc : ContinuousOn f (Box.Icc I)) (μ : Measure ℝⁿ) [IsLocallyFiniteMeasure μ] :
    Integrable.{u, v, v} I l f μ.toBoxAdditive.toSMul

Proof state:
case hb
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C

Tactic:
obtain ⟨C, hC⟩ := (NormedSpace.isBounded_iff_subset_smul_closedBall ℝ).1
                    (I.isCompact_Icc.image_of_continuousOn hc).isBounded

Result:
case hb.intro
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ
hC : f '' Box.Icc I ⊆ C • Metric.closedBall 0 1
⊢ ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C

Proof state:
case hc
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ Box.Icc I ∈ ae (μ.restrict (Box.Icc I))

Tactic:
rw [mem_ae_iff, μ.restrict_apply] <;> simp [MeasurableSet.compl_iff.2 I.measurableSet_Icc]

Result:
no goals

Proof state:
case hb.intro
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ
hC : f '' Box.Icc I ⊆ C • Metric.closedBall 0 1
⊢ ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C

Tactic:
use ‖C‖, fun x hx ↦ by
  simpa only [smul_unitClosedBall, mem_closedBall_zero_iff] using hC (Set.mem_image_of_mem f hx)

Result:
no goals

Proof state:
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ
hC : f '' Box.Icc I ⊆ C • Metric.closedBall 0 1
x : ι → ℝ
hx : x ∈ Box.Icc I
⊢ ‖f x‖ ≤ ‖C‖

Tactic:
simpa only [smul_unitClosedBall, mem_closedBall_zero_iff] using hC (Set.mem_image_of_mem f hx)

Result:
no goals

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

Tactic:
apply integrable_of_bounded_and_ae_continuousWithinAt

Result:
case hb
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C

case hc
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x

Proof state:
case hc
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x

Tactic:
refine eventually_of_mem ?_ (fun x hx ↦ hc.continuousWithinAt hx)

Result:
case hc
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ Box.Icc I ∈ ae (μ.restrict (Box.Icc I))