-- Mathlib/Probability/Moments/Basic.lean
theorem iIndepFun.cgf_sum {X : ι → Ω → ℝ}
    (h_indep : iIndepFun (fun _ => inferInstance) X μ) (h_meas : ∀ i, Measurable (X i))
    {s : Finset ι} (h_int : ∀ i ∈ s, Integrable (fun ω => exp (t * X i ω)) μ) :
    cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t

Proof state:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω => rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
⊢ log (mgf (∑ i ∈ s, X i) μ t) = log (∏ i ∈ s, mgf (X i) μ t)

Tactic:
rw [h_indep.mgf_sum h_meas]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω => rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
j : ι
hj : j ∈ s
⊢ mgf (X j) μ t ≠ 0

Tactic:
exact (mgf_pos (h_int j hj)).ne'

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω => rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
⊢ log (mgf (∑ i ∈ s, X i) μ t) = ∑ x ∈ s, log (mgf (X x) μ t)

Tactic:
rw [← log_prod _ _ fun j hj => ?_]

Result:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω => rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
⊢ log (mgf (∑ i ∈ s, X i) μ t) = log (∏ i ∈ s, mgf (X i) μ t)

Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω => rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
j : ι
hj : j ∈ s
⊢ mgf (X j) μ t ≠ 0

Proof state:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω => rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
⊢ cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t

Tactic:
simp_rw [cgf]

Result:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω => rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
⊢ log (mgf (∑ i ∈ s, X i) μ t) = ∑ x ∈ s, log (mgf (X x) μ t)

Proof state:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω => rexp (t * X i ω)) μ
⊢ cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t

Tactic:
have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure

Result:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω => rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
⊢ cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t