Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: case 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)

pp: case 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)

pp: case 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)

Tactic:
]

Goal state after:
case 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 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 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)