-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem ContDiffAt.contDiffAt_norm_smul (ht : t ≠ 0) (h : ContDiffAt ℝ n (‖·‖) x) :
    ContDiffAt ℝ n (‖·‖) (t • x)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x => ‖x‖) x
h1 : ContDiffAt ℝ n (fun y => t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ n (fun y => |t| * ‖y‖) (t⁻¹ • t • x)
⊢ ContDiffAt ℝ n (fun x => ‖x‖) (t • x)

Tactic:
convert h2.comp (t • x) h1 using 1

Result:
case h.e'_10
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x => ‖x‖) x
h1 : ContDiffAt ℝ n (fun y => t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ n (fun y => |t| * ‖y‖) (t⁻¹ • t • x)
⊢ (fun x => ‖x‖) = (fun y => |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹

Proof state:
case h.e'_10
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x => ‖x‖) x
h1 : ContDiffAt ℝ n (fun y => t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ n (fun y => |t| * ‖y‖) (t⁻¹ • t • x)
⊢ (fun x => ‖x‖) = (fun y => |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹

Tactic:
ext y

Result:
case h.e'_10.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x => ‖x‖) x
h1 : ContDiffAt ℝ n (fun y => t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ n (fun y => |t| * ‖y‖) (t⁻¹ • t • x)
y : E
⊢ ‖y‖ = ((fun y => |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹) y

Proof state:
case h.e'_10.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x => ‖x‖) x
h1 : ContDiffAt ℝ n (fun y => t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ n (fun y => |t| * ‖y‖) (t⁻¹ • t • x)
y : E
⊢ ‖y‖ = ((fun y => |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹) y

Tactic:
simp only [Function.comp_apply]

Result:
case h.e'_10.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x => ‖x‖) x
h1 : ContDiffAt ℝ n (fun y => t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ n (fun y => |t| * ‖y‖) (t⁻¹ • t • x)
y : E
⊢ ‖y‖ = |t| * ‖t⁻¹ • y‖

Proof state:
case h.e'_10.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x => ‖x‖) x
h1 : ContDiffAt ℝ n (fun y => t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ n (fun y => |t| * ‖y‖) (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
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x => ‖x‖) x
h1 : ContDiffAt ℝ n (fun y => t⁻¹ • y) (t • x)
⊢ ContDiffAt ℝ n (fun x => ‖x‖) (t • x)

Tactic:
have h2 : ContDiffAt ℝ n (fun y ↦ |t| * ‖y‖) x := h.const_smul |t|

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x => ‖x‖) x
h1 : ContDiffAt ℝ n (fun y => t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ n (fun y => |t| * ‖y‖) x
⊢ ContDiffAt ℝ n (fun x => ‖x‖) (t • x)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x => ‖x‖) x
⊢ ContDiffAt ℝ n (fun x => ‖x‖) (t • x)

Tactic:
have h1 : ContDiffAt ℝ n (fun y ↦ t⁻¹ • y) (t • x) := (contDiff_const_smul t⁻¹).contDiffAt

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x => ‖x‖) x
h1 : ContDiffAt ℝ n (fun y => t⁻¹ • y) (t • x)
⊢ ContDiffAt ℝ n (fun x => ‖x‖) (t • x)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x => ‖x‖) x
h1 : ContDiffAt ℝ n (fun y => t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ n (fun y => |t| * ‖y‖) x
⊢ ContDiffAt ℝ n (fun x => ‖x‖) (t • x)

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

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x => ‖x‖) x
h1 : ContDiffAt ℝ n (fun y => t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ n (fun y => |t| * ‖y‖) (t⁻¹ • t • x)
⊢ ContDiffAt ℝ n (fun x => ‖x‖) (t • x)