style fixes

leanprover-community · Oct 3, 2024 · 1e7c736 · 1e7c736
1 parent f67bf07
commit 1e7c736
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/Mathlib/MeasureTheory/Function/L1Space.lean b/Mathlib/MeasureTheory/Function/L1Space.lean
@@ -1146,7 +1146,7 @@ theorem Integrable.im (hf : Integrable f μ) : Integrable (fun x => RCLike.im (f
   exact hf.im
 
 lemma Integrable.iff_ofReal {f : α → ℝ} : Integrable f μ ↔ Integrable (fun x ↦ (f x : ℂ)) μ :=
-    ⟨fun hf ↦ hf.ofReal, fun hf ↦ hf.re⟩
+  ⟨fun hf ↦ hf.ofReal, fun hf ↦ hf.re⟩
 
 end RCLike
 

diff --git a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean
@@ -700,7 +700,7 @@ namespace MeasureTheory
 variable {X : Type*} [MeasurableSpace X] {𝕜 : Type*} [RCLike 𝕜] {μ : Measure X} {s : Set X}
 theorem IntegrableOn.iff_ofReal {f : X → ℝ} :
     IntegrableOn f s μ ↔ IntegrableOn (fun x ↦ (f x : ℂ)) s μ :=
-    MeasureTheory.Integrable.iff_ofReal
+  MeasureTheory.Integrable.iff_ofReal
 
 theorem IntegrableOn.ofReal {f : X → ℝ} (hf : IntegrableOn f s μ) :
     IntegrableOn (fun x => (f x : 𝕜)) s μ := by
@@ -712,7 +712,7 @@ theorem IntegrableOn.re_im_iff {f : X → 𝕜} :
     IntegrableOn f s μ := Integrable.re_im_iff (f := f)
 
 theorem IntegrableOn.re {f : X → 𝕜} (hf : IntegrableOn f s μ) :
-    IntegrableOn (fun x => RCLike.re (f x)) s μ  := (IntegrableOn.re_im_iff.2 hf).left
+    IntegrableOn (fun x => RCLike.re (f x)) s μ := (IntegrableOn.re_im_iff.2 hf).left
 
 theorem IntegrableOn.im {f : X → 𝕜} (hf : IntegrableOn f s μ) :
     IntegrableOn (fun x => RCLike.im (f x)) s μ := (IntegrableOn.re_im_iff.2 hf).right

diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
@@ -602,10 +602,10 @@ nonrec theorem integral_ofReal {a b : ℝ} {μ : Measure ℝ} {f : ℝ → ℝ}
 theorem intervalIntegral_re {μ : Measure ℝ} {a b : ℝ} {f : ℝ → ℂ} (hab: a ≤ b)
     (hf: IntervalIntegrable f μ a b) :
     (∫ x in (a)..b, (f x).re ∂μ) = (∫ x in (a)..b, f x ∂μ).re := by
-    repeat rw [intervalIntegral.integral_of_le hab]
-    apply setIntegral_re
-    rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le hab]
-    exact hf
+  repeat rw [intervalIntegral.integral_of_le hab]
+  apply setIntegral_re
+  rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le hab]
+  exact hf
 
 section ContinuousLinearMap