-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem not_differentiableAt_norm_zero [Nontrivial E] :
    ¬DifferentiableAt ℝ (‖·‖) (0 : E)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
this : DifferentiableAt ℝ (fun t => |t| * ‖x‖) 0
aux : abs = fun t => 1 / ‖x‖ * (|t| * ‖x‖)
⊢ DifferentiableAt ℝ (fun x_1 => (fun t => 1 / ‖x‖ * (|t| * ‖x‖)) x_1) 0

Tactic:
exact this.const_mul _

Result:
no goals

Proof state:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
this✝ : DifferentiableAt ℝ (fun t => ‖t • x‖) 0
this : DifferentiableAt ℝ (fun x => |x|) 0
⊢ False

Tactic:
exact not_differentiableAt_abs_zero this

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
⊢ DifferentiableAt ℝ Norm.norm (0 • x)

Tactic:
simpa

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
this : DifferentiableAt ℝ (fun t => |t| * ‖x‖) 0
⊢ abs = fun t => 1 / ‖x‖ * (|t| * ‖x‖)

Tactic:
field_simp

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
⊢ ¬DifferentiableAt ℝ (fun x => ‖x‖) 0

Tactic:
obtain ⟨x, hx⟩ := NormedSpace.exists_lt_norm ℝ E 0

Result:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
⊢ ¬DifferentiableAt ℝ (fun x => ‖x‖) 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
this : DifferentiableAt ℝ (fun t => ‖t • x‖) 0
⊢ DifferentiableAt ℝ (fun x => |x|) 0

Tactic:
simp_rw [norm_smul, norm_eq_abs] at this

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
this : DifferentiableAt ℝ (fun t => |t| * ‖x‖) 0
⊢ DifferentiableAt ℝ (fun x => |x|) 0

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

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
this : DifferentiableAt ℝ (fun t => |t| * ‖x‖) 0
aux : abs = fun t => 1 / ‖x‖ * (|t| * ‖x‖)
⊢ DifferentiableAt ℝ (fun x => |x|) 0

Tactic:
rw [aux]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
this : DifferentiableAt ℝ (fun t => |t| * ‖x‖) 0
aux : abs = fun t => 1 / ‖x‖ * (|t| * ‖x‖)
⊢ DifferentiableAt ℝ (fun x_1 => (fun t => 1 / ‖x‖ * (|t| * ‖x‖)) x_1) 0

Proof state:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
⊢ ¬DifferentiableAt ℝ (fun x => ‖x‖) 0

Tactic:
intro h

Result:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
⊢ False

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
this : DifferentiableAt ℝ (fun t => |t| * ‖x‖) 0
⊢ DifferentiableAt ℝ (fun x => |x|) 0

Tactic:
have aux : abs = fun t ↦ (1 / ‖x‖) * (|t| * ‖x‖) := by field_simp

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
this : DifferentiableAt ℝ (fun t => |t| * ‖x‖) 0
aux : abs = fun t => 1 / ‖x‖ * (|t| * ‖x‖)
⊢ DifferentiableAt ℝ (fun x => |x|) 0

Proof state:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
⊢ False

Tactic:
have : DifferentiableAt ℝ (fun t : ℝ ↦ ‖t • x‖) 0 := DifferentiableAt.comp _ (by simpa) (by simp)

Result:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
this : DifferentiableAt ℝ (fun t => ‖t • x‖) 0
⊢ False