-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_finset_sum {ι : Type*} {s : Finset ι} {f : ι → α → E}
    (hf : ∀ i ∈ s, Integrable (f i) μ) (m : MeasurableSpace α) :
    μ[∑ i ∈ s, f i|m] =ᵐ[μ] ∑ i ∈ s, μ[f i|m]

Proof state:
case insert
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
i : ι
s : Finset ι
his : i ∉ s
heq : (∀ i ∈ s, Integrable (f i) μ) → μ[∑ i ∈ s, f i|m] =ᶠ[ae μ] ∑ i ∈ s, μ[f i|m]
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ μ[f i + ∑ x ∈ s, f x|m] =ᶠ[ae μ] μ[f i|m] + ∑ x ∈ s, μ[f x|m]

Tactic:
exact (condExp_add (hf i <| Finset.mem_insert_self i s)
  (integrable_finset_sum' _ <| Finset.forall_of_forall_insert hf) _).trans
    ((EventuallyEq.refl _ _).add <| heq <| Finset.forall_of_forall_insert hf)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, Integrable (f i) μ
m : MeasurableSpace α
⊢ μ[∑ i ∈ s, f i|m] =ᶠ[ae μ] ∑ i ∈ s, μ[f i|m]

Tactic:
induction' s using Finset.induction_on with i s his heq hf

Result:
case empty
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
hf : ∀ i ∈ ∅, Integrable (f i) μ
⊢ μ[∑ i ∈ ∅, f i|m] =ᶠ[ae μ] ∑ i ∈ ∅, μ[f i|m]

case insert
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
i : ι
s : Finset ι
his : i ∉ s
heq : (∀ i ∈ s, Integrable (f i) μ) → μ[∑ i ∈ s, f i|m] =ᶠ[ae μ] ∑ i ∈ s, μ[f i|m]
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ μ[∑ i ∈ insert i s, f i|m] =ᶠ[ae μ] ∑ i ∈ insert i s, μ[f i|m]

Proof state:
case empty
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
hf : ∀ i ∈ ∅, Integrable (f i) μ
⊢ μ[∑ i ∈ ∅, f i|m] =ᶠ[ae μ] ∑ i ∈ ∅, μ[f i|m]

Tactic:
rw [Finset.sum_empty, Finset.sum_empty, condExp_zero]

Result:
no goals

Proof state:
case insert
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
i : ι
s : Finset ι
his : i ∉ s
heq : (∀ i ∈ s, Integrable (f i) μ) → μ[∑ i ∈ s, f i|m] =ᶠ[ae μ] ∑ i ∈ s, μ[f i|m]
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ μ[∑ i ∈ insert i s, f i|m] =ᶠ[ae μ] ∑ i ∈ insert i s, μ[f i|m]

Tactic:
rw [Finset.sum_insert his, Finset.sum_insert his]

Result:
case insert
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
i : ι
s : Finset ι
his : i ∉ s
heq : (∀ i ∈ s, Integrable (f i) μ) → μ[∑ i ∈ s, f i|m] =ᶠ[ae μ] ∑ i ∈ s, μ[f i|m]
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ μ[f i + ∑ x ∈ s, f x|m] =ᶠ[ae μ] μ[f i|m] + ∑ x ∈ s, μ[f x|m]