Has Indep Increments is Gaussian Process

lemma HasIndepIncrements.isGaussianProcess [LinearOrder T] [OrderBot T]    [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]    [SecondCountableTopology E] [CompleteSpace E]    {X : T → Ω → E} (law : ∀ t, HasGaussianLaw (X t) P) (h_bot : ∀ᵐ ω ∂P, X ⊥ ω = 0)    (incr : HasIndepIncrements X P) :    IsGaussianProcess X P where  hasGaussianLaw I := by    have := (law ⊥).isProbabilityMeasure    obtain rfl | hI := I.eq_empty_or_nonempty    · constructor      have : P.map (fun ω ↦ Finset.restrict ∅ fun x ↦ X x ω) = .dirac Classical.ofNonempty := by        ext s -        apply Subsingleton.set_cases (p := fun s ↦ Measure.map _ _ s = _)        · simp        simp only [measure_univ]        exact @measure_univ _ _ _          (Measure.isProbabilityMeasure_map (aemeasurable_pi_lambda _ fun _ ↦ (law _).aemeasurable))      rw [this]      infer_instance    have := incrementsToRestrict_increments_ofFin'_ae_eq_restrict ℝ h_bot I    refine @HasGaussianLaw.congr _ _ _ _ _ _ _ _ _ _ ?_ this.symm    refine HasGaussianLaw.map ?_ _    exact (incr _ _ (monotone_ofFin' I)).hasGaussianLaw fun i ↦      incr.indepFun_eval_sub bot_le        (monotone_ofFin' I (Fin.castSucc_le_succ i)) h_bot          |>.hasGaussianLaw_sub_of_sub (law _) (law _)