have this R v : deriv (deriv (fun v => h R v * f v)) v = h'' R v * f v + 2 * h' R v * f' v + h R v * f'' v := by
  have df v : HasDerivAt f (f' v) v := f.hasDerivAt v
  have df' v : HasDerivAt f' (f'' v) v := f'.hasDerivAt v
  have l3 v : HasDerivAt (fun v => h R v * f v) (h' R v * f v + h R v * f' v) v :=
    (dh R v).ofReal_comp.mul (df v)
  have l5 : HasDerivAt (fun v => h' R v * f v) (h'' R v * f v + h' R v * f' v) v :=
    (dh' R v).ofReal_comp.mul (df v)
  have l7 : HasDerivAt (fun v => h R v * f' v) (h' R v * f' v + h R v * f'' v) v :=
    (dh R v).ofReal_comp.mul (df' v)
  have d1 : deriv (fun v => h R v * f v) = fun v => h' R v * f v + h R v * f' v :=
    funext (fun v => (l3 v).deriv)
  rw [d1] ; convert (l5.add l7).deriv using 1 ; ring
case h.e'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W21
g : trunc
f' : W1 1 ℂ := W1.deriv f
f'' : W1 0 ℂ := f'.deriv
g' : CS 1 ℝ := g.deriv
g'' : CS 0 ℝ := g'.deriv
h : ℝ → ℝ → ℝ := fun R v => 1 - (g.scale R).toFun v
h' : ℝ → CS 1 ℝ := fun R => -(g.scale R).deriv
h'' : ℝ → CS 0 ℝ := fun R => -(g.scale R).deriv.deriv
ch : ∀ {R : ℝ}, Continuous fun v => ↑(h R v)
ch' : ∀ {R : ℝ}, Continuous fun v => ↑((h' R).toFun v)
ch'' : ∀ {R : ℝ}, Continuous fun v => ↑((h'' R).toFun v)
dh : ∀ (R v : ℝ), HasDerivAt (h R) ((h' R).toFun v) v
dh' : ∀ (R v : ℝ), HasDerivAt (h' R).toFun ((h'' R).toFun v) v
hh1 : ∀ (R v : ℝ), |h R v| ≤ 1
vR : ∀ (v : ℝ), Tendsto (fun R => v * R⁻¹) atTop (𝓝 0)
F : ℝ → ℝ → ℝ :=
  fun R v => ‖↑((h'' R).toFun v) * f.toFun v + 2 * ↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v‖
⊢ (fun k => ∫ (v : ℝ), ‖deriv (deriv fun v => ↑(h k v) * f.toFun v) v‖) = fun R => ∫ (v : ℝ), F R v
case h.e'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W21
g : trunc
f' : W1 1 ℂ := W1.deriv f
f'' : W1 0 ℂ := f'.deriv
g' : CS 1 ℝ := g.deriv
g'' : CS 0 ℝ := g'.deriv
h : ℝ → ℝ → ℝ := fun R v => 1 - (g.scale R).toFun v
h' : ℝ → CS 1 ℝ := fun R => -(g.scale R).deriv
h'' : ℝ → CS 0 ℝ := fun R => -(g.scale R).deriv.deriv
ch : ∀ {R : ℝ}, Continuous fun v => ↑(h R v)
ch' : ∀ {R : ℝ}, Continuous fun v => ↑((h' R).toFun v)
ch'' : ∀ {R : ℝ}, Continuous fun v => ↑((h'' R).toFun v)
dh : ∀ (R v : ℝ), HasDerivAt (h R) ((h' R).toFun v) v
dh' : ∀ (R v : ℝ), HasDerivAt (h' R).toFun ((h'' R).toFun v) v
hh1 : ∀ (R v : ℝ), |h R v| ≤ 1
vR : ∀ (v : ℝ), Tendsto (fun R => v * R⁻¹) atTop (𝓝 0)
F : ℝ → ℝ → ℝ :=
  fun R v => ‖↑((h'' R).toFun v) * f.toFun v + 2 * ↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v‖
this :
  ∀ (R v : ℝ),
    deriv (deriv fun v => ↑(h R v) * f.toFun v) v =
      ↑((h'' R).toFun v) * f.toFun v + 2 * ↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v
⊢ (fun k => ∫ (v : ℝ), ‖deriv (deriv fun v => ↑(h k v) * f.toFun v) v‖) = fun R => ∫ (v : ℝ), F R v