Theorem: CS.deriv_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
⊢ (f.scale R).deriv.toFun v = R⁻¹ • f.deriv.toFun (R⁻¹ • v)
Tactic:
rw [deriv_scale, smul_apply]
State after:
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.scale R).toFun v = R⁻¹ • f.deriv.toFun (R⁻¹ • v)

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.scale R).toFun v = R⁻¹ • f.deriv.toFun (R⁻¹ • v)
Tactic:
by_cases hR : R = 0 <;> simp [hR, scale, funscale]
State after:
no goals