awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ DifferentiableAt ℝ (F := ℝ) (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v
have hc : DifferentiableAt ℝ (iteratedDeriv 1 (mgf X μ)) v
Tactic: rw [h_d_mgf.symm.differentiableAt_iff, ← iteratedDeriv_one]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ)) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2
have rw : (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
      HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ)) /
    HPow.hPow (β := ℕ) (mgf X μ v) 2 =
  (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
      HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ)) /
    HPow.hPow (β := ℕ) (mgf X μ v) 2
Tactic: rw [deriv_mgf h]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ)) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have rw : deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / HPow.hPow (β := ℕ) (mgf X μ v) 2 -
    HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
  deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
Tactic: rw [sub_div]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / HPow.hPow (β := ℕ) (mgf X μ v) 2 -
      HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) /
        HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have e_a : deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / HPow.hPow (β := ℕ) (mgf X μ v) 2 =
  deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
e_a :
  deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v
⊢ deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / HPow.hPow (β := ℕ) (mgf X μ v) 2 -
      HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) /
        HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have e_a₁ : HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) /
    HPow.hPow (β := ℕ) (mgf X μ v) 2 =
  HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v
have e_a : mgf X μ v ≠ 0
Tactic: rw [pow_two, div_mul_eq_div_div, mul_div_assoc, div_self, mul_one]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have e_a : HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) /
    HPow.hPow (β := ℕ) (mgf X μ v) 2 =
  HPow.hPow (β := ℕ) ((∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v) 2
Tactic: rw [deriv_cgf h]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have e_a : Eq (α := ℝ) (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v)
  (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ Eq (α := ℝ) (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v)
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ)
have h₁ : Eq (α := ℝ) (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v)
  (deriv (fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 1 * rexp (t * X ω)) x ∂μ) v)
Tactic: convert! (hasDerivAt_integral_pow_mul_exp_real h 1).deriv using 1
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ deriv (fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have calc : deriv (fun (u : ℝ) ↦ (∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) / mgf X μ u) v =
  (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
    HPow.hPow (β := ℕ) (mgf X μ v) 2
Tactic: calc deriv (fun u ↦ (∫ ω, X ω * exp (u * X ω) ∂μ) / mgf X μ u) v
  _ = (deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ ω, X ω * exp (v * X ω) ∂μ) * deriv (mgf X μ) v) / mgf X μ v ^ 2 := by
    rw [deriv_fun_div]
    · rw [h_d_mgf.symm.differentiableAt_iff, ← iteratedDeriv_one]
      exact differentiableAt_iteratedDeriv_mgf h 1
    · exact differentiableAt_mgf h
    · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
  _ = (deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ ω, X ω * exp (v * X ω) ∂μ) * ∫ ω, X ω * exp (v * X ω) ∂μ) / mgf X μ v ^ 2 := by
    rw [deriv_mgf h]
  _ = deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v / mgf X μ v - deriv (cgf X μ) v ^ 2 := by
    rw [sub_div]
    congr 1
    · rw [pow_two, div_mul_eq_div_div, mul_div_assoc, div_self, mul_one]
      exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
    · rw [deriv_cgf h]
      ring
  _ = (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2 := by
    congr
    convert! (hasDerivAt_integral_pow_mul_exp_real h 1).deriv using 1
    simp
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
calc :
  deriv (fun (u : ℝ) ↦ (∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) / mgf X μ u) v =
    (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2
⊢ deriv (fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have calc₁ : (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
    HPow.hPow (β := ℕ) (mgf X μ v) 2 =
  (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
      HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ)) /
    HPow.hPow (β := ℕ) (mgf X μ v) 2
Tactic: calc deriv (fun u ↦ (∫ ω, X ω * exp (u * X ω) ∂μ) / mgf X μ u) v
  _ = (deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ ω, X ω * exp (v * X ω) ∂μ) * deriv (mgf X μ) v) / mgf X μ v ^ 2 := by
    rw [deriv_fun_div]
    · rw [h_d_mgf.symm.differentiableAt_iff, ← iteratedDeriv_one]
      exact differentiableAt_iteratedDeriv_mgf h 1
    · exact differentiableAt_mgf h
    · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
  _ = (deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ ω, X ω * exp (v * X ω) ∂μ) * ∫ ω, X ω * exp (v * X ω) ∂μ) / mgf X μ v ^ 2 := by
    rw [deriv_mgf h]
  _ = deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v / mgf X μ v - deriv (cgf X μ) v ^ 2 := by
    rw [sub_div]
    congr 1
    · rw [pow_two, div_mul_eq_div_div, mul_div_assoc, div_self, mul_one]
      exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
    · rw [deriv_cgf h]
      ring
  _ = (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2 := by
    congr
    convert! (hasDerivAt_integral_pow_mul_exp_real h 1).deriv using 1
    simp
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
calc :
  deriv (fun (u : ℝ) ↦ (∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) / mgf X μ u) v =
    (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2
calc₁ :
  (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ)) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2
⊢ deriv (fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have calc₂ : (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
      HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ)) /
    HPow.hPow (β := ℕ) (mgf X μ v) 2 =
  deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
Tactic: calc deriv (fun u ↦ (∫ ω, X ω * exp (u * X ω) ∂μ) / mgf X μ u) v
  _ = (deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ ω, X ω * exp (v * X ω) ∂μ) * deriv (mgf X μ) v) / mgf X μ v ^ 2 := by
    rw [deriv_fun_div]
    · rw [h_d_mgf.symm.differentiableAt_iff, ← iteratedDeriv_one]
      exact differentiableAt_iteratedDeriv_mgf h 1
    · exact differentiableAt_mgf h
    · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
  _ = (deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ ω, X ω * exp (v * X ω) ∂μ) * ∫ ω, X ω * exp (v * X ω) ∂μ) / mgf X μ v ^ 2 := by
    rw [deriv_mgf h]
  _ = deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v / mgf X μ v - deriv (cgf X μ) v ^ 2 := by
    rw [sub_div]
    congr 1
    · rw [pow_two, div_mul_eq_div_div, mul_div_assoc, div_self, mul_one]
      exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
    · rw [deriv_cgf h]
      ring
  _ = (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2 := by
    congr
    convert! (hasDerivAt_integral_pow_mul_exp_real h 1).deriv using 1
    simp
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
calc :
  deriv (fun (u : ℝ) ↦ (∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) / mgf X μ u) v =
    (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2
calc₁ :
  (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ)) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2
calc₂ :
  (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ)) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
