ext σ
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
⊢ (deriv fun {σ₂} => f (↑σ₂ + ↑t * I)) = fun σ => deriv f (↑σ + ↑t * I)
case h
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv f (↑σ + ↑t * I)