Theorem: Real.differentiableAt_cpow_const_of_ne (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℝ (fun x => ↑x ^ s) x
Tactic:
apply DifferentiableAt.comp_ofReal (e := fun z ↦ z ^ s)
State after:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℂ (fun z => z ^ s) ↑x

State before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℂ (fun z => z ^ s) ↑x
Tactic:
apply DifferentiableAt.cpow (by simp) (by simp) (by simp [xpos])
State after:
no goals

State before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℂ (fun x => x) ↑x
Tactic:
simp
State after:
no goals

State before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℂ (fun x => s) ↑x
Tactic:
simp
State after:
no goals

State before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ ↑x ∈ slitPlane
Tactic:
simp [xpos]
State after:
no goals