awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
hg_ker : (LinearMap.eqLocus f 1)ᗮ ≤ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮᗮ
⊢ (↑(LinearMap.ker (M₂ := ↥(LinearMap.eqLocus (↑f : E →ₗ[𝕜] E) 1))
          (↑(Submodule.orthogonalProjection (LinearMap.eqLocus f 1)) :
            E →ₗ[𝕜] ↥(LinearMap.eqLocus (↑f : E →ₗ[𝕜] E) 1))) :
      Set E) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑((↑f : E →ₗ[𝕜] E) - 1).range : Set E)

Tactic:
rw [Submodule.ker_orthogonalProjection, ← Submodule.topologicalClosure_coe,
      SetLike.coe_subset_coe, ← Submodule.orthogonal_orthogonal_eq_closure]

Premises used: Submodule.orthogonal_orthogonal_eq_closure, SetLike.coe_subset_coe, Submodule.topologicalClosure_coe, Submodule.ker_orthogonalProjection
-- Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
⊢ (LinearMap.eqLocus f 1)ᗮ ≤ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮᗮ

Tactic:
Submodule.orthogonal_le fun x hx ↦ eq_of_norm_le_re_inner_eq_norm_sq (𝕜 := 𝕜) ?_ ?_

Premises used: eq_of_norm_le_re_inner_eq_norm_sq, Submodule.orthogonal_le
-- Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
hg_ker :
  ∀ (x : E) (hx : x ∈ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮ),
    norm (E := E) ((f : (a : E) → E) x : E) ≤ norm (E := E) ((1 : (a : E) → E) x : E)
hg_ker₁ :
  ∀ (x : E) (hx : x ∈ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮ),
    (RCLike.re : (a : 𝕜) → ℝ) (inner 𝕜 (E := E) ((f : (a : E) → E) x : E) ((1 : (a : E) → E) x : E)) =
      HPow.hPow (β := ℕ) (norm (E := E) ((1 : (a : E) → E) x : E)) 2
⊢ (LinearMap.eqLocus f 1)ᗮ ≤ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮᗮ

Tactic:
refine Submodule.orthogonal_le fun x hx ↦ eq_of_norm_le_re_inner_eq_norm_sq (𝕜 := 𝕜) ?_ ?_

Premises used: Submodule.orthogonal_le
-- Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮ
⊢ norm (E := E) ((f : (a : E) → E) x : E) ≤ norm (E := E) ((1 : (a : E) → E) x : E)

Tactic:
simpa using f.le_of_opNorm_le hf x

Premises used: ContinuousLinearMap.le_of_opNorm_le
-- Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮ
⊢ ∀ (y : E), ⟪(f : (a : E) → E) y, x⟫ = ⟪y, x⟫

Tactic:
simpa [Submodule.mem_orthogonal, inner_sub_left, sub_eq_zero] using hx

Premises used: sub_eq_zero, inner_sub_left, Submodule.mem_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮ
⊢ ∀ (y : E), ⟪(f : (a : E) → E) y, x⟫ = ⟪y, x⟫

Tactic:
have : ∀ y, ⟪f y, x⟫ = ⟪y, x⟫ := by
        simpa [Submodule.mem_orthogonal, inner_sub_left, sub_eq_zero] using hx
-- Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮ
this : ∀ (y : E), ⟪(f : (a : E) → E) y, x⟫ = ⟪y, x⟫
⊢ (RCLike.re : (a : 𝕜) → ℝ) (inner 𝕜 (E := E) ((f : (a : E) → E) x : E) ((1 : (a : E) → E) x : E)) =
    HPow.hPow (β := ℕ) (norm (E := E) ((1 : (a : E) → E) x : E)) 2

Tactic:
simp [this]
-- Module: Mathlib.Analysis.InnerProductSpace.MulOpposite
Goal:
𝕜 : Type u_1
H : Type u_2
inst : Inner 𝕜 H
x y : Hᵐᵒᵖ
⊢ inner 𝕜 (unop x) (unop y) = inner 𝕜 x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.MulOpposite
Goal:
𝕜 : Type u_1
H : Type u_2
inst : Inner 𝕜 H
x y : H
⊢ inner 𝕜 (op x) (op y) = inner 𝕜 x y

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.MulOpposite
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
ι : Type u_3
b : Module.Basis ι 𝕜 H
⊢ Orthonormal.{u_1, u_2, u_3} 𝕜 (E := Hᵐᵒᵖ) (ι := ι) (⇑b.mulOpposite : (a : ι) → Hᵐᵒᵖ) ↔
    Orthonormal.{u_1, u_2, u_3} 𝕜 (E := H) (ι := ι) (⇑b : (a : ι) → H)

