{E : Type u_1} →
  [inst : TopologicalSpace E] →
    [inst_1 : AddCommMonoid E] →
      [inst_2 : Module ℝ E] →
        {mE : MeasurableSpace E} →
          {μ : MeasureTheory.Measure E} →
            {motive : ProbabilityTheory.IsGaussian μ → Sort u} →
              (t : ProbabilityTheory.IsGaussian μ) →
                ((map_eq_gaussianReal :
                      ∀ (L : StrongDual ℝ E),
                        MeasureTheory.Measure.map (⇑L) μ =
                          ProbabilityTheory.gaussianReal (∫ (x : E), L x ∂μ)
                            (ProbabilityTheory.variance (⇑L) μ).toNNReal) →
                    motive ⋯) →
                  motive t