awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : E) ↦ ‖x‖ * ‖x‖ ^ (p - 1)) fun (x : E) ↦ ‖x‖ * 1
have refine : Filter.Tendsto (β := ℝ) (fun (x : E) ↦ ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)
Tactic: refine (isBigO_refl _ _).mul_isLittleO <| (isLittleO_const_iff <| by simp).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ Filter.Tendsto (β := ℝ) (fun (x : E) ↦ ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)
have h : 0 = Norm.norm.{u_1} (E := E) (id 0) ^ (p - 1)
Tactic: convert! continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ IsBigO (E := ℝ) (F := E) (𝓝 0) (fun (x : E) ↦ ‖x‖ * 1) fun (x : E) ↦ x - 0
have simp_rw : IsBigO (E := ℝ) (F := E) (𝓝 0) (fun (x : E) ↦ ‖x‖) fun (x : E) ↦ x - 0
Tactic: simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
simp_rw : IsBigO (E := ℝ) (F := E) (𝓝 0) (fun (x : E) ↦ ‖x‖) fun (x : E) ↦ x - 0
⊢ IsBigO (E := ℝ) (F := E) (𝓝 0) (fun (x : E) ↦ ‖x‖ * 1) fun (x : E) ↦ x - 0
have simp_rw₁ : IsBigO (E := E) (F := E) (𝓝 0) (fun (x : E) ↦ x) fun (x : E) ↦ x - 0
Tactic: simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
simp_rw : IsBigO (E := ℝ) (F := E) (𝓝 0) (fun (x : E) ↦ ‖x‖) fun (x : E) ↦ x - 0
simp_rw₁ : IsBigO (E := E) (F := E) (𝓝 0) (fun (x : E) ↦ x) fun (x : E) ↦ x - 0
⊢ IsBigO (E := ℝ) (F := E) (𝓝 0) (fun (x : E) ↦ ‖x‖ * 1) fun (x : E) ↦ x - 0
have simp_rw₂ : IsBigO (E := E) (F := E) (𝓝 0) (fun (x : E) ↦ x) fun (x : E) ↦ x
Tactic: simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ IsLittleO (E := ℝ) (F := E) (𝓝 0)
    (fun (x' : E) ↦ HSub.hSub (β := ℝ) (‖x'‖ ^ p - Norm.norm.{u_1} (E := E) 0 ^ p) ((0 : (a : E) → ℝ) (x' - 0) : ℝ))
    fun (x' : E) ↦ x' - 0
have calc : Eq.{u_1 + 1} (α := (x : E) → ℝ) (fun (x : E) ↦ ‖x‖ ^ p - Norm.norm.{u_1} (E := E) 0 ^ p - 0) fun (x : E) ↦ ‖x‖ ^ p
Tactic: calc (fun x : E ↦ ‖x‖ ^ p - ‖(0 : E)‖ ^ p - 0)
        = (fun x : E ↦ ‖x‖ ^ p) := by simp [zero_lt_one.trans hp |>.ne']
      _ = (fun x : E ↦ ‖x‖ * ‖x‖ ^ (p - 1)) := by
          ext x
          rw [← rpow_one_add' (norm_nonneg x) (by positivity)]
          ring_nf
      _ =o[𝓝 0] (fun x : E ↦ ‖x‖ * 1) := by
        refine (isBigO_refl _ _).mul_isLittleO <| (isLittleO_const_iff <| by simp).mpr ?_
        convert! continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto
        simp [h2p.ne']
      _ =O[𝓝 0] (fun (x : E) ↦ x - 0) := by
        simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
calc :
  Eq.{u_1 + 1} (α := (x : E) → ℝ) (fun (x : E) ↦ ‖x‖ ^ p - Norm.norm.{u_1} (E := E) 0 ^ p - 0) fun (x : E) ↦ ‖x‖ ^ p
⊢ IsLittleO (E := ℝ) (F := E) (𝓝 0)
    (fun (x' : E) ↦ HSub.hSub (β := ℝ) (‖x'‖ ^ p - Norm.norm.{u_1} (E := E) 0 ^ p) ((0 : (a : E) → ℝ) (x' - 0) : ℝ))
    fun (x' : E) ↦ x' - 0
have calc₁ : Eq.{u_1 + 1} (α := (x : E) → ℝ) (fun (x : E) ↦ ‖x‖ ^ p) fun (x : E) ↦ ‖x‖ * ‖x‖ ^ (p - 1)
Tactic: calc (fun x : E ↦ ‖x‖ ^ p - ‖(0 : E)‖ ^ p - 0)
        = (fun x : E ↦ ‖x‖ ^ p) := by simp [zero_lt_one.trans hp |>.ne']
      _ = (fun x : E ↦ ‖x‖ * ‖x‖ ^ (p - 1)) := by
          ext x
          rw [← rpow_one_add' (norm_nonneg x) (by positivity)]
          ring_nf
      _ =o[𝓝 0] (fun x : E ↦ ‖x‖ * 1) := by
        refine (isBigO_refl _ _).mul_isLittleO <| (isLittleO_const_iff <| by simp).mpr ?_
        convert! continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto
        simp [h2p.ne']
      _ =O[𝓝 0] (fun (x : E) ↦ x - 0) := by
        simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
calc :
  Eq.{u_1 + 1} (α := (x : E) → ℝ) (fun (x : E) ↦ ‖x‖ ^ p - Norm.norm.{u_1} (E := E) 0 ^ p - 0) fun (x : E) ↦ ‖x‖ ^ p
calc₁ : Eq.{u_1 + 1} (α := (x : E) → ℝ) (fun (x : E) ↦ ‖x‖ ^ p) fun (x : E) ↦ ‖x‖ * ‖x‖ ^ (p - 1)
⊢ IsLittleO (E := ℝ) (F := E) (𝓝 0)
    (fun (x' : E) ↦ HSub.hSub (β := ℝ) (‖x'‖ ^ p - Norm.norm.{u_1} (E := E) 0 ^ p) ((0 : (a : E) → ℝ) (x' - 0) : ℝ))
    fun (x' : E) ↦ x' - 0
have calc₂ : IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : E) ↦ ‖x‖ * ‖x‖ ^ (p - 1)) fun (x : E) ↦ ‖x‖ * 1
Tactic: calc (fun x : E ↦ ‖x‖ ^ p - ‖(0 : E)‖ ^ p - 0)
        = (fun x : E ↦ ‖x‖ ^ p) := by simp [zero_lt_one.trans hp |>.ne']
      _ = (fun x : E ↦ ‖x‖ * ‖x‖ ^ (p - 1)) := by
          ext x
          rw [← rpow_one_add' (norm_nonneg x) (by positivity)]
          ring_nf
      _ =o[𝓝 0] (fun x : E ↦ ‖x‖ * 1) := by
        refine (isBigO_refl _ _).mul_isLittleO <| (isLittleO_const_iff <| by simp).mpr ?_
        convert! continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto
        simp [h2p.ne']
      _ =O[𝓝 0] (fun (x : E) ↦ x - 0) := by
        simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
calc :
  Eq.{u_1 + 1} (α := (x : E) → ℝ) (fun (x : E) ↦ ‖x‖ ^ p - Norm.norm.{u_1} (E := E) 0 ^ p - 0) fun (x : E) ↦ ‖x‖ ^ p
calc₁ : Eq.{u_1 + 1} (α := (x : E) → ℝ) (fun (x : E) ↦ ‖x‖ ^ p) fun (x : E) ↦ ‖x‖ * ‖x‖ ^ (p - 1)
calc₂ : IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : E) ↦ ‖x‖ * ‖x‖ ^ (p - 1)) fun (x : E) ↦ ‖x‖ * 1
⊢ IsLittleO (E := ℝ) (F := E) (𝓝 0)
    (fun (x' : E) ↦ HSub.hSub (β := ℝ) (‖x'‖ ^ p - Norm.norm.{u_1} (E := E) 0 ^ p) ((0 : (a : E) → ℝ) (x' - 0) : ℝ))
    fun (x' : E) ↦ x' - 0
have calc₃ : IsBigO (E := ℝ) (F := E) (𝓝 0) (fun (x : E) ↦ ‖x‖ * 1) fun (x : E) ↦ x - 0
Tactic: calc (fun x : E ↦ ‖x‖ ^ p - ‖(0 : E)‖ ^ p - 0)
        = (fun x : E ↦ ‖x‖ ^ p) := by simp [zero_lt_one.trans hp |>.ne']
      _ = (fun x : E ↦ ‖x‖ * ‖x‖ ^ (p - 1)) := by
          ext x
          rw [← rpow_one_add' (norm_nonneg x) (by positivity)]
          ring_nf
      _ =o[𝓝 0] (fun x : E ↦ ‖x‖ * 1) := by
        refine (isBigO_refl _ _).mul_isLittleO <| (isLittleO_const_iff <| by simp).mpr ?_
        convert! continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto
        simp [h2p.ne']
      _ =O[𝓝 0] (fun (x : E) ↦ x - 0) := by
        simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x
have neg : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
  (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x
Tactic: apply HasStrictFDerivAt.hasFDerivAt
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasStrictFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x
have a : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x ↔
  HasStrictFDerivAt (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2 ^ (p / 2))
    ((p / 2 * HPow.hPow (β := ℕ) ‖x‖ 2 ^ (p / 2 - 1)) •
      HSMul.hSMul (α := ℕ) (β := E →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ))
    x
Tactic: convert! (hasStrictFDerivAt_norm_sq x).rpow_const (p := p / 2) (by simp [hx]) using 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasStrictFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
      (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x ↔
    HasStrictFDerivAt (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2 ^ (p / 2))
      ((p / 2 * HPow.hPow (β := ℕ) ‖x‖ 2 ^ (p / 2 - 1)) •
        HSMul.hSMul (α := ℕ) (β := E →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ))
      x
have a : HasStrictFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x ↔
  HasStrictFDerivAt (fun (x : E) ↦ ‖x‖ ^ ((↑2 : ℝ) * (p / 2)))
    (HSMul.hSMul (β := StrongDual ℝ E) (p / 2 * ‖x‖ ^ ((↑2 : ℝ) * (p / 2 - 1)) * (↑2 : ℝ))
      ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ))
    x
Tactic: simp_rw [← Real.rpow_natCast_mul (norm_nonneg _), ← Nat.cast_smul_eq_nsmul ℝ, smul_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
x p : ℝ
hp : 1 < p
⊢ HasDerivAt (fun (x : ℝ) ↦ ‖x‖ ^ p) (p * ‖x‖ ^ (p - 2) * x) x
have h : p * ‖x‖ ^ (p - 2) * x =
  (HSMul.hSMul (β := ℝ →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) 1
Tactic: convert! hasFDerivAt_norm_rpow x hp |>.hasDerivAt using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ Norm.norm (E := F →L[ℝ] ℝ) (fderiv ℝ (fun (x : F) ↦ ‖f x‖ ^ p) x) ≤
    p * ‖f x‖ ^ (p - 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)
have rw : ‖p‖ * ‖‖f x‖ ^ (p - 2)‖ *
    Norm.norm (E := F →L[ℝ] ℝ)
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (f x)) (fderiv ℝ f x)) ≤
  p * ‖f x‖ ^ (p - 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)
Tactic: rw [hf.fderiv_norm_rpow hp, norm_smul, norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖‖f x‖ ^ (p - 2)‖ *
      Norm.norm (E := F →L[ℝ] ℝ)
        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (f x)) (fderiv ℝ f x)) ≤
    p * ‖f x‖ ^ (p - 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)
have simp_rw : p *
    (‖f x‖ ^ (p - 2) *
      Norm.norm (E := F →L[ℝ] ℝ)
        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (f x)) (fderiv ℝ f x))) ≤
  p * (‖f x‖ ^ (p - 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x))
Tactic: simp_rw [norm_rpow_of_nonneg (norm_nonneg _), norm_norm, norm_eq_abs,
    abs_eq_self.mpr <| zero_le_one.trans hp.le, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ p *
      (‖f x‖ ^ (p - 2) *
        Norm.norm (E := F →L[ℝ] ℝ)
          (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (f x)) (fderiv ℝ f x))) ≤
    p * (‖f x‖ ^ (p - 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x))
have hbc : ‖f x‖ ^ (p - 2) *
    Norm.norm (E := F →L[ℝ] ℝ)
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (f x)) (fderiv ℝ f x)) ≤
  ‖f x‖ ^ (p - 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)
Tactic: gcongr _ * ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖f x‖ ^ (p - 2) *
      Norm.norm (E := F →L[ℝ] ℝ)
        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (f x)) (fderiv ℝ f x)) ≤
    ‖f x‖ ^ (p - 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)
have hbc : ‖f x‖ ^ (p - 2) *
    (Norm.norm (E := E →L[ℝ] ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (f x) : E →L[ℝ] ℝ) *
      Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)) =
  ‖f x‖ ^ (p - 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)
Tactic: refine mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le ..) (by positivity)
    |>.trans_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ p - 2 + 1 ≠ 0
have linarith : p - 2 + 1 = 0 → 1 - p + (p - 2 + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖f x‖ ^ (p - 2) *
      (Norm.norm (E := E →L[ℝ] ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (f x) : E →L[ℝ] ℝ) *
        Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)) =
    ‖f x‖ ^ (p - 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)
have hbc : ‖f x‖ ^ (p - 2 + 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x) =
  ‖f x‖ ^ (p - 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)
Tactic: rw [innerSL_apply_norm, ← mul_assoc, ← Real.rpow_add_one' (by positivity) (by linarith)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖ ^ p) x) = p * ‖x‖ ^ (p - 1)
have rw : ‖p‖ * ‖‖x‖ ^ (p - 2)‖ * Norm.norm (E := E →L[ℝ] ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) = p * ‖x‖ ^ (p - 1)
Tactic: rw [fderiv_norm_rpow x hp, norm_smul, norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖‖x‖ ^ (p - 2)‖ * Norm.norm (E := E →L[ℝ] ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) =
    p * ‖x‖ ^ (p - 1)
have simp_rw : p * (‖x‖ ^ (p - 2) * ‖x‖) = p * ‖x‖ ^ (p - 1)
Tactic: simp_rw [norm_rpow_of_nonneg (norm_nonneg _), norm_norm, norm_eq_abs,
    abs_eq_self.mpr <| zero_le_one.trans hp.le, mul_assoc, innerSL_apply_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ p - 2 + 1 ≠ 0
have linarith : p - 2 + 1 = 0 → 1 - p + (p - 2 + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ p * (‖x‖ ^ (p - 2) * ‖x‖) = p * ‖x‖ ^ (p - 1)
have rw : p * ‖x‖ ^ (p - 2 + 1) = p * ‖x‖ ^ (p - 1)
Tactic: rw [← Real.rpow_add_one' (by positivity) (by linarith)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ ContDiff ℝ (F := ℝ) 1 fun (x : E) ↦ ‖x‖ ^ p
have rw : (Differentiable ℝ (F := ℝ) fun (x : E) ↦ ‖x‖ ^ p) ∧
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p)
Tactic: rw [contDiff_one_iff_fderiv]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ (Differentiable ℝ (F := ℝ) fun (x : E) ↦ ‖x‖ ^ p) ∧
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p)
have refine : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p)
Tactic: refine ⟨fun x ↦ hasFDerivAt_norm_rpow x hp |>.differentiableAt, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p)
have simp_rw : ∀ (x : E), ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x
Tactic: simp_rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
⊢ ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x
have pos : ∀ (hx : x = 0), ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
pos : ∀ (hx : x = 0), ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x
⊢ ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x
have neg : ∀ (hx : ¬x = 0), ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x
have pos : Filter.Tendsto.{u_1, u_1} (α := E) (β := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) (𝓝 0) (𝓝 0)
Tactic: simp_rw [hx, ContinuousAt, fderiv_norm_rpow (0 : E) hp, norm_zero, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto.{u_1, u_1} (α := E) (β := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) (𝓝 0) (𝓝 0)
have pos : Filter.Tendsto (β := ℝ) (fun (x : E) ↦ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖ ^ p) x)) (𝓝 0) (𝓝 0)
Tactic: rw [tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (β := ℝ) (fun (x : E) ↦ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖ ^ p) x)) (𝓝 0) (𝓝 0)
have pos : Filter.Tendsto (β := ℝ) (fun (x : E) ↦ p * ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le (tendsto_const_nhds) ?_
      (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_fderiv_norm_id_rpow _ hp |>.le)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (β := ℝ) (fun (x : E) ↦ p * ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)
have pos : ContinuousAt (Y := ℝ) (fun (x : E) ↦ p * ‖x‖ ^ (p - 1)) 0
Tactic: suffices ContinuousAt (fun x : E ↦ p * ‖x‖ ^ (p - 1)) 0 by
      simpa [ContinuousAt, sub_ne_zero_of_ne hp.ne'] using this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ ContinuousAt (Y := ℝ) (fun (x : E) ↦ p * ‖x‖ ^ (p - 1)) 0
have funProp : Norm.norm.{u_1} (E := E) 0 ≠ 0 ∨ 0 ≤ p - 1
Tactic: fun_prop (discharger := simp [hp.le])
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
⊢ ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x
have neg : ContinuousAt (Y := E →L[ℝ] ℝ)
  (fun (x : E) ↦ HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x
Tactic: simp_rw [funext fun x ↦ fderiv_norm_rpow (E := E) (x := x) hp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
⊢ ContinuousAt (Y := E →L[ℝ] ℝ)
    (fun (x : E) ↦ HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x
have funProp : ‖x‖ ≠ 0 ∨ 0 ≤ p - 2
Tactic: fun_prop (discharger := simp [hx])
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : ℝ → E
hf : Continuous f
hg : Continuous g
⊢ Continuous.{0, u_1} (Y := 𝕜) fun (x : ℝ) ↦ _root_.inner_ 𝕜 (f x) (g x)
have unfold : Continuous.{0, u_1} (Y := 𝕜) fun (x : ℝ) ↦
  4⁻¹ *
    (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖f x + g x‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖f x + g x‖ : 𝕜) -
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖f x - g x‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖f x - g x‖ : 𝕜) +
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (f x) + g x‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (f x) + g x‖ : 𝕜) -
      HMul.hMul (β := 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (f x) - g x‖ : 𝕜))
        ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (f x) - g x‖ : 𝕜))
Tactic: unfold _root_.inner_