chore: fix duplicated lemma (leanprover-community#40870)

Reported on Zulip at [#mathlib4 > Redundant copy of &leanprover-community#96;intervalIntegrable_const&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Redundant.20copy.20of.20.60intervalIntegrable_const.60/near/605394633)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean

@@ -187,9 +187,6 @@ theorem integrableOn_Ioo_cpow_iff {s : ℂ} {t : ℝ} (ht : 0 < t) :
 theorem intervalIntegrable_id : IntervalIntegrable (fun x => x) μ a b :=
   continuous_id.intervalIntegrable a b
 
-theorem intervalIntegrable_const : IntervalIntegrable (fun _ => c) μ a b :=
-  continuous_const.intervalIntegrable a b
-
 theorem intervalIntegrable_one_div (h : ∀ x : ℝ, x ∈ [[a, b]] → f x ≠ 0)
     (hf : ContinuousOn f [[a, b]]) : IntervalIntegrable (fun x => 1 / f x) μ a b :=
   (continuousOn_const.div hf h).intervalIntegrable

Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean

@@ -171,10 +171,9 @@ theorem intervalIntegrable_const_iff {c : ε} (hc : ‖c‖ₑ ≠ ⊤ := by fin
   simp [intervalIntegrable_iff, integrableOn_const_iff hc]
 
 @[simp]
-theorem intervalIntegrable_const [IsLocallyFiniteMeasure μ]
-    {c : E} (hc : ‖c‖ₑ ≠ ⊤ := by finiteness) :
+theorem intervalIntegrable_const [IsLocallyFiniteMeasure μ] {c : E} :
     IntervalIntegrable (fun _ => c) μ a b :=
-  intervalIntegrable_const_iff hc |>.2 <| Or.inr measure_Ioc_lt_top
+  intervalIntegrable_const_iff (by simp) |>.2 <| Or.inr measure_Ioc_lt_top
 
 protected theorem IntervalIntegrable.zero : IntervalIntegrable (0 : ℝ → E) μ a b :=
   (intervalIntegrable_const_iff <| by finiteness).mpr <| .inl rfl