awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun (x : E) ↦ ‖x‖) f x
⊢ HasFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)

Tactic:
have h1 : HasFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x) :=
    hasFDerivAt_id (t • x) |>.const_smul t⁻¹
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
⊢ HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x

Tactic:
have h2 : HasFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) x := h.const_smul |t|
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x
enter : x
| HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x

Tactic:
enter [3]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x
rw : t⁻¹ • t • x
| x

Tactic:
rw [← one_smul ℝ x, ← inv_mul_cancel₀ ht, mul_smul]

Premises used: Real, one_smul, inv_mul_cancel₀, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x
enter : t⁻¹ • t • x
| HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x

Tactic:
enter [3]; rw [← one_smul ℝ x, ← inv_mul_cancel₀ ht, mul_smul]

Premises used: Real, one_smul, inv_mul_cancel₀, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x
⊢ HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)

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

Premises used: Real, one_smul, inv_mul_cancel₀, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
⊢ HasFDerivAt ((fun (y : E) ↦ |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹)
    ((|t| • f) ∘SL HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)

Tactic:
h2.comp (t • x) h1

Premises used: HSMul.hSMul, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
h₁ : ∀ (x : E), ‖x‖ = ((fun (y : E) ↦ |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹) x
h₂ :
  instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
      HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f =
        (|t| • f) ∘SL HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)
⊢ HasFDerivAt (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f) (t • x)

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

Premises used: HSMul.hSMul, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
x_1 : E
h₁ : ‖x_1‖ = |t| * (‖t⁻¹‖ * ‖x_1‖)
h₂ : ‖x_1‖ = |t| * ‖t⁻¹‖ * ‖x_1‖
h₃ : ‖x_1‖ = |t| * |t⁻¹| * ‖x_1‖
h₄ : ‖x_1‖ = |t * t⁻¹| * ‖x_1‖
h₅ : ‖x_1‖ = |1| * ‖x_1‖
h₆ : ‖x_1‖ = 1 * ‖x_1‖
h₇ h₈ : ‖x_1‖ = ‖x_1‖
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖

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

Premises used: norm_smul, mul_inv_cancel₀, mul_assoc, abs_mul, abs_one, one_mul, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
h₁ :
  ∀ (y : E),
    Eq (α := ℝ) ((HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f : (a : E) → ℝ) y : ℝ)
      (((|t| • f) ∘SL HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E) : (a : E) → ℝ) y : ℝ)
⊢ HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f =
    (|t| • f) ∘SL HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
y : E
h₁ :
  HMul.hMul (α := ℝ) (β := ℝ) ((↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) : ℝ) ((f : (a : E) → ℝ) y : ℝ) =
    t⁻¹ * HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ)
⊢ Eq (α := ℝ) ((HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f : (a : E) → ℝ) y : ℝ)
    (((|t| • f) ∘SL HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E) : (a : E) → ℝ) y : ℝ)

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

Premises used: ContinuousLinearMap.coe_smul', RingHom.id_apply, map_inv₀, ContinuousLinearMap.comp_smulₛₗ, smul_eq_mul, ContinuousLinearMap.comp_id, Pi.smul_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
y : E
h₁ :
  t * HMul.hMul (α := ℝ) (β := ℝ) ((↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) : ℝ) ((f : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ)
h₂ :
  HMul.hMul (β := ℝ) (t * (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)) ((f : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ)
h₃ h₄ : HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ) = HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) : ℝ) ((f : (a : E) → ℝ) y : ℝ) =
    t⁻¹ * HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ)

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

Premises used: mul_assoc, eq_inv_mul_iff_mul_eq₀, self_mul_sign
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : 0 < t
h : HasFDerivAt (fun (x : E) ↦ ‖x‖) f x
⊢ HasFDerivAt (fun (x : E) ↦ ‖x‖) f (t • x)

Tactic:
simpa [ht] using h.hasFDerivAt_norm_smul ht.ne'

