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 : 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‖
⊢ HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f) (t • x)
have 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)
Tactic: convert! h2.comp (t • x) h1 with y
-- 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 : 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
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₁ : ‖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]
-- 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 : 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‖)
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₂ : ‖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]
-- 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 : 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‖
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₃ : ‖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]
-- 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 : 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‖
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₄ : ‖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]
-- 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 : 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‖
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₅ : ‖x_1‖ = |1| * ‖x_1‖
Tactic: rw [norm_smul, ← mul_assoc, norm_eq_abs, ← abs_mul, mul_inv_cancel₀ ht, abs_one, one_mul]
-- 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 : 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‖
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₆ : ‖x_1‖ = 1 * ‖x_1‖
Tactic: rw [norm_smul, ← mul_assoc, norm_eq_abs, ← abs_mul, mul_inv_cancel₀ ht, abs_one, one_mul]
-- 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 : 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‖
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₇ : ‖x_1‖ = ‖x_1‖
Tactic: rw [norm_smul, ← mul_assoc, norm_eq_abs, ← abs_mul, mul_inv_cancel₀ ht, abs_one, one_mul]
-- 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 : 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
⊢ HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f =
    (|t| • f) ∘SL HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)
have 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 : ℝ)
Tactic: ext y
-- 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 : 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
⊢ 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 : ℝ)
have h₁ : HMul.hMul (α := ℝ) (β := ℝ) ((↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) : ℝ) ((f : (a : E) → ℝ) y : ℝ) =
  t⁻¹ * HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ)
Tactic: simp only [coe_smul', Pi.smul_apply, smul_eq_mul, comp_smulₛₗ, map_inv₀, RingHom.id_apply,
    comp_id]
-- 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 : 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
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) : ℝ) ((f : (a : E) → ℝ) y : ℝ) =
    t⁻¹ * HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ)
have h₁ : t * HMul.hMul (α := ℝ) (β := ℝ) ((↑((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 : 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 : ℝ)
⊢ 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 : 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 : ℝ)
⊢ 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 (hypothesis)
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 (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f) (t • x)
have h1 : 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⁻¹
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (hypothesis)
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 (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f) (t • x)
have h2 : HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x
Tactic: have h2 : HasFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) x := h.const_smul |t|
-- 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) x
| HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x
have enter : x
Tactic: enter [3]
-- 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) x
| x
have rw : t⁻¹ • t • x
Tactic: rw [← one_smul ℝ x, ← inv_mul_cancel₀ ht, mul_smul]
-- 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) x
| HasFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x
have enter : t⁻¹ • t • x
Tactic: enter [3]; rw [← one_smul ℝ x, ← inv_mul_cancel₀ ht, mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (hypothesis)
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 (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f) (t • x)
have h2₁ : 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]
Cleared hypotheses: h2
-- 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)
⊢ HasFDerivAt (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f) (t • x)
have h₁ : ∀ (x : E), ‖x‖ = ((fun (y : E) ↦ |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹) x
Tactic: convert! h2.comp (t • x) h1 using 2 with y
-- 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)
h₁ : ∀ (x : E), ‖x‖ = ((fun (y : E) ↦ |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹) x
⊢ HasFDerivAt (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f) (t • x)
have 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)
Tactic: convert! h2.comp (t • x) h1 using 2 with y
-- 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)
x_1 : E
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₁ : ‖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]
-- 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)
x_1 : E
h₁ : ‖x_1‖ = |t| * (‖t⁻¹‖ * ‖x_1‖)
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₂ : ‖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]
-- 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)
x_1 : E
h₁ : ‖x_1‖ = |t| * (‖t⁻¹‖ * ‖x_1‖)
h₂ : ‖x_1‖ = |t| * ‖t⁻¹‖ * ‖x_1‖
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₃ : ‖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]
-- 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)
x_1 : E
h₁ : ‖x_1‖ = |t| * (‖t⁻¹‖ * ‖x_1‖)
h₂ : ‖x_1‖ = |t| * ‖t⁻¹‖ * ‖x_1‖
h₃ : ‖x_1‖ = |t| * |t⁻¹| * ‖x_1‖
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₄ : ‖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]
-- 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)
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‖
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₅ : ‖x_1‖ = |1| * ‖x_1‖
Tactic: rw [norm_smul, ← mul_assoc, norm_eq_abs, ← abs_mul, mul_inv_cancel₀ ht, abs_one, one_mul]
-- 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)
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‖
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₆ : ‖x_1‖ = 1 * ‖x_1‖
Tactic: rw [norm_smul, ← mul_assoc, norm_eq_abs, ← abs_mul, mul_inv_cancel₀ ht, abs_one, one_mul]
-- 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)
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‖
⊢ ‖x_1‖ = |t| * ‖t⁻¹ • x_1‖
have h₇ : ‖x_1‖ = ‖x_1‖
Tactic: rw [norm_smul, ← mul_assoc, norm_eq_abs, ← abs_mul, mul_inv_cancel₀ ht, abs_one, one_mul]
-- 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
⊢ HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f =
    (|t| • f) ∘SL HSMul.hSMul (β := E →L[ℝ] E) t⁻¹ (ContinuousLinearMap.id ℝ E)
have 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 : ℝ)
Tactic: ext y
-- 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
⊢ 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 : ℝ)
have h₁ : HMul.hMul (α := ℝ) (β := ℝ) ((↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) : ℝ) ((f : (a : E) → ℝ) y : ℝ) =
  t⁻¹ * HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ)
Tactic: simp only [coe_smul', Pi.smul_apply, smul_eq_mul, comp_smulₛₗ, map_inv₀, RingHom.id_apply,
      comp_id]
-- 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
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) : ℝ) ((f : (a : E) → ℝ) y : ℝ) =
    t⁻¹ * HMul.hMul (β := ℝ) |t| ((f : (a : E) → ℝ) y : ℝ)
have h₁ : t * HMul.hMul (α := ℝ) (β := ℝ) ((↑((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]