Tactic:
Iff.rfl

Premises used: Orthonormal, Iff.rfl, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Analysis.InnerProductSpace.MulOpposite
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 H
⊢ b.mulOpposite.toBasis = b.toBasis.mulOpposite

Tactic:
rfl

Premises used: LinearEquiv.symm, Multiset.map, Module.Basis.map, Finset.map, Module.Basis.mulOpposite, Set.toFinset, Set.Finite.toFinset, LinearEquiv.toEquiv, MulOpposite.unop, LinearEquiv.trans, rfl, OrthonormalBasis.toBasis, MulOpposite.op
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
pos :
  ∀ (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
neg :
  ∀ (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
⊢ HasFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
pos : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (x : E) ↦ ‖x‖ ^ p) 0 0
⊢ HasFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x

Tactic:
simp only [hx, norm_zero, map_zero, smul_zero]

Premises used: norm_zero, smul_zero, map_zero
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
⊢ 0 < p - 1

Tactic:
have h2p : 0 < p - 1 := sub_pos.mpr hp
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
⊢ HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (x : E) ↦ ‖x‖ ^ p) 0 0

Tactic:
.of_isLittleO ?_

Premises used: HasFDerivAt.of_isLittleO
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
pos :
  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
⊢ HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (x : E) ↦ ‖x‖ ^ p) 0 0

Tactic:
refine .of_isLittleO ?_
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
⊢ 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:
simp [zero_lt_one.trans hp |>.ne']

Premises used: LT.lt.ne', zero_lt_one, LT.lt.trans
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
h : ∀ (x : E), ‖x‖ ^ p = ‖x‖ * ‖x‖ ^ (p - 1)
⊢ Eq.{u_1 + 1} (α := (x : E) → ℝ) (fun (x : E) ↦ ‖x‖ ^ p) fun (x : E) ↦ ‖x‖ * ‖x‖ ^ (p - 1)

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x_1 : E
p : ℝ
hp : 1 < p
hx : x_1 = 0
h2p : 0 < p - 1
x : E
⊢ 1 + (p - 1) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x_1 : E
p : ℝ
hp : 1 < p
hx : x_1 = 0
h2p : 0 < p - 1
x : E
h : ‖x‖ ^ p = ‖x‖ ^ (1 + (p - 1))
⊢ ‖x‖ ^ p = ‖x‖ * ‖x‖ ^ (p - 1)

Tactic:
rw [← rpow_one_add' (norm_nonneg x) (by positivity)]

Premises used: Real.rpow_one_add', norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x_1 : E
p : ℝ
hp : 1 < p
hx : x_1 = 0
h2p : 0 < p - 1
x : E
⊢ ‖x‖ ^ p = ‖x‖ ^ (1 + (p - 1))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
⊢ Ne (α := ℝ) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
refine : Filter.Tendsto (β := ℝ) (fun (x : E) ↦ ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : E) ↦ ‖x‖ * ‖x‖ ^ (p - 1)) fun (x : E) ↦ ‖x‖ * 1

Tactic:
refine (isBigO_refl _ _).mul_isLittleO <| (isLittleO_const_iff <| by simp).mpr ?_

Premises used: Iff.mpr, Asymptotics.isLittleO_const_iff, Asymptotics.IsBigO.mul_isLittleO
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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) ↦ ‖id x‖ ^ (p - 1)) (𝓝 0) (𝓝 (Norm.norm.{u_1} (E := E) (id 0) ^ (p - 1)))

Tactic:
continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto

Premises used: LT.lt.le, ContinuousAt.tendsto, ContinuousAt.rpow_const, ContinuousAt.norm, continuousAt_id, Or.inr
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
h : 0 = Norm.norm.{u_1} (E := E) (id 0) ^ (p - 1)
⊢ Filter.Tendsto (β := ℝ) (fun (x : E) ↦ ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)

Tactic:
convert! continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto

Premises used: LT.lt.le, ContinuousAt.tendsto, ContinuousAt.rpow_const, ContinuousAt.norm, continuousAt_id, Or.inr
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
⊢ 0 = Norm.norm.{u_1} (E := E) (id 0) ^ (p - 1)

Tactic:
simp [h2p.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
simp_rw₂ : IsBigO (E := E) (F := E) (𝓝 0) (fun (x : E) ↦ x) fun (x : E) ↦ x
⊢ IsBigO (E := ℝ) (F := E) (𝓝 0) (fun (x : E) ↦ ‖x‖ * 1) fun (x : E) ↦ x - 0

Tactic:
simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]

