-- Mathlib/Analysis/BoxIntegral/Integrability.lean
theorem hasBoxIntegral (f : SimpleFunc (ι → ℝ) E) (μ : Measure (ι → ℝ)) [IsLocallyFiniteMeasure μ]
    (I : Box ι) (l : IntegrationParams) (hl : l.bRiemann = false) :
    HasIntegral.{u, v, v} I l f μ.toBoxAdditive.toSMul (f.integral (μ.restrict I))

Proof state:
case h_add
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ⇑f) (Function.support ⇑g)
hfi : HasIntegral I l (⇑f) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) f)
hgi : HasIntegral I l (⇑g) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : Fact (μ ↑I < ⊤)
⊢ HasIntegral I l (⇑(f + g)) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) (f + g))

Tactic:
rw [integral_add]

Result:
case h_add
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ⇑f) (Function.support ⇑g)
hfi : HasIntegral I l (⇑f) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) f)
hgi : HasIntegral I l (⇑g) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : Fact (μ ↑I < ⊤)
⊢ HasIntegral I l (⇑(f + g)) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) f + integral (μ.restrict ↑I) g)

case h_add.hf
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ⇑f) (Function.support ⇑g)
hfi : HasIntegral I l (⇑f) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) f)
hgi : HasIntegral I l (⇑g) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : Fact (μ ↑I < ⊤)
⊢ Integrable (⇑f) (μ.restrict ↑I)

case h_add.hg
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ⇑f) (Function.support ⇑g)
hfi : HasIntegral I l (⇑f) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) f)
hgi : HasIntegral I l (⇑g) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : Fact (μ ↑I < ⊤)
⊢ Integrable (⇑g) (μ.restrict ↑I)

Proof state:
case h_add
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ⇑f) (Function.support ⇑g)
hfi : HasIntegral I l (⇑f) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) f)
hgi : HasIntegral I l (⇑g) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ HasIntegral I l (⇑(f + g)) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) (f + g))

Tactic:
haveI := Fact.mk (I.measure_coe_lt_top μ)

Result:
case h_add
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
f g : SimpleFunc (ι → ℝ) E
a✝ : Disjoint (Function.support ⇑f) (Function.support ⇑g)
hfi : HasIntegral I l (⇑f) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) f)
hgi : HasIntegral I l (⇑g) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) g)
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : Fact (μ ↑I < ⊤)
⊢ HasIntegral I l (⇑(f + g)) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) (f + g))