awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec :
  ∀ (h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ insert i s, X i) ω)) μ
have this : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
Tactic: have : ∀ i : ι, i ∈ s → AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec :
  ∀ (h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ insert i s, X i) ω)) μ
have h_rec₁ : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
Tactic: specialize h_rec this
Cleared hypotheses: h_rec
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
h_rec : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ insert i s, X i) ω)) μ
have insert : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * HAdd.hAdd (β := Ω → ℝ) (X i) (∑ x ∈ s, X x) ω)) μ
Tactic: rw [sum_insert hi_notin_s]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
s : Finset ι
h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
have empty : ∀
  (h_int :
    ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
  AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
Tactic: induction s using Finset.induction_on with
  | empty =>
    simp only [sum_apply, sum_empty, mul_zero, exp_zero]
    exact aestronglyMeasurable_const
  | insert i s hi_notin_s h_rec =>
    have : ∀ i : ι, i ∈ s → AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
    specialize h_rec this
    rw [sum_insert hi_notin_s]
    apply aestronglyMeasurable_exp_mul_add (h_int i (mem_insert_self _ _)) h_rec
Cleared hypotheses: s, h_int
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
s : Finset ι
h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
empty :
  ∀
    (h_int :
      ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
have insert : ∀ (i : ι) (s : Finset ι) (hi_notin_s : i ∉ s)
  (h_rec :
    ∀ (h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
      AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ)
  (h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ),
  AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ insert i s, X i) ω)) μ
Tactic: induction s using Finset.induction_on with
  | empty =>
    simp only [sum_apply, sum_empty, mul_zero, exp_zero]
    exact aestronglyMeasurable_const
  | insert i s hi_notin_s h_rec =>
    have : ∀ i : ι, i ∈ s → AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
    specialize h_rec this
    rw [sum_insert hi_notin_s]
    apply aestronglyMeasurable_exp_mul_add (h_int i (mem_insert_self _ _)) h_rec
Cleared hypotheses: s, h_int
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
s : Finset ι
h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
have empty : ∀
  (h_int :
    ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
  AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
Tactic: classical
  induction s using Finset.induction_on with
  | empty =>
    simp only [sum_apply, sum_empty, mul_zero, exp_zero]
    exact aestronglyMeasurable_const
  | insert i s hi_notin_s h_rec =>
    have : ∀ i : ι, i ∈ s → AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
    specialize h_rec this
    rw [sum_insert hi_notin_s]
    apply aestronglyMeasurable_exp_mul_add (h_int i (mem_insert_self _ _)) h_rec
Cleared hypotheses: s, h_int
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
s : Finset ι
h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
empty :
  ∀
    (h_int :
      ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
have insert : ∀ (i : ι) (s : Finset ι) (hi_notin_s : i ∉ s)
  (h_rec :
    ∀ (h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
      AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ)
  (h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ),
  AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ insert i s, X i) ω)) μ
Tactic: classical
  induction s using Finset.induction_on with
  | empty =>
    simp only [sum_apply, sum_empty, mul_zero, exp_zero]
    exact aestronglyMeasurable_const
  | insert i s hi_notin_s h_rec =>
    have : ∀ i : ι, i ∈ s → AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
    specialize h_rec this
    rw [sum_insert hi_notin_s]
    apply aestronglyMeasurable_exp_mul_add (h_int i (mem_insert_self _ _)) h_rec
Cleared hypotheses: s, h_int
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (X + Y) ω)) μ
have simp_rw : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) μ
Tactic: simp_rw [Pi.add_apply, mul_add, exp_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
have empty : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 1) μ
Tactic: simp only [sum_apply, sum_empty, mul_zero, exp_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec :
  ∀ (h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ insert i s, X i) ω)) μ
have this : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
Tactic: have : ∀ i : ι, i ∈ s → Integrable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec :
  ∀ (h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ insert i s, X i) ω)) μ
have h_rec₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
Tactic: specialize h_rec this
Cleared hypotheses: h_rec
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_int : ∀ i_1 ∈ insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
h_rec : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ insert i s, X i) ω)) μ
have insert : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * HAdd.hAdd (β := Ω → ℝ) (X i) (∑ x ∈ s, X x) ω)) μ
Tactic: rw [sum_insert hi_notin_s]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_int : ∀ i_1 ∈ insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
h_rec : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * HAdd.hAdd (β := Ω → ℝ) (X i) (∑ x ∈ s, X x) ω)) μ
have insert : X i ⟂ᵢ[μ] ∑ x ∈ s, X x
Tactic: refine IndepFun.integrable_exp_mul_add ?_ (h_int i (mem_insert_self _ _)) h_rec
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
have empty : ∀ (h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
  Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
Tactic: induction s using Finset.induction_on with
  | empty =>
    simp only [sum_apply, sum_empty, mul_zero, exp_zero]
    exact integrable_const _
  | insert i s hi_notin_s h_rec =>
    have : ∀ i : ι, i ∈ s → Integrable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
    specialize h_rec this
    rw [sum_insert hi_notin_s]
    refine IndepFun.integrable_exp_mul_add ?_ (h_int i (mem_insert_self _ _)) h_rec
    exact (h_indep.indepFun_finsetSum_of_notMem h_meas hi_notin_s).symm
Cleared hypotheses: s, h_int
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
empty :
  ∀ (h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
have insert : ∀ (i : ι) (s : Finset ι) (hi_notin_s : i ∉ s)
  (h_rec :
    ∀ (h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
      Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ)
  (h_int : ∀ i_1 ∈ insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ),
  Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ insert i s, X i) ω)) μ