Premises used: sub_zero, Asymptotics.isBigO_norm_left, mul_one, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
calc₃ : IsBigO (E := ℝ) (F := E) (𝓝 0) (fun (x : E) ↦ ‖x‖ * 1) fun (x : E) ↦ x - 0
⊢ 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

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]

Premises used: Norm.norm, HMul.hMul, HSub.hSub, nhds, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
neg :
  HasStrictFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x
⊢ HasFDerivAt (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

Premises used: HasStrictFDerivAt.hasFDerivAt
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0 ∨ 1 ≤ p / 2

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
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
⊢ HasStrictFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 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

Premises used: hasStrictFDerivAt_norm_sq, HasStrictFDerivAt.rpow_const
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
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
⊢ 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:
simp_rw [← Real.rpow_natCast_mul (norm_nonneg _), ← Nat.cast_smul_eq_nsmul ℝ, smul_smul]

Premises used: Real, smul_smul, Nat.cast_smul_eq_nsmul, norm_nonneg, Real.rpow_natCast_mul
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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) ↦ ‖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:
ring_nf
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ Differentiable ℝ (F := ℝ) fun (x : E) ↦ ‖x‖ ^ p

Tactic:
fun x ↦ hasFDerivAt_norm_rpow x hp |>.differentiableAt

Premises used: Differentiable, hasFDerivAt_norm_rpow, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
x p : ℝ
hp : 1 < p
⊢ HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ ‖x‖ ^ p)
    ((HSMul.hSMul (β := ℝ →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ)
        1 :
      ℝ)
    x

Tactic:
hasFDerivAt_norm_rpow x hp |>.hasDerivAt

Premises used: hasFDerivAt_norm_rpow, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
x p : ℝ
hp : 1 < p
h :
  p * ‖x‖ ^ (p - 2) * x =
    (HSMul.hSMul (β := ℝ →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) 1
⊢ HasDerivAt (fun (x : ℝ) ↦ ‖x‖ ^ p) (p * ‖x‖ ^ (p - 2) * x) x

Tactic:
convert! hasFDerivAt_norm_rpow x hp |>.hasDerivAt using 1

Premises used: hasFDerivAt_norm_rpow, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
x p : ℝ
hp : 1 < p
⊢ p * ‖x‖ ^ (p - 2) * x =
    (HSMul.hSMul (β := ℝ →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) 1

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
x p : ℝ
hp : 1 < p
⊢ HasDerivAt (fun (x : ℝ) ↦ |x| ^ p) (p * |x| ^ (p - 2) * x) x

Tactic:
simpa using hasDerivAt_norm_rpow x hp

Premises used: hasDerivAt_norm_rpow
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖ ^ p) x =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)

Tactic:
hasFDerivAt_norm_rpow x hp |>.fderiv

Premises used: hasFDerivAt_norm_rpow, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
⊢ fderiv ℝ (fun (x : F) ↦ ‖f x‖ ^ p) x =
    HSMul.hSMul (β := F →L[ℝ] ℝ) (p * ‖f x‖ ^ (p - 2))
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (f x)) (fderiv ℝ f x))

Tactic:
hasFDerivAt_norm_rpow (f x) hp |>.comp x (hf x).hasFDerivAt |>.fderiv

Premises used: ContinuousLinearMap.comp, hasFDerivAt_norm_rpow, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.comp
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
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)
⊢ 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)

Tactic:
rw [hf.fderiv_norm_rpow hp, norm_smul, norm_mul]

Premises used: Differentiable.fderiv_norm_rpow, norm_smul, norm_mul
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
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))
⊢ ‖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]

Premises used: Iff.mpr, mul_assoc, LT.lt.le, norm_norm, zero_le_one, LE.le.trans, Real.norm_rpow_of_nonneg, abs_eq_self, norm_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
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)
⊢ 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:
gcongr _ * ?_
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
⊢ 0 ≤ ‖f x‖ ^ (p - 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
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)
⊢ ‖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:
refine mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le ..) (by positivity)
    |>.trans_eq ?_

Premises used: LE.le.trans_eq, ContinuousLinearMap.opNorm_comp_le, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
⊢ 0 ≤ ‖f x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
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
linarith : p - 2 + 1 = 0 → 1 - p + (p - 2 + 1 - 0) = 0
⊢ p - 2 + 1 ≠ 0

Tactic:
linarith