awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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 : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) : ℝ) ((f : (a : E) → ℝ) y : ℝ) =
    t⁻¹ * HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ)
have h₂ : HMul.hMul (β := ℝ) (t * (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)) ((f : (a : E) → ℝ) y : ℝ) =
  HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ)
Tactic: rw [eq_inv_mul_iff_mul_eq₀ ht, ← mul_assoc, self_mul_sign]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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 : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) : ℝ) ((f : (a : E) → ℝ) y : ℝ) =
    t⁻¹ * HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ)
have h₃ : HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ) = HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ)
Tactic: rw [eq_inv_mul_iff_mul_eq₀ ht, ← mul_assoc, self_mul_sign]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖) x
have h : x = t⁻¹ • t • x
Tactic: convert! (hd.hasFDerivAt.hasFDerivAt_norm_smul (inv_ne_zero ht)).differentiableAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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)
⊢ x = t⁻¹ • t • x
have h : x = (t⁻¹ * t) • x
Tactic: rw [smul_smul, inv_mul_cancel₀ ht, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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
⊢ x = t⁻¹ • t • x
have h₁ : x = HSMul.hSMul (α := ℝ) 1 x
Tactic: rw [smul_smul, inv_mul_cancel₀ ht, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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
⊢ x = t⁻¹ • t • x
have h₂ : x = x
Tactic: rw [smul_smul, inv_mul_cancel₀ ht, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (t • x)
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
have inl : ∀ (h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x)),
  DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
Tactic: obtain rfl | ht := eq_or_ne t 0
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
have inr : ∀ (ht : t ≠ 0), DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
Tactic: obtain rfl | ht := eq_or_ne t 0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖) x
have inl : Subsingleton E
Tactic: suffices Subsingleton E from (hasFDerivAt_of_subsingleton _ _).differentiableAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (hypothesis)
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)
⊢ Subsingleton E
have h₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
Tactic: rw [zero_smul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
⊢ Subsingleton E
have inl : ∀ (this : Nontrivial E), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
⊢ (fderiv ℝ (fun (x : E) ↦ ‖x‖) x : (a : E) → ℝ) x = ‖x‖
have rw : deriv (fun (t : ℝ) ↦ ‖x + t • x‖) 0 = ‖x‖
Tactic: rw [← h.lineDeriv_eq_fderiv, lineDeriv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖
have rw : ‖x + t • x‖ = ‖1 + t‖ * ‖x‖
Tactic: rw [← norm_eq_abs, ← norm_smul, add_smul, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖
⊢ ‖x + t • x‖ = |1 + t| * ‖x‖
have rw₁ : ‖x + t • x‖ = ‖(1 + t) • x‖
Tactic: rw [← norm_eq_abs, ← norm_smul, add_smul, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖
⊢ ‖x + t • x‖ = |1 + t| * ‖x‖
have rw₂ : ‖x + t • x‖ = ‖HSMul.hSMul (α := ℝ) 1 x + t • x‖
Tactic: rw [← norm_eq_abs, ← norm_smul, add_smul, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖
⊢ ‖x + t • x‖ = |1 + t| * ‖x‖
have rw₃ : ‖x + t • x‖ = ‖x + t • x‖
Tactic: rw [← norm_eq_abs, ← norm_smul, add_smul, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
⊢ deriv (fun (t : ℝ) ↦ ‖x + t • x‖) 0 = ‖x‖
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖
⊢ deriv (fun (t : ℝ) ↦ ‖x + t • x‖) 0 = ‖x‖
have simp_rw : deriv (fun (t : ℝ) ↦ |1 + t| * ‖x‖) 0 = ‖x‖
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖
⊢ deriv (fun (t : ℝ) ↦ |1 + t| * ‖x‖) 0 = ‖x‖
have rw : deriv (fun (t : ℝ) ↦ |1 + t|) 0 * ‖x‖ = ‖x‖
Tactic: rw [deriv_mul_const]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖
⊢ deriv (fun (t : ℝ) ↦ |1 + t| * ‖x‖) 0 = ‖x‖
have hc : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ |1 + t|) 0
Tactic: rw [deriv_mul_const]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖
| deriv (fun (t : ℝ) ↦ |1 + t|) 0 * ‖x‖
have enter : fun (t : ℝ) ↦ |1 + t|
Tactic: enter [1, 1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖
| deriv (fun (t : ℝ) ↦ |1 + t|) 0 * ‖x‖
have enter : _root_.abs ∘ fun (t : ℝ) ↦ 1 + t
Tactic: enter [1, 1]; change _root_.abs ∘ (fun t ↦ 1 + t)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖
⊢ deriv (𝕜 := ℝ) (_root_.abs ∘ fun (t : ℝ) ↦ 1 + t) 0 * ‖x‖ = ‖x‖
have rw : HMul.hMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) 1 0)) : ℝ) 1 * ‖x‖ = ‖x‖
Tactic: rw [deriv_comp, deriv_abs, deriv_const_add_id]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖
⊢ deriv (𝕜 := ℝ) (_root_.abs ∘ fun (t : ℝ) ↦ 1 + t) 0 * ‖x‖ = ‖x‖
have hh₂ : DifferentiableAt ℝ _root_.abs (HAdd.hAdd (α := ℝ) 1 0)
Tactic: rw [deriv_comp, deriv_abs, deriv_const_add_id]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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)
⊢ deriv (𝕜 := ℝ) (_root_.abs ∘ fun (t : ℝ) ↦ 1 + t) 0 * ‖x‖ = ‖x‖
have hh : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ 1 + t) 0
Tactic: rw [deriv_comp, deriv_abs, deriv_const_add_id]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
have 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)
Tactic: cases subsingleton_or_nontrivial E
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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)
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
have 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)
Tactic: cases subsingleton_or_nontrivial E
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : Subsingleton E
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
have inl : 0 = HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) 0
Tactic: simp_rw [(hasFDerivAt_of_subsingleton _ _).fderiv, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : Nontrivial E
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
have 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)
Tactic: by_cases hd : DifferentiableAt ℝ (‖·‖) x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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)
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
have 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)
Tactic: by_cases hd : DifferentiableAt ℝ (‖·‖) x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
have 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)
Tactic: obtain rfl | ht := eq_or_ne t 0
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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)
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
have 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)
Tactic: obtain rfl | ht := eq_or_ne t 0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
have pos : Eq.{u_1 + 1} (α := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) 0) 0
Tactic: simp only [zero_smul, _root_.sign_zero, SignType.coe_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
have 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)
Tactic: rw [(hd.hasFDerivAt.hasFDerivAt_norm_smul ht).fderiv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
have neg : 0 = HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) 0
Tactic: rw [fderiv_zero_of_not_differentiableAt hd, fderiv_zero_of_not_differentiableAt]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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
neg : 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)
have neg₁ : ¬DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (t • x)
Tactic: rw [fderiv_zero_of_not_differentiableAt hd, fderiv_zero_of_not_differentiableAt]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
⊢ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) x) = 1
have this : x ≠ 0
Tactic: have : x ≠ 0 := fun hx ↦ not_differentiableAt_norm_zero E (hx ▸ h)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : x ≠ 0
⊢ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) x) = 1
have refine : 1 ≤ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
Tactic: refine le_antisymm (NNReal.coe_one ▸ norm_fderiv_le_of_lipschitz ℝ lipschitzWith_one_norm) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : x ≠ 0
⊢ 1 ≤ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
have apply : 1 * ‖x‖ ≤ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) x) * ‖x‖
Tactic: apply le_of_mul_le_mul_right _ (norm_pos_iff.2 this)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : x ≠ 0
⊢ 1 * ‖x‖ = (fderiv ℝ (fun (x : E) ↦ ‖x‖) x : (a : E) → ℝ) x
have rw : ‖x‖ = (fderiv ℝ (fun (x : E) ↦ ‖x‖) x : (a : E) → ℝ) x
Tactic: rw [one_mul, h.fderiv_norm_self]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : x ≠ 0
rw : ‖x‖ = (fderiv ℝ (fun (x : E) ↦ ‖x‖) x : (a : E) → ℝ) x
⊢ 1 * ‖x‖ = (fderiv ℝ (fun (x : E) ↦ ‖x‖) x : (a : E) → ℝ) x
have rw₁ : ‖x‖ = ‖x‖
Tactic: rw [one_mul, h.fderiv_norm_self]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : x ≠ 0
⊢ 1 * ‖x‖ ≤ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) x) * ‖x‖
have fderiv : 1 * ‖x‖ = (fderiv ℝ (fun (x : E) ↦ ‖x‖) x : (a : E) → ℝ) x
Tactic: calc
    1 * ‖x‖ = fderiv ℝ (‖·‖) x x := by rw [one_mul, h.fderiv_norm_self]
    _ ≤ ‖fderiv ℝ (‖·‖) x x‖ := le_norm_self _
    _ ≤ ‖fderiv ℝ (‖·‖) x‖ * ‖x‖ := le_opNorm _ _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
