replace hx : x ≠ 1 := by
  contrapose! hx
  simp only [hx, mem_image, Complex.ext_iff, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im,
    I_im, mul_one, sub_self, add_zero, one_re, add_im, mul_im, zero_add, one_im, not_exists,
    not_and]
  exact fun _ _ _ ↦ t_ne_zero
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
⊢ DifferentiableAt ℂ (deriv ζ) x
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
⊢ DifferentiableAt ℂ (deriv ζ) x