Tactic: induction s using Finset.induction_on with
  | empty =>
    simp only [sum_apply, sum_empty, mul_zero, exp_zero]
    exact integrable_const _
  | insert i s hi_notin_s h_rec =>
    have : ∀ i : ι, i ∈ s → Integrable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
    specialize h_rec this
    rw [sum_insert hi_notin_s]
    refine IndepFun.integrable_exp_mul_add ?_ (h_int i (mem_insert_self _ _)) h_rec
    exact (h_indep.indepFun_finsetSum_of_notMem h_meas hi_notin_s).symm
Cleared hypotheses: s, h_int
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
have empty : ∀ (h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
  Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
Tactic: classical
  induction s using Finset.induction_on with
  | empty =>
    simp only [sum_apply, sum_empty, mul_zero, exp_zero]
    exact integrable_const _
  | insert i s hi_notin_s h_rec =>
    have : ∀ i : ι, i ∈ s → Integrable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
    specialize h_rec this
    rw [sum_insert hi_notin_s]
    refine IndepFun.integrable_exp_mul_add ?_ (h_int i (mem_insert_self _ _)) h_rec
    exact (h_indep.indepFun_finsetSum_of_notMem h_meas hi_notin_s).symm
Cleared hypotheses: s, h_int
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
empty :
  ∀ (h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
have insert : ∀ (i : ι) (s : Finset ι) (hi_notin_s : i ∉ s)
  (h_rec :
    ∀ (h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
      Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ)
  (h_int : ∀ i_1 ∈ insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ),
  Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ insert i s, X i) ω)) μ
Tactic: classical
  induction s using Finset.induction_on with
  | empty =>
    simp only [sum_apply, sum_empty, mul_zero, exp_zero]
    exact integrable_const _
  | insert i s hi_notin_s h_rec =>
    have : ∀ i : ι, i ∈ s → Integrable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
    specialize h_rec this
    rw [sum_insert hi_notin_s]
    refine IndepFun.integrable_exp_mul_add ?_ (h_int i (mem_insert_self _ _)) h_rec
    exact (h_indep.indepFun_finsetSum_of_notMem h_meas hi_notin_s).symm
Cleared hypotheses: s, h_int
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
have this : IsProbabilityMeasure μ
Tactic: have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
⊢ mgf (∑ i ∈ insert i s, X i) μ t = ∏ i ∈ insert i s, mgf (X i) μ t
have h_int' : ∀ (i : ι), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
Tactic: have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
      ((h_meas i).const_mul t).exp.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
h_int' : ∀ (i : ι), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ mgf (∑ i ∈ insert i s, X i) μ t = ∏ i ∈ insert i s, mgf (X i) μ t
have insert : mgf (X i + ∑ x ∈ s, X x) μ t = ∏ i ∈ insert i s, mgf (X i) μ t
Tactic: rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
h_int' : ∀ (i : ι), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
insert : mgf (X i + ∑ x ∈ s, X x) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
⊢ mgf (∑ i ∈ Insert.insert i s, X i) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
have insert₁ : mgf (X i) μ t * mgf (∑ j ∈ s, X j) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
Tactic: rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
h_int' : ∀ (i : ι), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
insert : mgf (X i + ∑ x ∈ s, X x) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
insert₁ : mgf (X i) μ t * mgf (∑ j ∈ s, X j) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
⊢ mgf (∑ i ∈ Insert.insert i s, X i) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
have insert₂ : mgf (X i) μ t * ∏ i ∈ s, mgf (X i) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
Tactic: rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
h_int' : ∀ (i : ι), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
insert : mgf (X i + ∑ x ∈ s, X x) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
insert₁ : mgf (X i) μ t * mgf (∑ j ∈ s, X j) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
insert₂ : mgf (X i) μ t * ∏ i ∈ s, mgf (X i) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
⊢ mgf (∑ i ∈ Insert.insert i s, X i) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
have insert₃ : mgf (X i) μ t * ∏ i ∈ s, mgf (X i) μ t = mgf (X i) μ t * ∏ x ∈ s, mgf (X x) μ t
Tactic: rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
this : IsProbabilityMeasure μ
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
have empty : mgf (∑ i ∈ ∅, X i) μ t = ∏ i ∈ ∅, mgf (X i) μ t
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi_notin_s h_rec =>
    have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
      ((h_meas i).const_mul t).exp.aestronglyMeasurable
    rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Probability.Moments.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
this : IsProbabilityMeasure μ
empty : mgf (∑ i ∈ ∅, X i) μ t = ∏ i ∈ ∅, mgf (X i) μ t
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
have insert : ∀ (i : ι) (s : Finset ι) (hi_notin_s : i ∉ s) (h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t),
  mgf (∑ i ∈ insert i s, X i) μ t = ∏ i ∈ insert i s, mgf (X i) μ t
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi_notin_s h_rec =>
    have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
      ((h_meas i).const_mul t).exp.aestronglyMeasurable
    rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]
Cleared hypotheses: s