[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
[PROOFSTEP]
have A : p.1 ≠ 0 := by intro h; simp [h, lt_irrefl] at hp 
[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
⊢ p.fst ≠ 0
[PROOFSTEP]
intro h
[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
h : p.fst = 0
⊢ False
[PROOFSTEP]
simp [h, lt_irrefl] at hp 
[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
[PROOFSTEP]
have : (fun x : ℂ × ℂ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
  ((isOpen_ne.preimage continuous_fst).eventually_mem A).mono fun p hp => cpow_def_of_ne_zero hp _
[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
[PROOFSTEP]
rw [cpow_sub _ _ A, cpow_one, mul_div_left_comm, mul_smul, mul_smul]
[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    (p.fst ^ p.snd • (p.snd / p.fst) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      p.fst ^ p.snd • log p.fst • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
[PROOFSTEP]
refine' HasStrictFDerivAt.congr_of_eventuallyEq _ this.symm
[GOAL]
p : ℂ × ℂ
hp : 0 < p.fst.re ∨ p.fst.im ≠ 0
A : p.fst ≠ 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => exp (log x.fst * x.snd))
    (p.fst ^ p.snd • (p.snd / p.fst) • ContinuousLinearMap.fst ℂ ℂ ℂ +
      p.fst ^ p.snd • log p.fst • ContinuousLinearMap.snd ℂ ℂ ℂ)
    p
[PROOFSTEP]
simpa only [cpow_def_of_ne_zero A, div_eq_mul_inv, mul_smul, add_comm, smul_add] using
  ((hasStrictFDerivAt_fst.clog hp).mul hasStrictFDerivAt_snd).cexp
[GOAL]
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
⊢ HasStrictDerivAt (fun y => x ^ y) (x ^ y * log x) y
[PROOFSTEP]
rcases em (x = 0) with (rfl | hx)
[GOAL]
case inl
y : ℂ
h : 0 ≠ 0 ∨ y ≠ 0
⊢ HasStrictDerivAt (fun y => 0 ^ y) (0 ^ y * log 0) y
[PROOFSTEP]
replace h := h.neg_resolve_left rfl
[GOAL]
case inl
y : ℂ
h : y ≠ 0
⊢ HasStrictDerivAt (fun y => 0 ^ y) (0 ^ y * log 0) y
[PROOFSTEP]
rw [log_zero, mul_zero]
[GOAL]
case inl
y : ℂ
h : y ≠ 0
⊢ HasStrictDerivAt (fun y => 0 ^ y) 0 y
[PROOFSTEP]
refine' (hasStrictDerivAt_const _ 0).congr_of_eventuallyEq _
[GOAL]
case inl
y : ℂ
h : y ≠ 0
⊢ (fun x => 0) =ᶠ[𝓝 y] fun y => 0 ^ y
[PROOFSTEP]
exact (isOpen_ne.eventually_mem h).mono fun y hy => (zero_cpow hy).symm
[GOAL]
case inr
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ HasStrictDerivAt (fun y => x ^ y) (x ^ y * log x) y
[PROOFSTEP]
simpa only [cpow_def_of_ne_zero hx, mul_one] using ((hasStrictDerivAt_id y).const_mul (log x)).cexp
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
f' g' : E →L[ℂ] ℂ
x : E
s : Set E
c : ℂ
hf : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
h0 : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasStrictFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x
[PROOFSTEP]
convert (@hasStrictFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp x (hf.prod hg)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
f' g' : E →L[ℂ] ℂ
x : E
s : Set E
c : ℂ
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
h0 : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x
[PROOFSTEP]
convert (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp x (hf.prod hg)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
f' g' : E →L[ℂ] ℂ
x : E
s : Set E
c : ℂ
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
h0 : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasFDerivWithinAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') s x
[PROOFSTEP]
convert (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp_hasFDerivWithinAt x (hf.prod hg)
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x c : ℂ
⊢ ↑((g x * f x ^ (g x - 1)) • ContinuousLinearMap.smulRight 1 f' +
          (f x ^ g x * log (f x)) • ContinuousLinearMap.smulRight 1 g')
      1 =
    g x * f x ^ (g x - 1) * f' + f x ^ g x * log (f x) * g'
[PROOFSTEP]
simp only [Algebra.id.smul_eq_mul, one_mul, ContinuousLinearMap.one_apply, ContinuousLinearMap.smulRight_apply,
  ContinuousLinearMap.add_apply, Pi.smul_apply, ContinuousLinearMap.coe_smul']
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x c : ℂ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h0 : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasStrictDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
[PROOFSTEP]
simpa using (hf.cpow hg h0).hasStrictDerivAt
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x c : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ HasStrictDerivAt (fun z => z ^ c) (c * x ^ (c - 1)) x
[PROOFSTEP]
simpa only [mul_zero, add_zero, mul_one] using (hasStrictDerivAt_id x).cpow (hasStrictDerivAt_const x c) h
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x c : ℂ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h0 : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
[PROOFSTEP]
simpa only [aux] using (hf.hasFDerivAt.cpow hg h0).hasDerivAt
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x c : ℂ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h0 : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivWithinAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x
[PROOFSTEP]
simpa only [aux] using (hf.hasFDerivWithinAt.cpow hg h0).hasDerivWithinAt
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ -1
⊢ HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
[PROOFSTEP]
rw [Ne.def, ← add_eq_zero_iff_eq_neg, ← Ne.def] at hr 
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
⊢ HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
[PROOFSTEP]
rcases lt_or_gt_of_ne hx.symm with (hx | hx)
[GOAL]
case inl
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
[PROOFSTEP]
apply HasDerivAt.comp_ofReal (e := fun y => (y : ℂ) ^ (r + 1) / (r + 1))
[GOAL]
case inl
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y => y ^ (r + 1) / (r + 1)) (↑x ^ r) ↑x
[PROOFSTEP]
convert HasDerivAt.div_const (𝕜 := ℂ) ?_ (r + 1) using 1
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ↑x ^ r = ?inl.convert_3 / (r + 1)
[PROOFSTEP]
exact (mul_div_cancel _ hr).symm
[GOAL]
case inl.convert_4
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y => y ^ (r + 1)) (↑x ^ r * (r + 1)) ↑x
[PROOFSTEP]
convert HasDerivAt.cpow_const ?_ ?_ using 1
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ↑x ^ r * (r + 1) = (r + 1) * ↑x ^ (r + 1 - 1) * ?inl.convert_4.convert_2
[PROOFSTEP]
rw [add_sub_cancel, mul_comm]
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ (r + 1) * ↑x ^ r = (r + 1) * ↑x ^ r * ?inl.convert_4.convert_2
case inl.convert_4.convert_2
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ℂ
case inl.convert_4.convert_2 f g : ℂ → ℂ s : Set ℂ f' g' x✝ c : ℂ x : ℝ hx✝ : x ≠ 0 r : ℂ hr : r + 1 ≠ 0 hx : 0 < x ⊢ ℂ
[PROOFSTEP]
exact (mul_one _).symm
[GOAL]
case inl.convert_4.convert_5
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y => y) 1 ↑x
[PROOFSTEP]
exact hasDerivAt_id (x : ℂ)
[GOAL]
case inl.convert_4.convert_6
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ 0 < (↑x).re ∨ (↑x).im ≠ 0
[PROOFSTEP]
simp [hx]
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
⊢ HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
[PROOFSTEP]
have : ∀ᶠ y : ℝ in nhds x, (y : ℂ) ^ (r + 1) / (r + 1) = (-y : ℂ) ^ (r + 1) * exp (π * I * (r + 1)) / (r + 1) :=
  by
  refine' Filter.eventually_of_mem (Iio_mem_nhds hx) fun y hy => _
  rw [ofReal_cpow_of_nonpos (le_of_lt hy)]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
⊢ ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
[PROOFSTEP]
refine' Filter.eventually_of_mem (Iio_mem_nhds hx) fun y hy => _
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
y : ℝ
hy : y ∈ Set.Iio 0
⊢ ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
[PROOFSTEP]
rw [ofReal_cpow_of_nonpos (le_of_lt hy)]
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
[PROOFSTEP]
refine' HasDerivAt.congr_of_eventuallyEq _ this
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun x => (-↑x) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)) (↑x ^ r) x
[PROOFSTEP]
rw [ofReal_cpow_of_nonpos (le_of_lt hx)]
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun x => (-↑x) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)) ((-↑x) ^ r * exp (↑π * I * r)) x
[PROOFSTEP]
suffices HasDerivAt (fun y : ℝ => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
  by
  convert this.div_const (r + 1) using 1
  conv_rhs => rw [mul_assoc, mul_comm, mul_div_cancel _ hr]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
⊢ HasDerivAt (fun x => (-↑x) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)) ((-↑x) ^ r * exp (↑π * I * r)) x
[PROOFSTEP]
convert this.div_const (r + 1) using 1
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
⊢ (-↑x) ^ r * exp (↑π * I * r) = (r + 1) * (-↑x) ^ r * exp (↑π * I * r) / (r + 1)
[PROOFSTEP]
conv_rhs => rw [mul_assoc, mul_comm, mul_div_cancel _ hr]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
| (r + 1) * (-↑x) ^ r * exp (↑π * I * r) / (r + 1)
[PROOFSTEP]
rw [mul_assoc, mul_comm, mul_div_cancel _ hr]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
| (r + 1) * (-↑x) ^ r * exp (↑π * I * r) / (r + 1)
[PROOFSTEP]
rw [mul_assoc, mul_comm, mul_div_cancel _ hr]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
| (r + 1) * (-↑x) ^ r * exp (↑π * I * r) / (r + 1)
[PROOFSTEP]
rw [mul_assoc, mul_comm, mul_div_cancel _ hr]
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
[PROOFSTEP]
rw [mul_add ((π : ℂ) * _), mul_one, exp_add, exp_pi_mul_I, mul_comm (_ : ℂ) (-1 : ℂ), neg_one_mul]
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => (-↑y) ^ (r + 1) * -exp (↑π * I * r)) ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x
[PROOFSTEP]
simp_rw [mul_neg, ← neg_mul, ← ofReal_neg]
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => -↑(-y) ^ (r + 1) * exp (↑π * I * r)) ((r + 1) * ↑(-x) ^ r * exp (↑π * I * r)) x
[PROOFSTEP]
suffices HasDerivAt (fun y : ℝ => ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x by convert this.neg.mul_const _ using 1;
  ring
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x
⊢ HasDerivAt (fun y => -↑(-y) ^ (r + 1) * exp (↑π * I * r)) ((r + 1) * ↑(-x) ^ r * exp (↑π * I * r)) x
[PROOFSTEP]
convert this.neg.mul_const _ using 1
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x
⊢ (r + 1) * ↑(-x) ^ r * exp (↑π * I * r) = -(-(r + 1) * ↑(-x) ^ r) * exp (↑π * I * r)
[PROOFSTEP]
ring
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x
[PROOFSTEP]
suffices HasDerivAt (fun y : ℝ => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
  by
  convert @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1
  rw [real_smul, ofReal_neg 1, ofReal_one]; ring
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ HasDerivAt (fun y => ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x
[PROOFSTEP]
convert @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ -(r + 1) * ↑(-x) ^ r = -1 • ((r + 1) * ↑(-x) ^ r)
[PROOFSTEP]
rw [real_smul, ofReal_neg 1, ofReal_one]
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ -(r + 1) * ↑(-x) ^ r = -1 * ((r + 1) * ↑(-x) ^ r)
[PROOFSTEP]
ring
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
[PROOFSTEP]
suffices HasDerivAt (fun y : ℂ => y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x) by exact this.comp_ofReal
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y => y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x)
⊢ HasDerivAt (fun y => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
[PROOFSTEP]
exact this.comp_ofReal
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x)
[PROOFSTEP]
conv in ↑_ ^ _ => rw [(by ring : r = r + 1 - 1)]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
y : ℂ
| y ^ (r + 1)
[PROOFSTEP]
rw [(by ring : r = r + 1 - 1)]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
y : ℂ
| y ^ (r + 1)
[PROOFSTEP]
rw [(by ring : r = r + 1 - 1)]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
y : ℂ
| y ^ (r + 1)
[PROOFSTEP]
rw [(by ring : r = r + 1 - 1)]
[GOAL]
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
y : ℂ
⊢ r = r + 1 - 1
[PROOFSTEP]
ring
[GOAL]
case inr
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => y ^ (r + 1 - 1 + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x)
[PROOFSTEP]
convert HasDerivAt.cpow_const ?_ ?_ using 1
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ (r + 1) * ↑(-x) ^ r = (r + 1 - 1 + 1) * ↑(-x) ^ (r + 1 - 1 + 1 - 1) * ?inr.convert_2
[PROOFSTEP]
rw [add_sub_cancel, add_sub_cancel]
[GOAL]
case h.e'_7
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ (r + 1) * ↑(-x) ^ r = (r + 1) * ↑(-x) ^ r * ?inr.convert_2
case inr.convert_2
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ ℂ
case inr.convert_2
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ ℂ
[PROOFSTEP]
exact (mul_one _).symm
[GOAL]
case inr.convert_5
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y => y) 1 ↑(-x)
[PROOFSTEP]
exact hasDerivAt_id ((-x : ℝ) : ℂ)
[GOAL]
case inr.convert_6
f g : ℂ → ℂ
s : Set ℂ
f' g' x✝ c : ℂ
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 > x
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)) / (r + 1)
⊢ 0 < (↑(-x)).re ∨ (↑(-x)).im ≠ 0
[PROOFSTEP]
simp [hx]
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
[PROOFSTEP]
have : (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
  (continuousAt_fst.eventually (lt_mem_nhds hp)).mono fun p hp => rpow_def_of_pos hp _
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
[PROOFSTEP]
refine' HasStrictFDerivAt.congr_of_eventuallyEq _ this.symm
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ HasStrictFDerivAt (fun x => exp (log x.fst * x.snd))
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
[PROOFSTEP]
convert ((hasStrictFDerivAt_fst.log hp.ne').mul hasStrictFDerivAt_snd).exp using 1
[GOAL]
case h.e'_10
x y z : ℝ
p : ℝ × ℝ
hp : 0 < p.fst
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
⊢ (p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    exp (log p.fst * p.snd) •
      (log p.fst • ContinuousLinearMap.snd ℝ ℝ ℝ + p.snd • p.fst⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ)
[PROOFSTEP]
rw [rpow_sub_one hp.ne', ← rpow_def_of_pos hp, smul_add, smul_smul, mul_div_left_comm, div_eq_mul_inv, smul_smul,
  smul_smul, mul_assoc, add_comm]
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
[PROOFSTEP]
have : (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) * cos (x.2 * π) :=
  (continuousAt_fst.eventually (gt_mem_nhds hp)).mono fun p hp => rpow_def_of_neg hp _
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
⊢ HasStrictFDerivAt (fun x => x.fst ^ x.snd)
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
[PROOFSTEP]
refine' HasStrictFDerivAt.congr_of_eventuallyEq _ this.symm
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
⊢ HasStrictFDerivAt (fun x => exp (log x.fst * x.snd) * cos (x.snd * π))
    ((p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ)
    p
[PROOFSTEP]
convert
  ((hasStrictFDerivAt_fst.log hp.ne).mul hasStrictFDerivAt_snd).exp.mul (hasStrictFDerivAt_snd.mul_const π).cos using 1
[GOAL]
case h.e'_10.h.h
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : NormedField.toNormedSpace = NormedAlgebra.toNormedSpace'
⊢ (p.snd * p.fst ^ (p.snd - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    exp (log p.fst * p.snd) • -sin (p.snd * π) • π • ContinuousLinearMap.snd ℝ ℝ ℝ +
      cos (p.snd * π) •
        exp (log p.fst * p.snd) •
          (log p.fst • ContinuousLinearMap.snd ℝ ℝ ℝ + p.snd • p.fst⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ)
[PROOFSTEP]
simp_rw [rpow_sub_one hp.ne, smul_add, ← add_assoc, smul_smul, ← add_smul, ← mul_assoc, mul_comm (cos _), ←
  rpow_def_of_neg hp]
[GOAL]
case h.e'_10.h.h
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : NormedField.toNormedSpace = NormedAlgebra.toNormedSpace'
⊢ (p.snd * (p.fst ^ p.snd / p.fst)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    (exp (log p.fst * p.snd) * -sin (p.snd * π) * π + p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ +
      (p.fst ^ p.snd * p.snd * p.fst⁻¹) • ContinuousLinearMap.fst ℝ ℝ ℝ
[PROOFSTEP]
rw [div_eq_mul_inv, add_comm]
[GOAL]
case h.e'_10.h.h
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : NormedField.toNormedSpace = NormedAlgebra.toNormedSpace'
⊢ (p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ +
      (p.snd * (p.fst ^ p.snd * p.fst⁻¹)) • ContinuousLinearMap.fst ℝ ℝ ℝ =
    (exp (log p.fst * p.snd) * -sin (p.snd * π) * π + p.fst ^ p.snd * log p.fst) • ContinuousLinearMap.snd ℝ ℝ ℝ +
      (p.fst ^ p.snd * p.snd * p.fst⁻¹) • ContinuousLinearMap.fst ℝ ℝ ℝ
[PROOFSTEP]
congr 2
[GOAL]
case h.e'_10.h.h.e_a.e_a
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : NormedField.toNormedSpace = NormedAlgebra.toNormedSpace'
⊢ p.fst ^ p.snd * log p.fst - exp (log p.fst * p.snd) * sin (p.snd * π) * π =
    exp (log p.fst * p.snd) * -sin (p.snd * π) * π + p.fst ^ p.snd * log p.fst
[PROOFSTEP]
ring
[GOAL]
case h.e'_10.h.h.e_a.e_a
x y z : ℝ
p : ℝ × ℝ
hp : p.fst < 0
this : (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : NormedField.toNormedSpace = NormedAlgebra.toNormedSpace'
⊢ p.snd * (p.fst ^ p.snd * p.fst⁻¹) = p.fst ^ p.snd * p.snd * p.fst⁻¹
[PROOFSTEP]
ring
[GOAL]
x y z : ℝ
p : ℝ × ℝ
hp : p.fst ≠ 0
n : ℕ∞
⊢ ContDiffAt ℝ n (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
cases' hp.lt_or_lt with hneg hpos
[GOAL]
case inl
x y z : ℝ
p : ℝ × ℝ
hp : p.fst ≠ 0
n : ℕ∞
hneg : p.fst < 0
⊢ ContDiffAt ℝ n (fun p => p.fst ^ p.snd) p
case inr x y z : ℝ p : ℝ × ℝ hp : p.fst ≠ 0 n : ℕ∞ hpos : 0 < p.fst ⊢ ContDiffAt ℝ n (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
exacts
  [(((contDiffAt_fst.log hneg.ne).mul contDiffAt_snd).exp.mul
        (contDiffAt_snd.mul contDiffAt_const).cos).congr_of_eventuallyEq
    ((continuousAt_fst.eventually (gt_mem_nhds hneg)).mono fun p hp => rpow_def_of_neg hp _),
  ((contDiffAt_fst.log hpos.ne').mul contDiffAt_snd).exp.congr_of_eventuallyEq
    ((continuousAt_fst.eventually (lt_mem_nhds hpos)).mono fun p hp => rpow_def_of_pos hp _)]
[GOAL]
x y z : ℝ
f g : ℝ → ℝ
f' g' : ℝ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h : 0 < f x
⊢ HasStrictDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x)) x
[PROOFSTEP]
convert (hasStrictFDerivAt_rpow_of_pos ((fun x => (f x, g x)) x) h).comp_hasStrictDerivAt x (hf.prod hg) using 1
[GOAL]
case h.e'_7
x y z : ℝ
f g : ℝ → ℝ
f' g' : ℝ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x) =
    ↑((((fun x => (f x, g x)) x).snd * ((fun x => (f x, g x)) x).fst ^ (((fun x => (f x, g x)) x).snd - 1)) •
            ContinuousLinearMap.fst ℝ ℝ ℝ +
          (((fun x => (f x, g x)) x).fst ^ ((fun x => (f x, g x)) x).snd * log ((fun x => (f x, g x)) x).fst) •
            ContinuousLinearMap.snd ℝ ℝ ℝ)
      (f', g')
[PROOFSTEP]
simp [mul_assoc, mul_comm, mul_left_comm]
[GOAL]
x✝ y z x : ℝ
hx : x ≠ 0
p : ℝ
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
[PROOFSTEP]
cases' hx.lt_or_lt with hx hx
[GOAL]
case inl
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
[PROOFSTEP]
have :=
  (hasStrictFDerivAt_rpow_of_neg (x, p) hx).comp_hasStrictDerivAt x
    ((hasStrictDerivAt_id x).prod (hasStrictDerivAt_const _ _))
[GOAL]
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
[PROOFSTEP]
convert this using 1
[GOAL]
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)
[PROOFSTEP]
simp
[GOAL]
case inr
x✝ y z x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : 0 < x
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
[PROOFSTEP]
simpa using (hasStrictDerivAt_id x).rpow (hasStrictDerivAt_const x p) hx
[GOAL]
x✝ y z a : ℝ
ha : 0 < a
x : ℝ
⊢ HasStrictDerivAt (fun x => a ^ x) (a ^ x * log a) x
[PROOFSTEP]
simpa using (hasStrictDerivAt_const _ _).rpow (hasStrictDerivAt_id x) ha
[GOAL]
x✝ y z a x : ℝ
ha : a < 0
⊢ HasStrictDerivAt (fun x => a ^ x) (a ^ x * log a - exp (log a * x) * sin (x * π) * π) x
[PROOFSTEP]
simpa using
  (hasStrictFDerivAt_rpow_of_neg (a, x) ha).comp_hasStrictDerivAt x
    ((hasStrictDerivAt_const _ _).prod (hasStrictDerivAt_id _))
[GOAL]
z x✝ y x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
[PROOFSTEP]
rcases ne_or_eq x 0 with (hx | rfl)
[GOAL]
case inl
z x✝ y x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
hx : x ≠ 0
⊢ HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
[PROOFSTEP]
exact (hasStrictDerivAt_rpow_const_of_ne hx _).hasDerivAt
[GOAL]
case inr
z x y p : ℝ
h : 0 ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun x => x ^ p) (p * 0 ^ (p - 1)) 0
[PROOFSTEP]
replace h : 1 ≤ p := h.neg_resolve_left rfl
[GOAL]
case inr
z x y p : ℝ
h : 1 ≤ p
⊢ HasDerivAt (fun x => x ^ p) (p * 0 ^ (p - 1)) 0
[PROOFSTEP]
apply hasDerivAt_of_hasDerivAt_of_ne fun x hx => (hasStrictDerivAt_rpow_const_of_ne hx p).hasDerivAt
[GOAL]
case inr.hf
z x y p : ℝ
h : 1 ≤ p
⊢ ContinuousAt (fun x => x ^ p) 0
case inr.hg z x y p : ℝ h : 1 ≤ p ⊢ ContinuousAt (fun x => p * x ^ (p - 1)) 0
[PROOFSTEP]
exacts [continuousAt_id.rpow_const (Or.inr (zero_le_one.trans h)),
  continuousAt_const.mul (continuousAt_id.rpow_const (Or.inr (sub_nonneg.2 h)))]
[GOAL]
z x y p : ℝ
n : ℕ
h : ↑n ≤ p
⊢ ContDiff ℝ ↑n fun x => x ^ p
[PROOFSTEP]
induction' n with n ihn generalizing p
[GOAL]
case zero
z x y p✝ : ℝ
n : ℕ
h✝ : ↑n ≤ p✝
p : ℝ
h : ↑Nat.zero ≤ p
⊢ ContDiff ℝ ↑Nat.zero fun x => x ^ p
[PROOFSTEP]
exact contDiff_zero.2 (continuous_id.rpow_const fun x => Or.inr <| by simpa using h)
[GOAL]
z x✝ y p✝ : ℝ
n : ℕ
h✝ : ↑n ≤ p✝
p : ℝ
h : ↑Nat.zero ≤ p
x : ℝ
⊢ 0 ≤ p
[PROOFSTEP]
simpa using h
[GOAL]
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(Nat.succ n) ≤ p
⊢ ContDiff ℝ ↑(Nat.succ n) fun x => x ^ p
[PROOFSTEP]
have h1 : 1 ≤ p := le_trans (by simp) h
[GOAL]
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(Nat.succ n) ≤ p
⊢ 1 ≤ ↑(Nat.succ n)
[PROOFSTEP]
simp
[GOAL]
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑(Nat.succ n) ≤ p
h1 : 1 ≤ p
⊢ ContDiff ℝ ↑(Nat.succ n) fun x => x ^ p
[PROOFSTEP]
rw [Nat.cast_succ, ← le_sub_iff_add_le] at h 
[GOAL]
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ ContDiff ℝ ↑(Nat.succ n) fun x => x ^ p
[PROOFSTEP]
rw [contDiff_succ_iff_deriv, deriv_rpow_const' h1]
[GOAL]
case succ
z x y p✝ : ℝ
n✝ : ℕ
h✝ : ↑n✝ ≤ p✝
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ fun x => x ^ p) ∧ ContDiff ℝ ↑n fun x => p * x ^ (p - 1)
[PROOFSTEP]
refine' ⟨differentiable_rpow_const h1, contDiff_const.mul (ihn h)⟩
[GOAL]
z x✝ y x p : ℝ
hx : x ≠ 0 ∨ 1 ≤ p
⊢ x ≠ 0 ∨ ↑One.one ≤ p
[PROOFSTEP]
rwa [← Nat.cast_one] at hx 
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
f' g' : E →L[ℝ] ℝ
x : E
s : Set E
c p : ℝ
n : ℕ∞
m : ℕ
hf : ContDiffAt ℝ (↑m) f x
h : ↑m ≤ p
⊢ ContDiffAt ℝ (↑m) (fun x => f x ^ p) x
[PROOFSTEP]
rw [← contDiffWithinAt_univ] at *
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
f' g' : E →L[ℝ] ℝ
x : E
s : Set E
c p : ℝ
n : ℕ∞
m : ℕ
hf : ContDiffWithinAt ℝ (↑m) f Set.univ x
h : ↑m ≤ p
⊢ ContDiffWithinAt ℝ (↑m) (fun x => f x ^ p) Set.univ x
[PROOFSTEP]
exact hf.rpow_const_of_le h
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) s x
[PROOFSTEP]
convert (hf.hasFDerivWithinAt.rpow hg.hasFDerivWithinAt h).hasDerivWithinAt using 1
[GOAL]
case h.e'_7
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    ↑((g x * f x ^ (g x - 1)) • ContinuousLinearMap.smulRight 1 f' +
          (f x ^ g x * Real.log (f x)) • ContinuousLinearMap.smulRight 1 g')
      1
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_7
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    g x * f x ^ (g x - 1) * (1 * f') + f x ^ g x * Real.log (f x) * (1 * g')
[PROOFSTEP]
ring
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h : 0 < f x
⊢ HasDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x
[PROOFSTEP]
rw [← hasDerivWithinAt_univ] at *
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' Set.univ x
hg : HasDerivWithinAt g g' Set.univ x
h : 0 < f x
⊢ HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) Set.univ x
[PROOFSTEP]
exact hf.rpow hg h
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) s x
[PROOFSTEP]
convert (hasDerivAt_rpow_const hx).comp_hasDerivWithinAt x hf using 1
[GOAL]
case h.e'_7
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ f' * p * f x ^ (p - 1) = p * f x ^ (p - 1) * f'
[PROOFSTEP]
ring
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) x
[PROOFSTEP]
rw [← hasDerivWithinAt_univ] at *
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) Set.univ x
[PROOFSTEP]
exact hf.rpow_const hx
[GOAL]
f g : ℝ → ℝ
f' g' x y p✝ : ℝ
s : Set ℝ
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =Θ[atTop] fun x => x ^ (p - 1)
[PROOFSTEP]
calc
  deriv (fun (x : ℝ) => x ^ p) =ᶠ[atTop] fun x => p * x ^ (p - 1) :=
    by
    filter_upwards [eventually_ne_atTop 0] with x hx
    rw [Real.deriv_rpow_const (Or.inl hx)]
  _ =Θ[atTop] fun x => x ^ (p - 1) := Asymptotics.IsTheta.const_mul_left hp Asymptotics.isTheta_rfl
[GOAL]
f g : ℝ → ℝ
f' g' x y p✝ : ℝ
s : Set ℝ
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =ᶠ[atTop] fun x => p * x ^ (p - 1)
[PROOFSTEP]
filter_upwards [eventually_ne_atTop 0] with x hx
[GOAL]
case h
f g : ℝ → ℝ
f' g' x✝ y p✝ : ℝ
s : Set ℝ
p : ℝ
hp : p ≠ 0
x : ℝ
hx : x ≠ 0
⊢ deriv (fun x => x ^ p) x = p * x ^ (p - 1)
[PROOFSTEP]
rw [Real.deriv_rpow_const (Or.inl hx)]
[GOAL]
f g : ℝ → ℝ
f' g' x y p✝ : ℝ
s : Set ℝ
p : ℝ
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)
[PROOFSTEP]
rcases eq_or_ne p 0 with rfl | hp
[GOAL]
case inl
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
⊢ (deriv fun x => x ^ 0) =O[atTop] fun x => x ^ (0 - 1)
case inr f g : ℝ → ℝ f' g' x y p✝ : ℝ s : Set ℝ p : ℝ hp : p ≠ 0 ⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)
[PROOFSTEP]
case inl => simp [zero_sub, Real.rpow_neg_one, Real.rpow_zero, deriv_const', Asymptotics.isBigO_zero]
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
⊢ (deriv fun x => x ^ 0) =O[atTop] fun x => x ^ (0 - 1)
[PROOFSTEP]
case inl => simp [zero_sub, Real.rpow_neg_one, Real.rpow_zero, deriv_const', Asymptotics.isBigO_zero]
[GOAL]
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
⊢ (deriv fun x => x ^ 0) =O[atTop] fun x => x ^ (0 - 1)
[PROOFSTEP]
simp [zero_sub, Real.rpow_neg_one, Real.rpow_zero, deriv_const', Asymptotics.isBigO_zero]
[GOAL]
case inr
f g : ℝ → ℝ
f' g' x y p✝ : ℝ
s : Set ℝ
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)
[PROOFSTEP]
case inr => exact (isTheta_deriv_rpow_const_atTop hp).1
[GOAL]
f g : ℝ → ℝ
f' g' x y p✝ : ℝ
s : Set ℝ
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)
[PROOFSTEP]
case inr => exact (isTheta_deriv_rpow_const_atTop hp).1
[GOAL]
f g : ℝ → ℝ
f' g' x y p✝ : ℝ
s : Set ℝ
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)
[PROOFSTEP]
exact (isTheta_deriv_rpow_const_atTop hp).1
[GOAL]
t : ℝ
⊢ Tendsto (fun x => (1 + t / x) ^ x) atTop (𝓝 (exp t))
[PROOFSTEP]
apply ((Real.continuous_exp.tendsto _).comp (tendsto_mul_log_one_plus_div_atTop t)).congr' _
[GOAL]
t : ℝ
⊢ (exp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
[PROOFSTEP]
have h₁ : (1 : ℝ) / 2 < 1 := by linarith
[GOAL]
t : ℝ
⊢ 1 / 2 < 1
[PROOFSTEP]
linarith
[GOAL]
t : ℝ
h₁ : 1 / 2 < 1
⊢ (exp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
[PROOFSTEP]
have h₂ : Tendsto (fun x : ℝ => 1 + t / x) atTop (𝓝 1) := by
  simpa using (tendsto_inv_atTop_zero.const_mul t).const_add 1
[GOAL]
t : ℝ
h₁ : 1 / 2 < 1
⊢ Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
[PROOFSTEP]
simpa using (tendsto_inv_atTop_zero.const_mul t).const_add 1
[GOAL]
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
⊢ (exp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
[PROOFSTEP]
refine' (eventually_ge_of_tendsto_gt h₁ h₂).mono fun x hx => _
[GOAL]
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
⊢ (exp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x
[PROOFSTEP]
have hx' : 0 < 1 + t / x := by linarith
[GOAL]
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
⊢ 0 < 1 + t / x
[PROOFSTEP]
linarith
[GOAL]
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
hx' : 0 < 1 + t / x
⊢ (exp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x
[PROOFSTEP]
simp [mul_comm x, exp_mul, exp_log hx']
[GOAL]
t : ℝ
⊢ ∀ (x : ℕ), ((fun x => (1 + t / x) ^ x) ∘ Nat.cast) x = (1 + t / ↑x) ^ ↑x
[PROOFSTEP]
simp
