exact fun x hx ↦ (hu x <| mem_Icc_of_Ioo hx).mul (hv x <| mem_Icc_of_Ioo hx) |>.hasDerivAt
  (Icc_mem_nhds hx.1 hx.2) |>.hasDerivWithinAt
case hderiv
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
h2u : ContinuousOn u [[a, b]]
h2v : ContinuousOn v [[a, b]]
⊢ ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt (fun x => u x * v x) (u' x * v x + u x * v' x) (Ioi x) x
no goals