Premises used: LT.lt.ne', HasFDerivAt.hasFDerivAt_norm_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
ht : t ≠ 0
hd : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (t • x)
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (t⁻¹ • t • x)

Tactic:
(hd.hasFDerivAt.hasFDerivAt_norm_smul (inv_ne_zero ht)).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.hasFDerivAt_norm_smul, HasFDerivAt.differentiableAt, inv_ne_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
ht : t ≠ 0
hd : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (t • x)
h : x = t⁻¹ • t • x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x

Tactic:
convert! (hd.hasFDerivAt.hasFDerivAt_norm_smul (inv_ne_zero ht)).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.hasFDerivAt_norm_smul, HasFDerivAt.differentiableAt, inv_ne_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
ht : t ≠ 0
hd : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (t • x)
h : x = (t⁻¹ * t) • x
h₁ : x = HSMul.hSMul (α := ℝ) 1 x
h₂ h₃ : x = x
⊢ x = t⁻¹ • t • x

Tactic:
rw [smul_smul, inv_mul_cancel₀ ht, one_smul]

Premises used: smul_smul, one_smul, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (t • x)
inl :
  ∀ (h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x)),
    DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
inr : ∀ (ht : t ≠ 0), DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x

Tactic:
obtain rfl | ht := eq_or_ne t 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x)
inl : Subsingleton E
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x

Tactic:
suffices Subsingleton E from (hasFDerivAt_of_subsingleton _ _).differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x)
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0

Tactic:
rw [zero_smul] at h

Premises used: zero_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
inl : ∀ (this : Nontrivial E), False
⊢ Subsingleton E

Tactic:
by_contra!
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
this : Nontrivial E
⊢ False

Tactic:
not_differentiableAt_norm_zero E h

Premises used: not_differentiableAt_norm_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
this : Nontrivial E
⊢ False

Tactic:
exact not_differentiableAt_norm_zero E h

Premises used: not_differentiableAt_norm_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (t • x)
ht : t ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x

Tactic:
differentiableAt_norm_smul ht |>.2 h

Premises used: Iff.mpr, differentiableAt_norm_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (t • x)
ht : t ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x

Tactic:
exact differentiableAt_norm_smul ht |>.2 h

Premises used: Iff.mpr, differentiableAt_norm_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
rw : deriv (fun (t : ℝ) ↦ ‖x + t • x‖) 0 = ‖x‖
⊢ (fderiv ℝ (fun (x : E) ↦ ‖x‖) x : (a : E) → ℝ) x = ‖x‖

Tactic:
rw [← h.lineDeriv_eq_fderiv, lineDeriv]

Premises used: lineDeriv, DifferentiableAt.lineDeriv_eq_fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
t : ℝ
rw : ‖x + t • x‖ = ‖1 + t‖ * ‖x‖
rw₁ : ‖x + t • x‖ = ‖(1 + t) • x‖
rw₂ : ‖x + t • x‖ = ‖HSMul.hSMul (α := ℝ) 1 x + t • x‖
rw₃ rw₄ : ‖x + t • x‖ = ‖x + t • x‖
⊢ ‖x + t • x‖ = |1 + t| * ‖x‖

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

Premises used: norm_smul, one_smul, add_smul, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
⊢ ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖

Tactic:
have this (t : ℝ) : ‖x + t • x‖ = |1 + t| * ‖x‖ := by
    rw [← norm_eq_abs, ← norm_smul, add_smul, one_smul]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
simp_rw : deriv (fun (t : ℝ) ↦ |1 + t| * ‖x‖) 0 = ‖x‖
⊢ deriv (fun (t : ℝ) ↦ ‖x + t • x‖) 0 = ‖x‖

Tactic:
simp_rw [this]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
rw : deriv (fun (t : ℝ) ↦ |1 + t|) 0 * ‖x‖ = ‖x‖
hc : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ |1 + t|) 0
⊢ deriv (fun (t : ℝ) ↦ |1 + t| * ‖x‖) 0 = ‖x‖

