intervalIntegrable_continuous_mul_lipschitzOnWith

lemma intervalIntegrable_continuous_mul_lipschitzOnWith    {a b : ℝ} {K : ℝ≥0} {f g : ℝ → ℂ} (hab : a ≤ b) (hf : Continuous f)    (hg : LipschitzOnWith K g (Set.Ioo a b)) :    IntervalIntegrable (fun x ↦ f x * g x) volume a b := by  rcases hab.eq_or_lt with rfl | h'ab  · simp  obtain ⟨C, hC⟩ : ∃ C, ∀ x ∈ f '' (Icc a b), ‖x‖ ≤ C :=    IsBounded.exists_norm_le (isCompact_Icc.image_of_continuousOn hf.continuousOn).isBounded  obtain ⟨D, hD⟩ : ∃ D, ∀ x ∈ Ioo a b, ‖g x‖ ≤ D := by    let x₀ := (a + b) / 2    have h₀ : x₀ ∈ Ioo a b := by simp only [x₀]; exact ⟨by linarith, by linarith⟩    refine ⟨‖g x₀‖ + K * ((b - a) / 2), fun y hy ↦ ?_⟩    calc ‖g y‖ = ‖g x₀ + (g y - g x₀)‖ := by congr; abel    _ ≤ ‖g x₀‖ + ‖g y - g x₀‖ := norm_add_le _ _    _ ≤ ‖g x₀‖ + K * ‖y - x₀‖ := by gcongr; apply hg.norm_sub_le hy h₀    _ ≤ ‖g x₀‖ + K * ((b - a) / 2) := by      gcongr      rw [Real.Ioo_eq_ball] at hy      simp only [Metric.mem_ball, dist_eq_norm] at hy      exact hy.le  apply (hf.continuousOn.fun_mul hg.continuousOn).intervalIntegrable_Ioo_of_bound hab    (C := C * D) (fun x hx ↦ ?_)  rw [norm_mul, mul_comm, mul_comm C]  gcongr  · apply (norm_nonneg _).trans (hD x hx)  · apply hD x hx  · apply hC    apply mem_image_of_mem    exact Ioo_subset_Icc_self hx