-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem fderiv_norm_smul :
    fderiv ℝ (‖·‖) (t • x) = (SignType.sign t : ℝ) • (fderiv ℝ (‖·‖) x)

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
hE : Nontrivial E
hd : ¬DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ fderiv ℝ (fun x => ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x => ‖x‖) x

Tactic:
rw [fderiv_zero_of_not_differentiableAt hd, fderiv_zero_of_not_differentiableAt]

Result:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
hE : Nontrivial E
hd : ¬DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ 0 = ↑(SignType.sign t) • 0

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
hE : Nontrivial E
hd : ¬DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ ¬DifferentiableAt ℝ (fun x => ‖x‖) (t • x)

Proof state:
case pos.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
hE : Nontrivial E
hd : DifferentiableAt ℝ (fun x => ‖x‖) x
ht : t ≠ 0
⊢ fderiv ℝ (fun x => ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x => ‖x‖) x

Tactic:
rw [(hd.hasFDerivAt.hasFDerivAt_norm_smul ht).fderiv]

Result:
no goals

Proof state:
case pos.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hE : Nontrivial E
hd : DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ fderiv ℝ (fun x => ‖x‖) 0 = 0

Tactic:
exact fderiv_zero_of_not_differentiableAt <| not_differentiableAt_norm_zero E

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
hE : Nontrivial E
hd : ¬DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ ¬DifferentiableAt ℝ (fun x => ‖x‖) (t • x)

Tactic:
exact mt DifferentiableAt.differentiableAt_norm_of_smul hd

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
hE : Subsingleton E
⊢ fderiv ℝ (fun x => ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x => ‖x‖) x

Tactic:
simp_rw [(hasFDerivAt_of_subsingleton _ _).fderiv, smul_zero]

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
hE : ¬Nontrivial E
⊢ fderiv ℝ (fun x => ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x => ‖x‖) x

Tactic:
rw [not_nontrivial_iff_subsingleton] at hE

Result:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
hE : Subsingleton E
⊢ fderiv ℝ (fun x => ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x => ‖x‖) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
⊢ fderiv ℝ (fun x => ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x => ‖x‖) x

Tactic:
by_cases hE : Nontrivial E

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
hE : Nontrivial E
⊢ fderiv ℝ (fun x => ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x => ‖x‖) x

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
hE : ¬Nontrivial E
⊢ fderiv ℝ (fun x => ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x => ‖x‖) x

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
hE : Nontrivial E
hd : ¬DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ 0 = ↑(SignType.sign t) • 0

Tactic:
simp

Result:
no goals

Proof state:
case pos.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hE : Nontrivial E
hd : DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ fderiv ℝ (fun x => ‖x‖) (0 • x) = ↑(SignType.sign 0) • fderiv ℝ (fun x => ‖x‖) x

Tactic:
simp only [zero_smul, _root_.sign_zero, SignType.coe_zero]

Result:
case pos.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hE : Nontrivial E
hd : DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ fderiv ℝ (fun x => ‖x‖) 0 = 0

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
hE : Nontrivial E
hd : DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ fderiv ℝ (fun x => ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x => ‖x‖) x

Tactic:
obtain rfl | ht := eq_or_ne t 0

Result:
case pos.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hE : Nontrivial E
hd : DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ fderiv ℝ (fun x => ‖x‖) (0 • x) = ↑(SignType.sign 0) • fderiv ℝ (fun x => ‖x‖) x

case pos.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
hE : Nontrivial E
hd : DifferentiableAt ℝ (fun x => ‖x‖) x
ht : t ≠ 0
⊢ fderiv ℝ (fun x => ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x => ‖x‖) x