refactor(MeasureTheory/Function/LocallyIntegrable): golf ContinuousOn.integrableOn_compact'

Author: Deep0Thinking

Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

@@ -505,8 +505,8 @@ variable [IsFiniteMeasureOnCompacts μ]
 locally finite measure. -/
 theorem ContinuousOn.integrableOn_compact'
     (hK : IsCompact K) (h'K : MeasurableSet K) (hf : ContinuousOn f K) :
-    IntegrableOn f K μ := by
-  exact hf.integrableOn_of_subset_isCompact hK h'K Subset.rfl hK.measure_ne_top
+    IntegrableOn f K μ :=
+  hf.integrableOn_of_subset_isCompact hK h'K Subset.rfl hK.measure_ne_top
 
 theorem ContinuousOn.integrableOn_compact [T2Space X]
     (hK : IsCompact K) (hf : ContinuousOn f K) : IntegrableOn f K μ :=