case inl
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x

case inr
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : 0 < x
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
x✝ y z x : ℝ
hx : x ≠ 0
p : ℝ
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
cases' hx.lt_or_lt with hx hx
case inl
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt ((fun x => x.fst ^ x.snd) ∘ fun x => (id x, p))
    (↑(((x, p).snd * (x, p).fst ^ ((x, p).snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
          ((x, p).fst ^ (x, p).snd * log (x, p).fst - exp (log (x, p).fst * (x, p).snd) * sin ((x, p).snd * π) * π) •
            ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0))
    x
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
case inl
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
have := (hasStrictFDerivAt_rpow_of_neg (x, p) hx).comp_hasStrictDerivAt x
  ((hasStrictDerivAt_id x).prod (hasStrictDerivAt_const _ _))
case h.e'_7
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt ((fun x => x.fst ^ x.snd) ∘ fun x => (id x, p))
    (↑(((x, p).snd * (x, p).fst ^ ((x, p).snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
          ((x, p).fst ^ (x, p).snd * log (x, p).fst - exp (log (x, p).fst * (x, p).snd) * sin ((x, p).snd * π) * π) •
            ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0))
    x
⊢ p * x ^ (p - 1) =
    ↑(((x, p).snd * (x, p).fst ^ ((x, p).snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
          ((x, p).fst ^ (x, p).snd * log (x, p).fst - exp (log (x, p).fst * (x, p).snd) * sin ((x, p).snd * π) * π) •
            ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0)
case inl
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt ((fun x => x.fst ^ x.snd) ∘ fun x => (id x, p))
    (↑(((x, p).snd * (x, p).fst ^ ((x, p).snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
          ((x, p).fst ^ (x, p).snd * log (x, p).fst - exp (log (x, p).fst * (x, p).snd) * sin ((x, p).snd * π) * π) •
            ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0))
    x
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
convert this using 1
no goals
case h.e'_7
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt ((fun x => x.fst ^ x.snd) ∘ fun x => (id x, p))
    (↑(((x, p).snd * (x, p).fst ^ ((x, p).snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
          ((x, p).fst ^ (x, p).snd * log (x, p).fst - exp (log (x, p).fst * (x, p).snd) * sin ((x, p).snd * π) * π) •
            ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0))
    x
⊢ p * x ^ (p - 1) =
    ↑(((x, p).snd * (x, p).fst ^ ((x, p).snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
          ((x, p).fst ^ (x, p).snd * log (x, p).fst - exp (log (x, p).fst * (x, p).snd) * sin ((x, p).snd * π) * π) •
            ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0)
simp
no goals
case inr
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : 0 < x
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
simpa using (hasStrictDerivAt_id x).rpow (hasStrictDerivAt_const x p) hx