apply DifferentiableAt.add_const <| differentiableAt_ofReal σ
case h.refine_1
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
⊢ DifferentiableAt ℝ (fun σ => ↑σ + ↑t * I) σ
no goals