rw [show f' u = cexp (c * u) * (c * 1) / c by field_simp]
n : ℕ
A a b c✝ d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
u : ℝ
a✝ : u ∈ Ici (-x.log)
⊢ HasDerivAt f (f' u) u
n : ℕ
A a b c✝ d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
u : ℝ
a✝ : u ∈ Ici (-x.log)
⊢ HasDerivAt f (cexp (c * ↑u) * (c * 1) / c) u