-- Mathlib/Analysis/InnerProductSpace/NormPow.lean
theorem contDiff_norm_rpow {p : ℝ} (hp : 1 < p) : ContDiff ℝ 1 (fun x : E ↦ ‖x‖ ^ p)

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (fun x => p * ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)

Tactic:
suffices ContinuousAt (fun x : E ↦ p * ‖x‖ ^ (p - 1)) 0  by
  simpa [ContinuousAt, sub_ne_zero_of_ne hp.ne'] using this

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ ContinuousAt (fun x => p * ‖x‖ ^ (p - 1)) 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ Continuous (fderiv ℝ fun x => ‖x‖ ^ p)

Tactic:
simp_rw [continuous_iff_continuousAt]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ ∀ (x : E), ContinuousAt (fderiv ℝ fun x => ‖x‖ ^ p) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ ContDiff ℝ 1 fun x => ‖x‖ ^ p

Tactic:
rw [contDiff_one_iff_fderiv]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ (Differentiable ℝ fun x => ‖x‖ ^ p) ∧ Continuous (fderiv ℝ fun x => ‖x‖ ^ p)

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ ContinuousAt (fun x => p * ‖x‖ ^ (p - 1)) 0

Tactic:
fun_prop (discharger := simp [hp.le])

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
this : ContinuousAt (fun x => p * ‖x‖ ^ (p - 1)) 0
⊢ Filter.Tendsto (fun x => p * ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)

Tactic:
simpa [ContinuousAt, sub_ne_zero_of_ne hp.ne'] using this

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
⊢ ContinuousAt (fderiv ℝ fun x => ‖x‖ ^ p) x

Tactic:
simp_rw [funext fun x ↦ fderiv_norm_rpow (E := E) (x := x) hp]

Result:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
⊢ ContinuousAt (fun x => (p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ ContinuousAt (fderiv ℝ fun x => ‖x‖ ^ p) x

Tactic:
simp_rw [hx, ContinuousAt, fderiv_norm_rpow (0 : E) hp, norm_zero, map_zero, smul_zero]

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (fderiv ℝ fun x => ‖x‖ ^ p) (𝓝 0) (𝓝 0)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ (Differentiable ℝ fun x => ‖x‖ ^ p) ∧ Continuous (fderiv ℝ fun x => ‖x‖ ^ p)

Tactic:
refine ⟨fun x ↦ hasFDerivAt_norm_rpow x hp |>.differentiableAt, ?_⟩

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ Continuous (fderiv ℝ fun x => ‖x‖ ^ p)

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
⊢ ContinuousAt (fun x => (p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x

Tactic:
fun_prop (discharger := simp [hx])

Result:
no goals

Proof state:
case funProp.discharger
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ ‖0‖ ≠ 0 ∨ 0 ≤ p - 1

Tactic:
simp [hp.le]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ ∀ (x : E), ContinuousAt (fderiv ℝ fun x => ‖x‖ ^ p) x

Tactic:
intro x

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
⊢ ContinuousAt (fderiv ℝ fun x => ‖x‖ ^ p) x

Proof state:
case funProp.discharger
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
⊢ ‖x‖ ≠ 0 ∨ 0 ≤ p - 2

Tactic:
simp [hx]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
⊢ ContinuousAt (fderiv ℝ fun x => ‖x‖ ^ p) x

Tactic:
by_cases hx : x = 0

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ ContinuousAt (fderiv ℝ fun x => ‖x‖ ^ p) x

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
⊢ ContinuousAt (fderiv ℝ fun x => ‖x‖ ^ p) x

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (fun x => ‖fderiv ℝ (fun x => ‖x‖ ^ p) x‖) (𝓝 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)

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (fun x => p * ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (fderiv ℝ fun x => ‖x‖ ^ p) (𝓝 0) (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (fun x => ‖fderiv ℝ (fun x => ‖x‖ ^ p) x‖) (𝓝 0) (𝓝 0)