have diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (σ + t * I) := by
  intro σ
  refine differentiableAt_riemannZeta ?_
  contrapose! t_ne_zero; apply And.right; simpa [Complex.ext_iff] using t_ne_zero
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
⊢ ∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I) = ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I) = ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)