⊢ deriv (fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
have calc₃ : deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
  (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
Tactic: calc deriv (fun u ↦ (∫ ω, X ω * exp (u * X ω) ∂μ) / mgf X μ u) v
  _ = (deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ ω, X ω * exp (v * X ω) ∂μ) * deriv (mgf X μ) v) / mgf X μ v ^ 2 := by
    rw [deriv_fun_div]
    · rw [h_d_mgf.symm.differentiableAt_iff, ← iteratedDeriv_one]
      exact differentiableAt_iteratedDeriv_mgf h 1
    · exact differentiableAt_mgf h
    · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
  _ = (deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ ω, X ω * exp (v * X ω) ∂μ) * ∫ ω, X ω * exp (v * X ω) ∂μ) / mgf X μ v ^ 2 := by
    rw [deriv_mgf h]
  _ = deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v / mgf X μ v - deriv (cgf X μ) v ^ 2 := by
    rw [sub_div]
    congr 1
    · rw [pow_two, div_mul_eq_div_div, mul_div_assoc, div_self, mul_one]
      exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
    · rw [deriv_cgf h]
      ring
  _ = (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2 := by
    congr
    convert! (hasDerivAt_integral_pow_mul_exp_real h 1).deriv using 1
    simp
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
⊢ iteratedDeriv 2 (cgf X μ) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v
have pos : ∀ (hμ : μ = 0),
  iteratedDeriv 2 (cgf X μ) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
pos :
  ∀ (hμ : μ = 0),
    iteratedDeriv 2 (cgf X μ) v =
      (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v
⊢ iteratedDeriv 2 (cgf X μ) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v
have neg : ∀ (hμ : ¬μ = 0),
  iteratedDeriv 2 (cgf X μ) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ iteratedDeriv 2 (cgf X μ) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v
have neg : (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
  (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v
Tactic: rw [iteratedDeriv_two_cgf h]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
          HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v) /
      mgf X μ v
have rw : (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
  (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v -
    (HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v / mgf X μ v)
Tactic: rw [add_div, sub_div, sub_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v -
      (HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v / mgf X μ v -
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v / mgf X μ v)
have e_a : HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
  HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v / mgf X μ v -
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v / mgf X μ v
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v / mgf X μ v
have e_a : HPow.hPow (β := ℕ) ((∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v) 2 =
  HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) *
        ((∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v) /
      mgf X μ v -
    HPow.hPow (β := ℕ) ((∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v) 2
Tactic: rw [mul_div_cancel_right₀, deriv_cgf h]