refactor(MeasureTheory/Integral/DominatedConvergence): golf and format

Author: Deep0Thinking

Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

@@ -472,8 +472,7 @@ theorem continuousOn_primitive (h_int : IntegrableOn f (Icc a b) μ) :
     rw [continuousOn_congr this]
     intro x₀ _
     refine continuousWithinAt_primitive (measure_singleton x₀) ?_
-    simp only [intervalIntegrable_iff_integrableOn_Ioc_of_le, max_eq_right, h,
-      min_self]
+    simp only [intervalIntegrable_iff_integrableOn_Ioc_of_le, max_eq_right, h, min_self]
     exact h_int.mono Ioc_subset_Icc_self le_rfl
   · rw [Icc_eq_empty h]
     exact continuousOn_empty _
@@ -645,8 +644,8 @@ open intervalIntegral
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure ℝ} {f : ℝ → E}
 
-theorem continuousWithinAt_Ici_primitive_Ioi {a₀ : ℝ} (hf : IntegrableOn f (Ioi a₀) μ)
-    : ContinuousWithinAt (fun b ↦ ∫ x in Ioi b, f x ∂μ) (Ici a₀) a₀ := by
+theorem continuousWithinAt_Ici_primitive_Ioi {a₀ : ℝ} (hf : IntegrableOn f (Ioi a₀) μ) :
+    ContinuousWithinAt (fun b ↦ ∫ x in Ioi b, f x ∂μ) (Ici a₀) a₀ := by
   simp_rw [← integral_indicator measurableSet_Ioi]
   apply tendsto_integral_filter_of_dominated_convergence ((Ioi a₀).indicator (norm ∘ f))
   · filter_upwards [self_mem_nhdsWithin] with a ha
@@ -665,14 +664,12 @@ theorem continuousWithinAt_Ici_primitive_Ioi {a₀ : ℝ} (hf : IntegrableOn f (
 
 theorem continuousOn_Ici_primitive_Ioi [NoAtoms μ] {a₀ : ℝ} (hf : IntegrableOn f (Ioi a₀) μ) :
     ContinuousOn (fun b ↦ ∫ x in Ioi b, f x ∂μ) (Ici a₀) := by
-  intro a ha
-  rw [mem_Ici] at ha
+  intro a (ha : a₀ ≤ a)
   rw [continuousWithinAt_iff_continuous_left_right]
   constructor
   · rw [Ici_inter_Iic]
-    have h_int : IntervalIntegrable f μ a₀ a := by
-      rw [intervalIntegrable_iff_integrableOn_Ioc_of_le ha]
-      exact hf.mono_set Ioc_subset_Ioi_self
+    have h_int : IntervalIntegrable f μ a₀ a :=
+      (intervalIntegrable_iff_integrableOn_Ioc_of_le ha).2 <| hf.mono_set Ioc_subset_Ioi_self
     have h_split : ∀ b ∈ Icc a₀ a, ∫ x in Ioi b, f x ∂μ =
         (∫ x in Ioi a₀, f x ∂μ) - ∫ x in a₀..b, f x ∂μ := by
       intro b hb
@@ -682,8 +679,8 @@ theorem continuousOn_Ici_primitive_Ioi [NoAtoms μ] {a₀ : ℝ} (hf : Integrabl
     exact (continuousWithinAt_const.sub h_cwa).congr h_split (h_split a (right_mem_Icc.2 ha))
   · simpa [ha] using (hf.mono_set (Ioi_subset_Ioi ha)).continuousWithinAt_Ici_primitive_Ioi
 
-theorem continuousWithinAt_Iic_primitive_Iio {a₀ : ℝ} (hf : IntegrableOn f (Iio a₀) μ)
-    : ContinuousWithinAt (fun b ↦ ∫ x in Iio b, f x ∂μ) (Iic a₀) a₀ := by
+theorem continuousWithinAt_Iic_primitive_Iio {a₀ : ℝ} (hf : IntegrableOn f (Iio a₀) μ) :
+    ContinuousWithinAt (fun b ↦ ∫ x in Iio b, f x ∂μ) (Iic a₀) a₀ := by
   simp_rw [← integral_indicator measurableSet_Iio]
   apply tendsto_integral_filter_of_dominated_convergence ((Iio a₀).indicator (norm ∘ f))
   · filter_upwards [self_mem_nhdsWithin] with a ha
@@ -702,21 +699,19 @@ theorem continuousWithinAt_Iic_primitive_Iio {a₀ : ℝ} (hf : IntegrableOn f (
 
 theorem continuousOn_Iic_primitive_Iio [NoAtoms μ] {a₀ : ℝ} (hf : IntegrableOn f (Iio a₀) μ) :
     ContinuousOn (fun b ↦ ∫ x in Iio b, f x ∂μ) (Iic a₀) := by
-  intro a ha
-  rw [mem_Iic] at ha
+  intro a (ha : a ≤ a₀)
   rw [continuousWithinAt_iff_continuous_left_right]
   constructor
   · simpa [ha] using (hf.mono_set (Iio_subset_Iio ha)).continuousWithinAt_Iic_primitive_Iio
   · rw [Iic_inter_Ici]
-    have h_int : IntervalIntegrable f μ a a₀ := by
-      rw [intervalIntegrable_iff_integrableOn_Ico_of_le ha]
-      exact hf.mono_set Ico_subset_Iio_self
+    have h_int : IntervalIntegrable f μ a a₀ :=
+      (intervalIntegrable_iff_integrableOn_Ico_of_le ha).2 <| hf.mono_set Ico_subset_Iio_self
     have h_split : ∀ b ∈ Icc a a₀, ∫ x in Iio b, f x ∂μ =
         (∫ x in Iio a₀, f x ∂μ) + ∫ x in a₀..b, f x ∂μ := by
       intro b hb
       simp [integral_symm b a₀, ← integral_Iio_sub_Iio' hf (hf.mono_set (Iio_subset_Iio hb.2))]
-    have h_cwa : ContinuousWithinAt (fun b ↦ ∫ x in a₀..b, f x ∂μ) (Icc a a₀) a := by
-      exact continuousWithinAt_primitive (measure_singleton a) (by simpa [ha])
+    have h_cwa : ContinuousWithinAt (fun b ↦ ∫ x in a₀..b, f x ∂μ) (Icc a a₀) a :=
+      continuousWithinAt_primitive (measure_singleton a) (by simpa [ha])
     exact (continuousWithinAt_const.add h_cwa).congr h_split (h_split a (left_mem_Icc.2 ha))
 
 theorem continuousOn_Ici_primitive_Ici [NoAtoms μ] {a₀ : ℝ} (hf : IntegrableOn f (Ici a₀) μ) :