-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem HasIntegral.sum {α : Type*} {s : Finset α} {f : α → ℝⁿ → E} {g : α → F}
    (h : ∀ i ∈ s, HasIntegral I l (f i) vol (g i)) :
    HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)

Proof state:
case insert
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
f : α → (ι → ℝ) → E
g : α → F
a : α
s : Finset α
ha : a ∉ s
ihs : (∀ i ∈ s, HasIntegral I l (f i) vol (g i)) → HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
h : HasIntegral I l (f a) vol (g a) ∧ ∀ x ∈ s, HasIntegral I l (f x) vol (g x)
⊢ HasIntegral I l (fun x => f a x + ∑ i ∈ s, f i x) vol (g a + ∑ i ∈ s, g i)

Tactic:
exact h.1.add (ihs h.2)

Result:
no goals

Proof state:
case empty
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
f : α → (ι → ℝ) → E
g : α → F
h : ∀ i ∈ ∅, HasIntegral I l (f i) vol (g i)
⊢ HasIntegral I l (fun x => ∑ i ∈ ∅, f i x) vol (∑ i ∈ ∅, g i)

Tactic:
simp [hasIntegral_zero]

Result:
no goals

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
s : Finset α
f : α → (ι → ℝ) → E
g : α → F
h : ∀ i ∈ s, HasIntegral I l (f i) vol (g i)
⊢ HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)

Tactic:
induction' s using Finset.induction_on with a s ha ihs

Result:
case empty
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
f : α → (ι → ℝ) → E
g : α → F
h : ∀ i ∈ ∅, HasIntegral I l (f i) vol (g i)
⊢ HasIntegral I l (fun x => ∑ i ∈ ∅, f i x) vol (∑ i ∈ ∅, g i)

case insert
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
f : α → (ι → ℝ) → E
g : α → F
a : α
s : Finset α
ha : a ∉ s
ihs : (∀ i ∈ s, HasIntegral I l (f i) vol (g i)) → HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
h : ∀ i ∈ insert a s, HasIntegral I l (f i) vol (g i)
⊢ HasIntegral I l (fun x => ∑ i ∈ insert a s, f i x) vol (∑ i ∈ insert a s, g i)

Proof state:
case insert
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
f : α → (ι → ℝ) → E
g : α → F
a : α
s : Finset α
ha : a ∉ s
ihs : (∀ i ∈ s, HasIntegral I l (f i) vol (g i)) → HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
h : ∀ i ∈ insert a s, HasIntegral I l (f i) vol (g i)
⊢ HasIntegral I l (fun x => f a x + ∑ i ∈ s, f i x) vol (g a + ∑ i ∈ s, g i)

Tactic:
rw [Finset.forall_mem_insert] at h

Result:
case insert
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
f : α → (ι → ℝ) → E
g : α → F
a : α
s : Finset α
ha : a ∉ s
ihs : (∀ i ∈ s, HasIntegral I l (f i) vol (g i)) → HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
h : HasIntegral I l (f a) vol (g a) ∧ ∀ x ∈ s, HasIntegral I l (f x) vol (g x)
⊢ HasIntegral I l (fun x => f a x + ∑ i ∈ s, f i x) vol (g a + ∑ i ∈ s, g i)

Proof state:
case insert
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
f : α → (ι → ℝ) → E
g : α → F
a : α
s : Finset α
ha : a ∉ s
ihs : (∀ i ∈ s, HasIntegral I l (f i) vol (g i)) → HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
h : ∀ i ∈ insert a s, HasIntegral I l (f i) vol (g i)
⊢ HasIntegral I l (fun x => ∑ i ∈ insert a s, f i x) vol (∑ i ∈ insert a s, g i)

Tactic:
simp only [Finset.sum_insert ha]

Result:
case insert
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
f : α → (ι → ℝ) → E
g : α → F
a : α
s : Finset α
ha : a ∉ s
ihs : (∀ i ∈ s, HasIntegral I l (f i) vol (g i)) → HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
h : ∀ i ∈ insert a s, HasIntegral I l (f i) vol (g i)
⊢ HasIntegral I l (fun x => f a x + ∑ i ∈ s, f i x) vol (g a + ∑ i ∈ s, g i)