-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem HasStrictFDerivAt.hasStrictFDerivAt_norm_smul
    (ht : t ≠ 0) (h : HasStrictFDerivAt (‖·‖) f x) :
    HasStrictFDerivAt (‖·‖) ((SignType.sign t : ℝ) • f) (t • x)

Proof state:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y => |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
⊢ ↑(SignType.sign t) • f = (|t| • f).comp (t⁻¹ • ContinuousLinearMap.id ℝ E)

Tactic:
ext y

Result:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y => |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
y : E
⊢ (↑(SignType.sign t) • f) y = ((|t| • f).comp (t⁻¹ • ContinuousLinearMap.id ℝ E)) y

Proof state:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y => |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
y : E
⊢ ↑(SignType.sign t) * f y = t⁻¹ * (|t| * f y)

Tactic:
rw [eq_inv_mul_iff_mul_eq₀ ht, ← mul_assoc, self_mul_sign]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y => |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
⊢ HasStrictFDerivAt (fun x => ‖x‖) (↑(SignType.sign t) • f) (t • x)

Tactic:
convert h2.comp (t • x) h1 with y

Result:
case h.e'_11.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y => |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
y : E
⊢ ‖y‖ = |t| * ‖t⁻¹ • y‖

case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y => |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
⊢ ↑(SignType.sign t) • f = (|t| • f).comp (t⁻¹ • ContinuousLinearMap.id ℝ E)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
⊢ HasStrictFDerivAt (fun x => ‖x‖) (↑(SignType.sign t) • f) (t • x)

Tactic:
have h1 : HasStrictFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x) :=
  hasStrictFDerivAt_id (t • x) |>.const_smul t⁻¹

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
⊢ HasStrictFDerivAt (fun x => ‖x‖) (↑(SignType.sign t) • f) (t • x)

Proof state:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y => |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
y : E
⊢ (↑(SignType.sign t) • f) y = ((|t| • f).comp (t⁻¹ • ContinuousLinearMap.id ℝ E)) y

Tactic:
simp only [coe_smul', Pi.smul_apply, smul_eq_mul, comp_smulₛₗ, map_inv₀, RingHom.id_apply,
  comp_id]

Result:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y => |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
y : E
⊢ ↑(SignType.sign t) * f y = t⁻¹ * (|t| * f y)

Proof state:
case h.e'_11.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y => |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
y : E
⊢ ‖y‖ = |t| * ‖t⁻¹ • y‖

Tactic:
rw [norm_smul, ← mul_assoc, norm_eq_abs, ← abs_mul, mul_inv_cancel₀ ht, abs_one, one_mul]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
⊢ HasStrictFDerivAt (fun x => ‖x‖) (↑(SignType.sign t) • f) (t • x)

Tactic:
have h2 : HasStrictFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) x := h.const_smul |t|

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y => |t| * ‖y‖) (|t| • f) x
⊢ HasStrictFDerivAt (fun x => ‖x‖) (↑(SignType.sign t) • f) (t • x)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y => |t| * ‖y‖) (|t| • f) x
⊢ HasStrictFDerivAt (fun x => ‖x‖) (↑(SignType.sign t) • f) (t • x)

Tactic:
conv at h2 => enter [3]; rw [← one_smul ℝ x, ← inv_mul_cancel₀ ht, mul_smul]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
h1 : HasStrictFDerivAt (fun y => t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y => |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
⊢ HasStrictFDerivAt (fun x => ‖x‖) (↑(SignType.sign t) • f) (t • x)