-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_finset_sum_measure {ι} {m : MeasurableSpace α} {f : α → G} {μ : ι → Measure α}
    {s : Finset ι} (hf : ∀ i ∈ s, Integrable f (μ i)) :
    ∫ a, f a ∂(∑ i ∈ s, μ i) = ∑ i ∈ s, ∫ a, f a ∂μ i

Proof state:
case h₂
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a✝ : ι
s✝ : Finset ι
h : a✝ ∉ s✝
ih : (∀ i ∈ s✝, Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s✝, μ i = ∑ i ∈ s✝, ∫ (a : α), f a ∂μ i
hf : Integrable f (μ a✝) ∧ ∀ x ∈ s✝, Integrable f (μ x)
⊢ ∫ (a : α), f a ∂∑ i ∈ Finset.cons a✝ s✝ h, μ i = ∑ i ∈ Finset.cons a✝ s✝ h, ∫ (a : α), f a ∂μ i

Tactic:
rw [Finset.sum_cons, Finset.sum_cons, ← ih hf.2]

Result:
case h₂
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a✝ : ι
s✝ : Finset ι
h : a✝ ∉ s✝
ih : (∀ i ∈ s✝, Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s✝, μ i = ∑ i ∈ s✝, ∫ (a : α), f a ∂μ i
hf : Integrable f (μ a✝) ∧ ∀ x ∈ s✝, Integrable f (μ x)
⊢ ∫ (a : α), f a ∂(μ a✝ + ∑ x ∈ s✝, μ x) = ∫ (a : α), f a ∂μ a✝ + ∫ (a : α), f a ∂∑ i ∈ s✝, μ i

Proof state:
case h₁
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : ∀ i ∈ ∅, Integrable f (μ i)
⊢ ∫ (a : α), f a ∂∑ i ∈ ∅, μ i = ∑ i ∈ ∅, ∫ (a : α), f a ∂μ i

Tactic:
simp

Result:
no goals

Proof state:
case h₂
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a✝ : ι
s✝ : Finset ι
h : a✝ ∉ s✝
ih : (∀ i ∈ s✝, Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s✝, μ i = ∑ i ∈ s✝, ∫ (a : α), f a ∂μ i
hf : Integrable f (μ a✝) ∧ ∀ x ∈ s✝, Integrable f (μ x)
⊢ ∫ (a : α), f a ∂(μ a✝ + ∑ x ∈ s✝, μ x) = ∫ (a : α), f a ∂μ a✝ + ∫ (a : α), f a ∂∑ i ∈ s✝, μ i

Tactic:
exact integral_add_measure hf.1 (integrable_finset_sum_measure.2 hf.2)

Result:
no goals

Proof state:
case h₂
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a✝ : ι
s✝ : Finset ι
h : a✝ ∉ s✝
ih : (∀ i ∈ s✝, Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s✝, μ i = ∑ i ∈ s✝, ∫ (a : α), f a ∂μ i
hf : ∀ i ∈ Finset.cons a✝ s✝ h, Integrable f (μ i)
⊢ ∫ (a : α), f a ∂∑ i ∈ Finset.cons a✝ s✝ h, μ i = ∑ i ∈ Finset.cons a✝ s✝ h, ∫ (a : α), f a ∂μ i

Tactic:
rw [Finset.forall_mem_cons] at hf

Result:
case h₂
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a✝ : ι
s✝ : Finset ι
h : a✝ ∉ s✝
ih : (∀ i ∈ s✝, Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s✝, μ i = ∑ i ∈ s✝, ∫ (a : α), f a ∂μ i
hf : Integrable f (μ a✝) ∧ ∀ x ∈ s✝, Integrable f (μ x)
⊢ ∫ (a : α), f a ∂∑ i ∈ Finset.cons a✝ s✝ h, μ i = ∑ i ∈ Finset.cons a✝ s✝ h, ∫ (a : α), f a ∂μ i

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_7
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
s : Finset ι
hf : ∀ i ∈ s, Integrable f (μ i)
⊢ ∫ (a : α), f a ∂∑ i ∈ s, μ i = ∑ i ∈ s, ∫ (a : α), f a ∂μ i

Tactic:
induction s using Finset.cons_induction_on with
| h₁ => simp
| h₂ h ih =>
  rw [Finset.forall_mem_cons] at hf
  rw [Finset.sum_cons, Finset.sum_cons, ← ih hf.2]
  exact integral_add_measure hf.1 (integrable_finset_sum_measure.2 hf.2)

Result:
no goals