-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem DifferentiableAt.fderiv_norm_self {x : E} (h : DifferentiableAt ℝ (‖·‖) x) :
    fderiv ℝ (‖·‖) x x = ‖x‖

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (fun t => ‖x + t • x‖) 0 = ‖x‖

Tactic:
simp_rw [this]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (fun t => |1 + t| * ‖x‖) 0 = ‖x‖

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ ↑(SignType.sign (1 + 0)) * deriv (fun t => t) 0 * ‖x‖ = ‖x‖

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (fun t => |1 + t|) 0 * ‖x‖ = ‖x‖

Tactic:
conv_lhs => enter [1, 1]; change _root_.abs ∘ (fun t ↦ 1 + t)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (_root_.abs ∘ fun t => 1 + t) 0 * ‖x‖ = ‖x‖

Proof state:
case hh
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t => 1 + t) 0

Tactic:
exact differentiableAt_id.const_add _

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ 1 + 0 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (_root_.abs ∘ fun t => 1 + t) 0 * ‖x‖ = ‖x‖

Tactic:
rw [deriv_comp, deriv_abs, deriv_const_add]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ ↑(SignType.sign (1 + 0)) * deriv (fun t => t) 0 * ‖x‖ = ‖x‖

case hh₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ _root_.abs (1 + 0)

case hh
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t => 1 + t) 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
t : ℝ
⊢ ‖x + t • x‖ = |1 + t| * ‖x‖

Tactic:
rw [← norm_eq_abs, ← norm_smul, add_smul, one_smul]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ (fderiv ℝ (fun x => ‖x‖) x) x = ‖x‖

Tactic:
rw [← h.lineDeriv_eq_fderiv, lineDeriv]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ deriv (fun t => ‖x + t • x‖) 0 = ‖x‖

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (fun t => |1 + t| * ‖x‖) 0 = ‖x‖

Tactic:
rw [deriv_mul_const]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (fun t => |1 + t|) 0 * ‖x‖ = ‖x‖

case hc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t => |1 + t|) 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
⊢ deriv (fun t => ‖x + t • x‖) 0 = ‖x‖

Tactic:
have this (t : ℝ) : ‖x + t • x‖ = |1 + t| * ‖x‖ := by
  rw [← norm_eq_abs, ← norm_smul, add_smul, one_smul]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (fun t => ‖x + t • x‖) 0 = ‖x‖

Proof state:
case hh₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ _root_.abs (1 + 0)

Tactic:
exact differentiableAt_abs (by norm_num)

Result:
no goals

Proof state:
case hc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t => |1 + t|) 0

Tactic:
exact (differentiableAt_abs (by norm_num)).comp _ (differentiableAt_id.const_add _)

Result:
no goals