-- Module: Mathlib.Probability.Moments.MGFAnalytic
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
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
⊢ 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

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

Premises used: HMul.hMul, ProbabilityTheory.cgf, deriv, HSub.hSub, HDiv.hDiv, Real.exp, HPow.hPow, MeasureTheory.integral, ProbabilityTheory.mgf, OfNat.ofNat