awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x
⊢ Eq (α := E →L[𝕜] 𝔸')
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
      (∑ i ∈ u.attach,
        (∏ j ∈ u.attach.erase i, g (↑j : ι) x) •> proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
      (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)))
    (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i)
have h : ∀ (x_1 : E),
  Eq.{u_7 + 1} (α := 𝔸')
    ((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
            (∑ i ∈ u.attach,
              (∏ j ∈ u.attach.erase i, g (↑j : ι) x) •> proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
            (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)) :
          (a : E) → 𝔸')
        x_1 :
      𝔸')
    ((∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i : (a : E) → 𝔸') x_1 : 𝔸')
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedRing R
inst_2 : HasSummableGeomSeries R
inst_3 : NormedAlgebra 𝕜 R
x : Rˣ
⊢ HasFDerivAt.{u_1, u_5, u_5} (𝕜 := 𝕜) Ring.inverse
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) (↑x⁻¹ : R) : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R)
        (↑x⁻¹ : R))
    (↑x : R)
have this : IsLittleO (E := R) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R) + (↑x⁻¹ : R) * t * (↑x⁻¹ : R)) id
Tactic: have : (fun t : R => Ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =o[𝓝 0] id :=
    (inverse_add_norm_diff_second_order x).trans_isLittleO (isLittleO_norm_pow_id one_lt_two)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedRing R
inst_2 : HasSummableGeomSeries R
inst_3 : NormedAlgebra 𝕜 R
x : Rˣ
⊢ HasStrictFDerivAt.{u_1, u_5, u_5} (𝕜 := 𝕜) Ring.inverse
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) (↑x⁻¹ : R) : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R)
        (↑x⁻¹ : R))
    (↑x : R)
have h : Eq.{u_5 + 1} (α := AddCommGroup R) toAddCommGroup NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module 𝕜 R) (NormedSpace.toModule : Module 𝕜 R) (β := Module 𝕜 R) (NormedSpace.toModule : Module 𝕜 R) →
    Eq (α := R →L[𝕜] R)
      (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) (↑x⁻¹ : R) : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R)
            (↑x⁻¹ : R) :
        R →L[𝕜] R)
      (fderiv 𝕜 Ring.inverse (↑x : R) : R →L[𝕜] R)
Tactic: convert! (analyticAt_inverse (𝕜 := 𝕜) x).hasStrictFDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedDivisionRing R
inst_2 : NormedAlgebra 𝕜 R
s : Set R
x : R
hx : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := R →L[𝕜] R) (fderivWithin 𝕜 (fun (x : R) ↦ x⁻¹) s x)
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) x⁻¹ : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R) x⁻¹)
have rw : Eq (α := R →L[𝕜] R) (fderiv 𝕜 Inv.inv x)
  (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) x⁻¹ : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R) x⁻¹)
