[pre-commit.ci lite] apply automatic fixes

Author: pre-commit-ci-lite[bot]

Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

@@ -314,8 +314,8 @@ lemma exists_integral_div_eq_mul_log {a b : ℝ} {f : ℝ → ℝ} {y : ℝ} (a_
   rw [mul_div_mul_right b a (ne_of_gt y_pos)] at heq
   exact ⟨c, hc, heq⟩
 
-/-- **Frullani integral**. 
-If `f : ℝ → ℝ` is continuous on `[0, ∞)` with `Tendsto f atTop (𝓝 L)`, and `0 < a`, `0 < b`, then 
+/-- **Frullani integral**.
+If `f : ℝ → ℝ` is continuous on `[0, ∞)` with `Tendsto f atTop (𝓝 L)`, and `0 < a`, `0 < b`, then
 `∫ x in Ioi 0, (f (a * x) - f (b * x)) / x = (f 0 - L) * log (b / a)`. -/
 theorem integral_Ioi
     {a b : ℝ} {f : ℝ → ℝ} {L : ℝ} (a_pos : 0 < a) (b_pos : 0 < b) (hf : ContinuousOn f (Ici 0))

Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

@@ -624,7 +624,7 @@ theorem intervalIntegral_tendsto_integral_Ioi (a : ℝ) (hfi : IntegrableOn f (I
 end IntegralOfIntervalIntegral
 
 theorem IntegrableOn.tendsto_integral_Ioi {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
-    {a : ℝ} {g : ℝ → E} (hg : IntegrableOn g (Ioi a)) : 
+    {a : ℝ} {g : ℝ → E} (hg : IntegrableOn g (Ioi a)) :
     Tendsto (fun ε : ℝ ↦ ∫ x in Ioi ε, g x) (𝓝[>] a) (𝓝 (∫ x in Ioi a, g x)) := by
   have hg' : IntervalIntegrable g volume a (a + 1) := by
     rw [intervalIntegrable_iff_integrableOn_Ioc_of_le (by linarith)]

Mathlib/Topology/Algebra/Monoid.lean

@@ -72,12 +72,12 @@ theorem continuous_mul_right (a : M) : Continuous fun b : M => b * a := by fun_p
 
 @[to_additive]
 theorem ContinuousOn.comp_mul_left {f : M → X} {s t : Set M} {c : M} (hf : ContinuousOn f t)
-    (hct : Set.MapsTo (fun x : M => c * x) s t) : ContinuousOn (fun x => f (c * x)) s := 
+    (hct : Set.MapsTo (fun x : M => c * x) s t) : ContinuousOn (fun x => f (c * x)) s :=
   hf.comp (continuous_mul_left c).continuousOn hct
 
 @[to_additive]
 theorem ContinuousOn.comp_mul_right {f : M → X} {s t : Set M} {c : M} (hf : ContinuousOn f t)
-    (hct : Set.MapsTo (fun x : M => x * c) s t) : ContinuousOn (fun x => f (x * c)) s := 
+    (hct : Set.MapsTo (fun x : M => x * c) s t) : ContinuousOn (fun x => f (x * c)) s :=
   hf.comp (continuous_mul_right c).continuousOn hct
 
 @[to_additive]