awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
t : ℝ
h₁ :
  cexp
      ((↑(HMul.hMul (β := ℝ) t ((L : (a : E) → ℝ) m : ℝ)) : ℂ) * I -
        (↑(t *
                HMul.hMul (β := ℝ) t
                  ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L :
                    ℝ)) :
            ℂ) /
          2) =
    cexp
      ((↑t : ℂ) * (↑((L : (a : E) → ℝ) m) : ℂ) * I -
        (↑(↑(Real.toNNReal
                      ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                          (a : StrongDual ℝ E) → ℝ)
                        L)) :
                  ℝ) :
              ℂ) *
            HPow.hPow (β := ℕ) (↑t : ℂ) 2 /
          2)
⊢ charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) t =
    charFun
      (gaussianReal ((L : (a : E) → ℝ) m)
        (Real.toNNReal
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L)))
      t

Tactic:
simp_rw [charFun_map_eq_charFunDual_smul, h, charFun_gaussianReal,
    smul_apply, map_smul, smul_apply, smul_eq_mul]

Premises used: ContinuousLinearMap.smul_apply, smul_eq_mul, MeasureTheory.charFun_map_eq_charFunDual_smul, ProbabilityTheory.charFun_gaussianReal, map_smul
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
t : ℝ
h₁ :
  cexp
      ((↑(HMul.hMul (β := ℝ) t ((L : (a : E) → ℝ) m : ℝ)) : ℂ) * I -
        (↑(t *
                HMul.hMul (β := ℝ) t
                  ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L :
                    ℝ) /
              2) :
          ℂ)) =
    cexp
      ((↑(HMul.hMul (β := ℝ) t ((L : (a : E) → ℝ) m : ℝ)) : ℂ) * I -
        (↑((↑(Real.toNNReal
                      ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                          (a : StrongDual ℝ E) → ℝ)
                        L)) :
                  ℝ) *
                HPow.hPow (β := ℕ) t 2 /
              2) :
          ℂ))
⊢ cexp
      ((↑(HMul.hMul (β := ℝ) t ((L : (a : E) → ℝ) m : ℝ)) : ℂ) * I -
        (↑(t *
                HMul.hMul (β := ℝ) t
                  ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L :
                    ℝ)) :
            ℂ) /
          2) =
    cexp
      ((↑t : ℂ) * (↑((L : (a : E) → ℝ) m) : ℂ) * I -
        (↑(↑(Real.toNNReal
                      ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                          (a : StrongDual ℝ E) → ℝ)
                        L)) :
                  ℝ) :
              ℂ) *
            HPow.hPow (β := ℕ) (↑t : ℂ) 2 /
          2)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
t : ℝ
h₁ :
  t *
        HMul.hMul (β := ℝ) t
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
              L :
            ℝ) /
      2 =
    (↑(Real.toNNReal
              ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                L)) :
          ℝ) *
        HPow.hPow (β := ℕ) t 2 /
      2
⊢ cexp
      ((↑(HMul.hMul (β := ℝ) t ((L : (a : E) → ℝ) m : ℝ)) : ℂ) * I -
        (↑(t *
                HMul.hMul (β := ℝ) t
                  ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L :
                    ℝ) /
              2) :
          ℂ)) =
    cexp
      ((↑(HMul.hMul (β := ℝ) t ((L : (a : E) → ℝ) m : ℝ)) : ℂ) * I -
        (↑((↑(Real.toNNReal
                      ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                          (a : StrongDual ℝ E) → ℝ)
                        L)) :
                  ℝ) *
                HPow.hPow (β := ℕ) t 2 /
              2) :
          ℂ))

Tactic:
congrm exp (_ - ofReal ?_)

Premises used: HSub.hSub, Complex.ofReal, Complex.exp
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
t : ℝ
h₁ :
  t *
        HMul.hMul (β := ℝ) t
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
              L :
            ℝ) /
      2 =
    HMul.hMul (α := ℝ)
        ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L :
          ℝ)
        (HPow.hPow (β := ℕ) t 2) /
      2
h₂ :
  LE.le (α := ℝ) (0 : ℝ)
    ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ) L :
      ℝ)
⊢ t *
        HMul.hMul (β := ℝ) t
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
              L :
            ℝ) /
      2 =
    (↑(Real.toNNReal
              ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                L)) :
          ℝ) *
        HPow.hPow (β := ℕ) t 2 /
      2

Tactic:
rw [Real.coe_toNNReal]

Premises used: Real.coe_toNNReal
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
t : ℝ
⊢ t *
        HMul.hMul (β := ℝ) t
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
              L :
            ℝ) /
      2 =
    HMul.hMul (α := ℝ)
        ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L :
          ℝ)
        (HPow.hPow (β := ℕ) t 2) /
      2

Tactic:
ring
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
t : ℝ
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ) L :
      ℝ)

Tactic:
hf.nonneg L

Premises used: LinearMap.BilinForm.IsNonneg.nonneg, LinearMap.BilinForm.IsPosSemidef.isNonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
t : ℝ
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ) L :
      ℝ)

Tactic:
exact hf.nonneg L

