Theorem: CS.hasDerivAt_scale (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 x : ℝ
⊢ HasDerivAt (f.scale R).toFun (R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x)) x
Tactic:
convert hasDerivAt (f.scale R) x
State after:
case h.e'_7
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS (n + 1) E
R x : ℝ
⊢ R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x) = (f.scale R).deriv.toFun x

State before:
case h.e'_7
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS (n + 1) E
R x : ℝ
⊢ R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x) = (f.scale R).deriv.toFun x
Tactic:
rw [deriv_scale']
State after:
case h.e'_7
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS (n + 1) E
R x : ℝ
⊢ R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x) = R⁻¹ • f.deriv.toFun (R⁻¹ • x)

State before:
case h.e'_7
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS (n + 1) E
R x : ℝ
⊢ R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x) = R⁻¹ • f.deriv.toFun (R⁻¹ • x)
Tactic:
rfl
State after:
no goals