h' : E →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hf_emb : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
htendsto : Tendsto (Prod.map g g) lE lF
hh : HasFDerivAtFilter h h' lE
hf : HasFDerivAtFilter f f' lF
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
ho :
  Asymptotics.IsBigOTVS.{u_1, u_2, u_3, u_4} 𝕜 (E := F) (F := G) lE
    (fun (x : E × E) ↦
      match (motive := E × E → F) x with
      | (x, y) => HSub.hSub (β := F) (g x - g y) ((g' : (a : E) → F) (x - y) : F))
    fun (x : E × E) ↦
    match (motive := E × E → G) x with
    | (x, y) => HSub.hSub (α := G) (β := G) ((f' : (a : F) → G) (g x - g y) : G) ((h' : (a : E) → G) (x - y) : G)
⊢ HasFDerivAtFilter g g' lE
have refine : Asymptotics.IsLittleOTVS 𝕜 (F := E) lE
  (HSub.hSub (α := E × E → G) (fun (p : E × E) ↦ h p.1 - h p.2) fun (x : E × E) ↦ (f' : (a : F) → G) (g x.1 - g x.2))
  fun (p : E × E) ↦ p.1 - p.2
Tactic: refine .of_isLittleOTVS <| ho.trans_isLittleOTVS <| .triangle (.symm ?_) hh.isLittleOTVS