diff --git a/Analysis/MeasureTheory/Section_1_2_0.lean b/Analysis/MeasureTheory/Section_1_2_0.lean
index 93e4cfa53..a0660cbec 100644
--- a/Analysis/MeasureTheory/Section_1_2_0.lean
+++ b/Analysis/MeasureTheory/Section_1_2_0.lean
@@ -575,7 +575,8 @@ example :
 
 /-- Exercise 1.2.2 -/
 -- The pointwise limit of uniformly bounded Riemann integrable functions need not be Riemann integrable.
-example : ∃ f: ℕ → ℝ → ℝ, ∃ F: ℝ → ℝ, ∃ M, ∀ n, ∀ x ∈ Set.Icc 0 1, |f n x| ≤ M ∧
+example : ∃ f: ℕ → ℝ → ℝ, ∃ F: ℝ → ℝ,
+    (∃ M, ∀ n, ∀ x ∈ Set.Icc 0 1, |f n x| ≤ M) ∧
     (∀ x ∈ Set.Icc 0 1, Filter.atTop.Tendsto (fun n ↦ f n x) (nhds (F x))) ∧
     (∀ n, RiemannIntegrableOn (f n) (Icc 0 1)) ∧
     ¬ RiemannIntegrableOn F (Icc 0 1) := by