Premises used: LinearMap.BilinForm.IsNonneg.nonneg, LinearMap.BilinForm.IsPosSemidef.isNonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
⊢ IsGaussian μ

Tactic:
have h' := isGaussian_iff_gaussian_charFunDual.2 ⟨m, f, hf, h⟩
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
h' : IsGaussian μ
⊢ ∀ (L : StrongDual ℝ E),
    ∃ (n : ℤ),
      (↑((L : (a : E) → ℝ) (∫ (x : E), id x ∂μ)) : ℂ) * I -
          (↑((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2 =
        (↑((L : (a : E) → ℝ) m) : ℂ) * I -
            (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                      (a : StrongDual ℝ E) → ℝ)
                    L) :
                ℂ) /
              2 +
          (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
simp_rw [h'.charFunDual_eq', Complex.exp_eq_exp_iff_exists_int] at h

Premises used: Complex.exp_eq_exp_iff_exists_int, ProbabilityTheory.IsGaussian.charFunDual_eq'
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
h :
  ∀ (L : StrongDual ℝ E),
    ∃ (n : ℤ),
      (↑((L : (a : E) → ℝ) (∫ (x : E), id x ∂μ)) : ℂ) * I -
          (↑((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2 =
        (↑((L : (a : E) → ℝ) m) : ℂ) * I -
            (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                      (a : StrongDual ℝ E) → ℝ)
                    L) :
                ℂ) /
              2 +
          (↑n : ℂ) * (2 * (↑π : ℂ) * I)
choose :
  ∀ (n : (L : StrongDual ℝ E) → ℤ)
    (hn :
      ∀ (L : StrongDual ℝ E),
        (↑((L : (a : E) → ℝ) (∫ (x : E), id x ∂μ)) : ℂ) * I -
            (↑((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                      (a : StrongDual ℝ E) → ℝ)
                    L) :
                ℂ) /
              2 =
          (↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2 +
            (↑(n L) : ℂ) * (2 * (↑π : ℂ) * I)),
    m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ

Tactic:
choose n hn using h
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
n : (L : StrongDual ℝ E) → ℤ
hn :
  ∀ (L : StrongDual ℝ E),
    (↑((L : (a : E) → ℝ) (∫ (x : E), id x ∂μ)) : ℂ) * I -
        (↑((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                L) :
            ℂ) /
          2 =
      (↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2 +
        (↑(n L) : ℂ) * (2 * (↑π : ℂ) * I)
L : StrongDual ℝ E
rw :
  (↑(n L) : ℂ) =
    ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2 +
            (↑(n L) : ℂ) * (2 * (↑π : ℂ) * I) -
          (↑((L : (a : E) → ℝ) m) : ℂ) * I +
        (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
                L) :
            ℂ) /
          2) /
      (2 * (↑π : ℂ) * I)
⊢ (↑(n L) : ℂ) =
    ((↑((L : (a : E) → ℝ) (∫ (x : E), id x ∂μ)) : ℂ) * I -
            (↑((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                      (a : StrongDual ℝ E) → ℝ)
                    L) :
                ℂ) /
              2 -
          (↑((L : (a : E) → ℝ) m) : ℂ) * I +
        (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
                L) :
            ℂ) /
          2) /
      (2 * (↑π : ℂ) * I)

Tactic:
rw [hn L]
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
n : (L : StrongDual ℝ E) → ℤ
hn :
  ∀ (L : StrongDual ℝ E),
    (↑((L : (a : E) → ℝ) (∫ (x : E), id x ∂μ)) : ℂ) * I -
        (↑((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                L) :
            ℂ) /
          2 =
      (↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2 +
        (↑(n L) : ℂ) * (2 * (↑π : ℂ) * I)
L : StrongDual ℝ E
field_simp :
  (↑(n L) : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑π : ℂ) =
    (↑((L : (a : E) → ℝ) m) : ℂ) * I * 2 -
            (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) +
          (↑(n L) : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑π : ℂ) -
        (↑((L : (a : E) → ℝ) m) : ℂ) * I * 2 +
      (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L) :
        ℂ)
⊢ (↑(n L) : ℂ) =
    ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2 +
            (↑(n L) : ℂ) * (2 * (↑π : ℂ) * I) -
          (↑((L : (a : E) → ℝ) m) : ℂ) * I +
        (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
                L) :
            ℂ) /
          2) /
      (2 * (↑π : ℂ) * I)

Tactic:
field_simp
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
n : (L : StrongDual ℝ E) → ℤ
hn :
  ∀ (L : StrongDual ℝ E),
    (↑((L : (a : E) → ℝ) (∫ (x : E), id x ∂μ)) : ℂ) * I -
        (↑((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                L) :
            ℂ) /
          2 =
      (↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2 +
        (↑(n L) : ℂ) * (2 * (↑π : ℂ) * I)
L : StrongDual ℝ E
⊢ (↑(n L) : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑π : ℂ) =
    (↑((L : (a : E) → ℝ) m) : ℂ) * I * 2 -
            (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) +
          (↑(n L) : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑π : ℂ) -
        (↑((L : (a : E) → ℝ) m) : ℂ) * I * 2 +
      (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L) :
        ℂ)

Tactic:
ring