Theorem: CS.deriv_smul (PrimeNumberTheoremAnd/Sobolev.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v : ℝ
f : CS (n + 1) E
⊢ (R • f).deriv = R • f.deriv
Tactic:
ext x
State after:
case toFun.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x✝ v : ℝ
f : CS (n + 1) E
x : ℝ
⊢ (R • f).deriv.toFun x = (R • f.deriv).toFun x

State before:
case toFun.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x✝ v : ℝ
f : CS (n + 1) E
x : ℝ
⊢ (R • f).deriv.toFun x = (R • f.deriv).toFun x
Tactic:
exact (f.hasDerivAt x |>.const_smul R).deriv
State after:
no goals