Use dot notation

fpvandoorn · Jul 25, 2024 · 42b0222 · 42b0222
1 parent dc3c491
commit 42b0222
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Carleson/Classical/CarlesonOnTheRealLine.lean b/Carleson/Classical/CarlesonOnTheRealLine.lean
@@ -569,7 +569,7 @@ instance h6 : IsOneSidedKernel 4 K where
         · norm_num
       · norm_num
   /- Lemma ?-/
-  measurable_K_left := fun y ↦ Measurable.of_uncurry_right Hilbert_kernel_measurable
+  measurable_K_left := fun y ↦ Hilbert_kernel_measurable.of_uncurry_right
   /- Lemma ?-/
   measurable_K_right := Hilbert_kernel_measurable