-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
calc :
  Eq (α := ℂ) (∫ (x : ℝ), cexp (z * (↑x : ℂ)) ∂gaussianReal μ v)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑(gaussianPDFReal μ v x) : ℂ) * cexp (z * (↑x : ℂ)))
calc₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑(gaussianPDFReal μ v x) : ℂ) * cexp (z * (↑x : ℂ))) =
    (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(↑(↑(2 * v)⁻¹ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
calc₂ :
  ((↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(↑(↑(2 * v)⁻¹ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))) =
    (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))
calc₃ :
  (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ))) =
    1 *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))
calc₄ :
  1 *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ))) =
    cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
⊢ complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)

Tactic:
calc ∫ x, cexp (z * x) ∂gaussianReal μ v
    _ = ∫ x, gaussianPDFReal μ v x * cexp (z * x) ∂ℙ := by
      simp_rw [integral_gaussianReal_eq_integral_smul hv, Complex.real_smul]
    _ = (√(2 * π * v))⁻¹
        * ∫ x : ℝ, cexp (-(2 * v)⁻¹ * x ^ 2 + (z + μ / v) * x + -μ ^ 2 / (2 * v)) ∂ℙ := by
      unfold gaussianPDFReal
      push_cast
      simp_rw [mul_assoc, integral_const_mul, ← Complex.exp_add]
      congr with x
      congr 1
      ring
    _ = (√(2 * π * v))⁻¹ * (π / - -(2 * v)⁻¹) ^ (1 / 2 : ℂ)
        * cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) := by
      rw [integral_cexp_quadratic (by simpa using pos_iff_ne_zero.mpr hv), ← mul_assoc]
    _ = 1 * cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) := by
      congr 1
      simp only [field, sqrt_eq_rpow, one_div, ofReal_inv, NNReal.coe_inv, NNReal.coe_mul,
        NNReal.coe_ofNat, ofReal_mul, ofReal_ofNat, neg_neg, div_inv_eq_mul,
        ne_eq, ofReal_eq_zero, rpow_eq_zero, not_false_eq_true]
      rw [Complex.ofReal_cpow (by positivity)]
      push_cast
      ring_nf
    _ = cexp (z * μ + v * z ^ 2 / 2) := by
      rw [one_mul]
      congr 1
      have : (v : ℂ) ≠ 0 := by simpa
      simp [field]
      ring

Premises used: Real.pi, HMul.hMul, HSub.hSub, ProbabilityTheory.gaussianReal, HDiv.hDiv, Complex.ofReal, Inv.inv, HPow.hPow, HAdd.hAdd, Complex.exp, Real.sqrt, OfNat.ofNat, NNReal.toReal, Neg.neg