Compactify code, as suggested by reviewers

Mathlib/Analysis/SpecialFunctions/Integrals.lean

@@ -248,15 +248,13 @@ theorem intervalIntegrable_log' : IntervalIntegrable log volume a b := by
     · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
     · intro s ⟨hs, _⟩
       norm_num at *
-      have h := (hasDerivAt_id s).sub (hasDerivAt_mul_log hs.ne.symm)
-      simp only [id_eq, sub_add_cancel_right] at h
-      exact h
+      simpa using (hasDerivAt_id s).sub (hasDerivAt_mul_log hs.ne.symm)
     · intro s ⟨hs₁, hs₂⟩
       norm_num at *
       exact (log_nonpos_iff hs₁).mpr hs₂.le
   · -- Show integrability on [1…t] by continuity
     apply ContinuousOn.intervalIntegrable
-    apply ContinuousOn.mono Real.continuousOn_log
+    apply Real.continuousOn_log.mono
     apply Set.not_mem_uIcc_of_lt zero_lt_one at hx
     simpa
 
@@ -494,9 +492,7 @@ lemma integral_log_from_zero_of_pos (ht : 0 < b) : ∫ s in (0)..b, log s = b *
   · abel
   · exact ht
   · intro s ⟨hs, _ ⟩
-    have h := (hasDerivAt_mul_log hs.ne.symm).sub (hasDerivAt_id s)
-    simp only [id_eq, add_sub_cancel_right] at h
-    exact h
+    simpa using (hasDerivAt_mul_log hs.ne.symm).sub (hasDerivAt_id s)
   · have h := tendsto_log_mul_rpow_nhds_zero zero_lt_one
     simp_rw [rpow_one, mul_comm] at h
     replace h := h.sub (tendsto_nhdsWithin_of_tendsto_nhds Filter.tendsto_id)

Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

@@ -399,22 +399,19 @@ lemma intervalIntegrable_of_even₀ (h₁f : ∀ x, f x = f (-x))
 if it is interval integrable (with respect to the volume measure) on every interval of the form
 `0..x`, for positive `x`. -/
 theorem intervalIntegrable_of_even
-  (h₁f : ∀ x, f x = f (-x))
-  (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) :
-  ∀ x y, IntervalIntegrable f volume x y :=
+  (h₁f : ∀ x, f x = f (-x)) (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) (a b : ℝ) :
+  IntervalIntegrable f volume a b :=
   -- Split integral and apply lemma
-  fun x y ↦ (intervalIntegrable_of_even₀ h₁f h₂f x).symm.trans (b := 0)
-    (intervalIntegrable_of_even₀ h₁f h₂f y)
+  (intervalIntegrable_of_even₀ h₁f h₂f a).symm.trans (b := 0)
+    (intervalIntegrable_of_even₀ h₁f h₂f b)
 
 /-- An odd function is interval integrable (with respect to the volume measure) on every interval
 of the form `0..x` if it is interval integrable (with respect to the volume measure) on every
 interval of the form `0..x`, for positive `x`.
 
 See `intervalIntegrable_of_odd` for a stronger result.-/
 lemma intervalIntegrable_of_odd₀
-  (h₁f : ∀ x, -f x = f (-x))
-  (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x)
-  (t : ℝ) :
+  (h₁f : ∀ x, -f x = f (-x)) (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) (t : ℝ) :
   IntervalIntegrable f volume 0 t := by
   rcases lt_trichotomy t 0 with h | h | h
   · rw [IntervalIntegrable.iff_comp_neg]
@@ -428,12 +425,10 @@ lemma intervalIntegrable_of_odd₀
 iff it is interval integrable (with respect to the volume measure) on every interval of the form
 `0..x`, for positive `x`. -/
 theorem intervalIntegrable_of_odd
-  (h₁f : ∀ x, -f x = f (-x))
-  (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) :
-  ∀ x y, IntervalIntegrable f volume x y :=
+  (h₁f : ∀ x, -f x = f (-x)) (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) (a b : ℝ) :
+  IntervalIntegrable f volume a b :=
   -- Split integral and apply lemma
-  fun x y ↦ (intervalIntegrable_of_odd₀ h₁f h₂f x).symm.trans (b := 0)
-    (intervalIntegrable_of_odd₀ h₁f h₂f y)
+  (intervalIntegrable_of_odd₀ h₁f h₂f a).symm.trans (b := 0) (intervalIntegrable_of_odd₀ h₁f h₂f b)
 
 end