-- Mathlib/Probability/Variance.lean
theorem IndepFun.variance_sum [IsProbabilityMeasure μ] {ι : Type*} {X : ι → Ω → ℝ}
    {s : Finset ι} (hs : ∀ i ∈ s, MemLp (X i) 2 μ)
    (h : Set.Pairwise ↑s fun i j => IndepFun (X i) (X j) μ) :
    variance (∑ i ∈ s, X i) μ = ∑ i ∈ s, variance (X i) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]

Tactic:
induction' s using Finset.induction_on with k s ks IH

Result:
case empty
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
hs : ∀ i ∈ ∅, MemLp (X i) 2 μ
h : (↑∅).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ Var[∑ i ∈ ∅, X i; μ] = ∑ i ∈ ∅, Var[X i; μ]

case insert
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ Var[∑ i ∈ insert k s, X i; μ] = ∑ i ∈ insert k s, Var[X i; μ]

Proof state:
case insert
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ Var[∑ i ∈ insert k s, X i; μ] = ∑ i ∈ insert k s, Var[X i; μ]

Tactic:
rw [variance_def' (memLp_finset_sum' _ hs), sum_insert ks, sum_insert ks]

Result:
case insert
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ ∫ (x : Ω), ((X k + ∑ x ∈ s, X x) ^ 2) x ∂μ - (∫ (x : Ω), (X k + ∑ x ∈ s, X x) x ∂μ) ^ 2 =
    Var[X k; μ] + ∑ x ∈ s, Var[X x; μ]

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
i : ι
hi : i ∈ s
⊢ k ≠ i

Tactic:
exact fun hki => ks (hki.symm ▸ hi)

Result:
no goals

Proof state:
case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ Integrable (∑ i ∈ s, X i) μ

Tactic:
apply integrable_finset_sum' _ fun i hi => ?_

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
i : ι
hi : i ∈ s
⊢ Integrable (X i) μ

Proof state:
case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ Integrable ((∑ i ∈ s, X i) ^ 2) μ

Tactic:
apply MemLp.integrable_sq

Result:
case hg.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ MemLp (∑ i ∈ s, X i) 2 μ

Proof state:
case hXY
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
i : ι
hi : i ∈ s
⊢ k ≠ i

Tactic:
exact fun hki => ks (hki.symm ▸ hi)

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ ∫ (x : Ω), (X k ^ 2) x ∂μ + ∫ (x : Ω), ((∑ i ∈ s, X i) ^ 2) x ∂μ + ∫ (x : Ω), (2 * X k * ∑ i ∈ s, X i) x ∂μ -
      (∫ (x : Ω), X k x ∂μ + ∫ (x : Ω), (∑ i ∈ s, X i) x ∂μ) ^ 2 =
    ∫ (x : Ω), (X k ^ 2) x ∂μ - (∫ (x : Ω), X k x ∂μ) ^ 2 +
        (∫ (x : Ω), ((∑ i ∈ s, X i) ^ 2) x ∂μ - (∫ (x : Ω), (∑ i ∈ s, X i) x ∂μ) ^ 2) +
      (∫ (x : Ω), (2 * X k * ∑ i ∈ s, X i) x ∂μ - (2 * ∫ (x : Ω), X k x ∂μ) * ∫ (x : Ω), (∑ i ∈ s, X i) x ∂μ)

Tactic:
ring

Result:
no goals

Proof state:
case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ Integrable (2 * X k * ∑ i ∈ s, X i) μ

Tactic:
rw [mul_assoc]

Result:
case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ Integrable (2 * (X k * ∑ i ∈ s, X i)) μ