perf(Probability/Kernel/Disintegration/Density): smile more (leanprover-community#30819)

Reverts an unintentional regression from leanprover-community#30691 ([benchmark output](https://leanprover.zulipchat.com/#narrow/channel/116290-rss/topic/Benchmark.20results.20for.20mathlib4/near/546585656)).
There was even a comment about this already.
Without this, elaborating the first two lemmas takes 8--10 seconds on my fast computer.

Add one more smile (without it, the exact takes half a second on my computer).

Author: grunweg

Mathlib/Probability/Kernel/Disintegration/Density.lean

@@ -135,18 +135,19 @@ lemma measurable_densityProcess (κ : Kernel α (γ × β)) (ν : Kernel α γ)
 lemma measurable_densityProcess_left (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ)
     (x : γ) {s : Set β} (hs : MeasurableSet s) :
     Measurable (fun a ↦ densityProcess κ ν n a x s) :=
-  (measurable_densityProcess κ ν n hs).comp (measurable_id.prodMk measurable_const)
+  ((measurable_densityProcess κ ν n hs).comp (measurable_id.prodMk measurable_const):)
 
 lemma measurable_densityProcess_right (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ)
     {s : Set β} (a : α) (hs : MeasurableSet s) :
     Measurable (fun x ↦ densityProcess κ ν n a x s) :=
-  (measurable_densityProcess κ ν n hs).comp (measurable_const.prodMk measurable_id)
+  ((measurable_densityProcess κ ν n hs).comp (measurable_const.prodMk measurable_id):)
 
 lemma measurable_countableFiltration_densityProcess (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ)
     (a : α) {s : Set β} (hs : MeasurableSet s) :
     Measurable[countableFiltration γ n] (fun x ↦ densityProcess κ ν n a x s) := by
   refine @Measurable.ennreal_toReal _ (countableFiltration γ n) _ ?_
-  exact (measurable_densityProcess_countableFiltration_aux κ ν n hs).comp measurable_prodMk_left
+  -- The exact also works without the `( :)`, but is a bit slow.
+  exact ((measurable_densityProcess_countableFiltration_aux κ ν n hs).comp measurable_prodMk_left :)
 
 lemma stronglyMeasurable_countableFiltration_densityProcess (κ : Kernel α (γ × β)) (ν : Kernel α γ)
     (n : ℕ) (a : α) {s : Set β} (hs : MeasurableSet s) :