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
inst_2 : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
this : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ |t| * ‖x‖) 0
aux : Eq (α := (a : ℝ) → ℝ) abs fun (t : ℝ) ↦ 1 / ‖x‖ * (|t| * ‖x‖)
rw : DifferentiableAt ℝ (F := ℝ) (fun (x_1 : ℝ) ↦ (fun (t : ℝ) ↦ 1 / ‖x‖ * (|t| * ‖x‖)) x_1) 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ |x|) 0

Tactic:
rw [aux]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
this : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ |t| * ‖x‖) 0
aux : Eq (α := (a : ℝ) → ℝ) abs fun (t : ℝ) ↦ 1 / ‖x‖ * (|t| * ‖x‖)
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x_1 : ℝ) ↦ (fun (t : ℝ) ↦ 1 / ‖x‖ * (|t| * ‖x‖)) x_1) 0

Tactic:
this.const_mul _

Premises used: DifferentiableAt.const_mul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
this : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ |t| * ‖x‖) 0
aux : Eq (α := (a : ℝ) → ℝ) abs fun (t : ℝ) ↦ 1 / ‖x‖ * (|t| * ‖x‖)
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x_1 : ℝ) ↦ (fun (t : ℝ) ↦ 1 / ‖x‖ * (|t| * ‖x‖)) x_1) 0

Tactic:
exact this.const_mul _

Premises used: DifferentiableAt.const_mul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
this : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ ‖t • x‖) 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ |x|) 0

Tactic:
have : DifferentiableAt ℝ (|·|) (0 : ℝ) := by
    simp_rw [norm_smul, norm_eq_abs] at this
    have aux : abs = fun t ↦ (1 / ‖x‖) * (|t| * ‖x‖) := by field_simp
    rw [aux]
    exact this.const_mul _
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
this_1 : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ ‖t • x‖) 0
this : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ |x|) 0
⊢ False

Tactic:
not_differentiableAt_abs_zero this

Premises used: not_differentiableAt_abs_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
this_1 : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ ‖t • x‖) 0
this : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ |x|) 0
⊢ False

Tactic:
exact not_differentiableAt_abs_zero this

Premises used: not_differentiableAt_abs_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
⊢ ContDiffAt ℝ (F := E) n (fun (y : E) ↦ t⁻¹ • y) (t • x)

Tactic:
have h1 : ContDiffAt ℝ n (fun y ↦ t⁻¹ • y) (t • x) := (contDiff_const_smul t⁻¹).contDiffAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
h1 : ContDiffAt ℝ (F := E) n (fun (y : E) ↦ t⁻¹ • y) (t • x)
⊢ ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ |t| * ‖y‖) x

Tactic:
have h2 : ContDiffAt ℝ n (fun y ↦ |t| * ‖y‖) x := h.const_smul |t|
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
h1 : ContDiffAt ℝ (F := E) n (fun (y : E) ↦ t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ |t| * ‖y‖) x
enter : x
| ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ |t| * ‖y‖) x

Tactic:
enter [4]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
h1 : ContDiffAt ℝ (F := E) n (fun (y : E) ↦ t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ |t| * ‖y‖) 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
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
h1 : ContDiffAt ℝ (F := E) n (fun (y : E) ↦ t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ |t| * ‖y‖) x
enter : t⁻¹ • t • x
| ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ |t| * ‖y‖) x

Tactic:
enter [4]; 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
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
h1 : ContDiffAt ℝ (F := E) n (fun (y : E) ↦ t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ |t| * ‖y‖) x
⊢ ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ |t| * ‖y‖) (t⁻¹ • t • x)