Tactic: rw [DifferentiableAt.fderivWithin (differentiableAt_inv hx) hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
⊢ ¬DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
have obtain : ∀ (x : E) (hx : 0 < ‖x‖), ¬DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
Tactic: obtain ⟨x, hx⟩ := NormedSpace.exists_lt_norm ℝ E 0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (hypothesis)
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
⊢ False
have this : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ ‖t • x‖) 0
Tactic: have : DifferentiableAt ℝ (fun t : ℝ ↦ ‖t • x‖) 0 := DifferentiableAt.comp _ (by simpa) (by simp)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (hypothesis)
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
have this₁ : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ |t| * ‖x‖) 0
Tactic: simp_rw [norm_smul, norm_eq_abs] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (hypothesis)
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
have aux : Eq (α := (a : ℝ) → ℝ) abs fun (t : ℝ) ↦ 1 / ‖x‖ * (|t| * ‖x‖)
Tactic: have aux : abs = fun t ↦ (1 / ‖x‖) * (|t| * ‖x‖) := by field_simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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 : ℝ) ↦ |x|) 0
have rw : DifferentiableAt ℝ (F := ℝ) (fun (x_1 : ℝ) ↦ (fun (t : ℝ) ↦ 1 / ‖x‖ * (|t| * ‖x‖)) x_1) 0
Tactic: rw [aux]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (hypothesis)
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
⊢ False
have this₁ : 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 _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (hypothesis)
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 := ℝ) n (fun (x : E) ↦ ‖x‖) (t • x)
have h1 : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (hypothesis)
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 (x : E) ↦ ‖x‖) (t • x)
have h2 : ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ |t| * ‖y‖) x
Tactic: have h2 : ContDiffAt ℝ n (fun y ↦ |t| * ‖y‖) 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
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‖) x
have enter : x
Tactic: enter [4]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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
| 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
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‖) x
have enter : t⁻¹ • t • x
Tactic: enter [4]; 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
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 (x : E) ↦ ‖x‖) (t • x)
have h2₁ : 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]
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
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 (x : E) ↦ ‖x‖) (t • x)
have h₁ : Eq (α := E → ℝ) (fun (x : E) ↦ ‖x‖) ((fun (y : E) ↦ |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹)
Tactic: convert! h2.comp (t • x) h1 using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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)
⊢ Eq (α := E → ℝ) (fun (x : E) ↦ ‖x‖) ((fun (y : E) ↦ |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹)
have h₁ : ∀ (y : E), ‖y‖ = ((fun (y : E) ↦ |t| * ‖y‖) ∘ HSMul.hSMul t⁻¹) 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
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
⊢ ‖y‖ = |t| * ‖t⁻¹ • y‖
have h₁ : ‖y‖ = |t| * (‖t⁻¹‖ * ‖y‖)
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
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‖)
⊢ ‖y‖ = |t| * ‖t⁻¹ • y‖
have h₂ : ‖y‖ = |t| * ‖t⁻¹‖ * ‖y‖
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
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‖
⊢ ‖y‖ = |t| * ‖t⁻¹ • y‖
have h₃ : ‖y‖ = |t| * |t⁻¹| * ‖y‖
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
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‖
⊢ ‖y‖ = |t| * ‖t⁻¹ • y‖
have h₄ : ‖y‖ = |t * t⁻¹| * ‖y‖
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
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‖
⊢ ‖y‖ = |t| * ‖t⁻¹ • y‖
have h₅ : ‖y‖ = |1| * ‖y‖
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
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‖
⊢ ‖y‖ = |t| * ‖t⁻¹ • y‖
have h₆ : ‖y‖ = 1 * ‖y‖
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
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‖
⊢ ‖y‖ = |t| * ‖t⁻¹ • y‖
have h₇ : ‖y‖ = ‖y‖
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
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‖) x
have h : x = t⁻¹ • t • x
Tactic: convert! hd.contDiffAt_norm_smul (inv_ne_zero ht)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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)
⊢ 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
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
hd : ContDiffAt ℝ (F := ℝ) n (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
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
⊢ 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
n : WithTop ℕ∞
x : E
t : ℝ
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (t • x)
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
have inl : ∀ (h : ContDiffAt ℝ (F := ℝ) 0 (fun (x : E) ↦ ‖x‖) (t • x)), ContDiffAt ℝ (F := ℝ) 0 (fun (x : E) ↦ ‖x‖) x
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
have inr : ∀ (hn : n ≠ 0), ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- 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 : ContDiffAt ℝ (F := ℝ) 0 (fun (x : E) ↦ ‖x‖) (t • x)
⊢ ContDiffAt ℝ (F := ℝ) 0 (fun (x : E) ↦ ‖x‖) x
have inl : ∃ u ∈ nhds x, ContinuousOn (Y := ℝ) (fun (x : E) ↦ ‖x‖) u
Tactic: apply contDiffAt_zero.2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
have inr : ∀ (h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x)),
  ContDiffAt ℝ (F := ℝ) n (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
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
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
have inr₁ : ∀ (ht : t ≠ 0), ContDiffAt ℝ (F := ℝ) n (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
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) 0 x)
this : Subsingleton E
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) x
have rw : ContDiffAt ℝ n (Function.const E (Norm.norm.{u_1} (E := E) 0)) x
Tactic: rw [eq_const_of_subsingleton (‖·‖) 0]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (goal)
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‖) x
have inr : Subsingleton E
Tactic: suffices Subsingleton E by
      rw [eq_const_of_subsingleton (‖·‖) 0]
      exact contDiffAt_const
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Norm (hypothesis)
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)
⊢ Subsingleton E
have h₁ : ContDiffAt ℝ (F := ℝ) n (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
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ ‖x‖) 0
⊢ Subsingleton E
have inr : ∀ (this : Nontrivial E), False
Tactic: by_contra!
-- 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 : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) f x
⊢ HasStrictFDerivAt (fun (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f) (t • x)
have h1 : 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⁻¹
-- 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 : 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 (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f) (t • x)
have h2 : HasStrictFDerivAt (fun (y : E) ↦ |t| * ‖y‖) (|t| • f) x
Tactic: have h2 : HasStrictFDerivAt (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 : 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
| 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 : 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) 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 : 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 (x : E) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f) (t • x)
have h2₁ : 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]
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 : 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) ↦ ‖x‖) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) f) (t • x)
have h₁ : ∀ (x : E), ‖x‖ = |t| * ‖t⁻¹ • x‖
Tactic: convert! h2.comp (t • x) h1 with y