Tactic:
rw [deriv_mul_const]

Premises used: deriv_mul_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
enter : fun (t : ℝ) ↦ |1 + t|
| deriv (fun (t : ℝ) ↦ |1 + t|) 0 * ‖x‖

Tactic:
enter [1, 1]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
enter : _root_.abs ∘ fun (t : ℝ) ↦ 1 + t
| deriv (fun (t : ℝ) ↦ |1 + t|) 0 * ‖x‖

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

Premises used: abs, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
rw : HMul.hMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) 1 0)) : ℝ) 1 * ‖x‖ = ‖x‖
hh₂ : DifferentiableAt ℝ _root_.abs (HAdd.hAdd (α := ℝ) 1 0)
hh : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ 1 + t) 0
⊢ deriv (𝕜 := ℝ) (_root_.abs ∘ fun (t : ℝ) ↦ 1 + t) 0 * ‖x‖ = ‖x‖

Tactic:
rw [deriv_comp, deriv_abs, deriv_const_add_id]

Premises used: deriv_abs, deriv_const_add_id, deriv_comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ HMul.hMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) 1 0)) : ℝ) 1 * ‖x‖ = ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ HAdd.hAdd (α := ℝ) 1 0 ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ _root_.abs (HAdd.hAdd (α := ℝ) 1 0)

Tactic:
exact differentiableAt_abs (by simp)

Premises used: differentiableAt_abs
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ 1 + t) 0

Tactic:
differentiableAt_id.const_add _

Premises used: DifferentiableAt.const_add, differentiableAt_id
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ 1 + t) 0

Tactic:
exact differentiableAt_id.const_add _

Premises used: DifferentiableAt.const_add, differentiableAt_id
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ |1 + t|) 0

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

Premises used: DifferentiableAt.const_add, DifferentiableAt.comp, differentiableAt_abs, differentiableAt_id
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
inl :
  Subsingleton E →
    fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
      HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
        (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
inr :
  Nontrivial E →
    fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
      HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
        (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)

Tactic:
cases subsingleton_or_nontrivial E

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : Subsingleton E
inl : 0 = HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) 0
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)

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

Premises used: hasFDerivAt_of_subsingleton, smul_zero, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : Nontrivial E
pos :
  ∀ (hd : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x),
    fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
      HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
        (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
neg :
  ∀ (hd : ¬DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x),
    fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
      HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
        (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)

Tactic:
by_cases hd : DifferentiableAt ℝ (‖·‖) x

Premises used: Norm.norm, Real, DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : Nontrivial E
hd : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
pos :
  fderiv ℝ (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
pos₁ :
  ∀ (ht : t ≠ 0),
    fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
      HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
        (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)

Tactic:
obtain rfl | ht := eq_or_ne t 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Nontrivial E
hd : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
pos : Eq.{u_1 + 1} (α := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) 0) 0
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)

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

Premises used: SignType.coe_zero, sign_zero, zero_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Nontrivial E
hd : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
⊢ Eq.{u_1 + 1} (α := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) 0) 0

Tactic:
fderiv_zero_of_not_differentiableAt <| not_differentiableAt_norm_zero E

Premises used: not_differentiableAt_norm_zero, fderiv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Nontrivial E
hd : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
⊢ Eq.{u_1 + 1} (α := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) 0) 0

Tactic:
exact fderiv_zero_of_not_differentiableAt <| not_differentiableAt_norm_zero E

Premises used: not_differentiableAt_norm_zero, fderiv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : Nontrivial E
hd : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
ht : t ≠ 0
pos pos₁ :
  HSMul.hSMul (α := ℝ) (β := StrongDual ℝ E) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)

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

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.hasFDerivAt_norm_smul, HasFDerivAt.fderiv