Tactic:
conv at h2 => enter [4]; 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
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
h1 : ContDiffAt ℝ (F := E) n (fun (y : E) ↦ t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ |t| * ‖y‖) (t⁻¹ • t • x)
⊢ ContDiffAt ℝ (F := ℝ) n ((fun (y : E) ↦ |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹) (t • x)

Tactic:
h2.comp (t • x) h1

Premises used: HSMul.hSMul, ContDiffAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
h1 : ContDiffAt ℝ (F := E) n (fun (y : E) ↦ t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ |t| * ‖y‖) (t⁻¹ • t • x)
h₁ : Eq (α := E → ℝ) (fun (x : E) ↦ ‖x‖) ((fun (y : E) ↦ |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹)
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (t • x)

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

Premises used: HSMul.hSMul, ContDiffAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
h1 : ContDiffAt ℝ (F := E) n (fun (y : E) ↦ t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ |t| * ‖y‖) (t⁻¹ • t • x)
h₁ : ∀ (y : E), ‖y‖ = ((fun (y : E) ↦ |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹) y
⊢ Eq (α := E → ℝ) (fun (x : E) ↦ ‖x‖) ((fun (y : E) ↦ |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹)

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
h1 : ContDiffAt ℝ (F := E) n (fun (y : E) ↦ t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ |t| * ‖y‖) (t⁻¹ • t • x)
y : E
h₁ : ‖y‖ = |t| * (‖t⁻¹‖ * ‖y‖)
h₂ : ‖y‖ = |t| * ‖t⁻¹‖ * ‖y‖
h₃ : ‖y‖ = |t| * |t⁻¹| * ‖y‖
h₄ : ‖y‖ = |t * t⁻¹| * ‖y‖
h₅ : ‖y‖ = |1| * ‖y‖
h₆ : ‖y‖ = 1 * ‖y‖
h₇ h₈ : ‖y‖ = ‖y‖
⊢ ‖y‖ = |t| * ‖t⁻¹ • y‖

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
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
hd : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (t • x)
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (t⁻¹ • t • x)

Tactic:
hd.contDiffAt_norm_smul (inv_ne_zero ht)

Premises used: ContDiffAt.contDiffAt_norm_smul, inv_ne_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
hd : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (t • x)
h : x = t⁻¹ • t • x
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x

Tactic:
convert! hd.contDiffAt_norm_smul (inv_ne_zero ht)

Premises used: ContDiffAt.contDiffAt_norm_smul, inv_ne_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
hd : ContDiffAt ℝ (F := ℝ) n (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
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (t • x)
inl : ∀ (h : ContDiffAt ℝ (F := ℝ) 0 (fun (x : E) ↦ ‖x‖) (t • x)), ContDiffAt ℝ (F := ℝ) 0 (fun (x : E) ↦ ‖x‖) x
inr : ∀ (hn : n ≠ 0), ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x

Tactic:
rcases eq_or_ne n 0 with rfl | hn

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
t : ℝ
h : ContDiffAt ℝ (F := ℝ) 0 (fun (x : E) ↦ ‖x‖) (t • x)
inl : ∃ u ∈ nhds x, ContinuousOn (Y := ℝ) (fun (x : E) ↦ ‖x‖) u
⊢ ContDiffAt ℝ (F := ℝ) 0 (fun (x : E) ↦ ‖x‖) x

Tactic:
apply contDiffAt_zero.2

Premises used: Iff.mpr, contDiffAt_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : ContDiffAt ℝ (F := ℝ) 0 (fun (x : E) ↦ ‖x‖) (t • x)
⊢ ∃ u ∈ nhds x, ContinuousOn (Y := ℝ) (fun (x : E) ↦ ‖x‖) u

Tactic:
⟨univ, univ_mem, continuous_norm.continuousOn⟩

Premises used: Continuous.continuousOn, Set.univ, And.intro, Exists.intro, Filter.univ_mem, continuous_norm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : ContDiffAt ℝ (F := ℝ) 0 (fun (x : E) ↦ ‖x‖) (t • x)
⊢ ∃ u ∈ nhds x, ContinuousOn (Y := ℝ) (fun (x : E) ↦ ‖x‖) u

Tactic:
exact ⟨univ, univ_mem, continuous_norm.continuousOn⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (t • x)
hn : n ≠ 0
inr :
  ∀ (h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x)),
    ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
inr₁ : ∀ (ht : t ≠ 0), ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
⊢ ContDiffAt ℝ (F := ℝ) n (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
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x)
this : Subsingleton E
rw : ContDiffAt ℝ n (Function.const E (Norm.norm.{u_1} (E := E) 0)) x
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x

Tactic:
rw [eq_const_of_subsingleton (‖·‖) 0]

Premises used: Norm.norm, eq_const_of_subsingleton, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x)
this : Subsingleton E
⊢ ContDiffAt ℝ n (Function.const E (Norm.norm.{u_1} (E := E) 0)) x

Tactic:
contDiffAt_const

Premises used: contDiffAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x)
this : Subsingleton E
⊢ ContDiffAt ℝ n (Function.const E (Norm.norm.{u_1} (E := E) 0)) x

Tactic:
exact contDiffAt_const

Premises used: contDiffAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x)
inr : Subsingleton E
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x

Tactic:
suffices Subsingleton E by
      rw [eq_const_of_subsingleton (‖·‖) 0]
      exact contDiffAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x)
⊢ ContDiffAt ℝ (F := ℝ) n (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
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) 0
inr : ∀ (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
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) 0
this : Nontrivial E
⊢ False

Tactic:
not_differentiableAt_norm_zero E <| h.differentiableAt hn

Premises used: not_differentiableAt_norm_zero, ContDiffAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) 0
this : Nontrivial E
⊢ False

Tactic:
exact not_differentiableAt_norm_zero E <| h.differentiableAt hn

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

Tactic:
contDiffAt_norm_smul_iff ht |>.2 h

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

Tactic:
exact contDiffAt_norm_smul_iff ht |>.2 h

Premises used: Iff.mpr, contDiffAt_norm_smul_iff
-- 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 : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f x
⊢ HasStrictFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)

Tactic:
have h1 : HasStrictFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x) :=
    hasStrictFDerivAt_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 : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
⊢ HasStrictFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x

Tactic:
have h2 : HasStrictFDerivAt (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 : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasStrictFDerivAt (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 : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasStrictFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x
enter : t⁻¹ • t • x
| HasStrictFDerivAt (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 : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasStrictFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x
⊢ HasStrictFDerivAt (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 : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasStrictFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
⊢ HasStrictFDerivAt (fun (x : E) ↦ |t| * ‖t⁻¹ • x‖)
    ((|t| • f) ∘SL HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)

Tactic:
h2.comp (t • x) h1

Premises used: HSMul.hSMul, HasStrictFDerivAt.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 : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasStrictFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
h₁ : ∀ (x : E), ‖x‖ = |t| * ‖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)
⊢ HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f) (t • x)

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

Premises used: HSMul.hSMul, HasStrictFDerivAt.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 : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasStrictFDerivAt (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 : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasStrictFDerivAt (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 : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasStrictFDerivAt (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 : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun (y : E) ↦ t⁻¹ • y) (HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)) (t • x)
h2 : HasStrictFDerivAt (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 : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f x
⊢ HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f (t • x)

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

Premises used: LT.lt.ne', HasStrictFDerivAt.hasStrictFDerivAt_norm_smul