have e2 : IntervalIntegrable (fun x ↦ A * x / (x ^ 2 + y ^ 2)) volume x₁ x₂ := by
  apply Continuous.intervalIntegrable
  simp_rw [mul_div_assoc] ; norm_cast
  exact continuous_const.mul <| continuous_ofReal.comp <| continuous_self_div_sq_add_sq hy
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ ∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * I) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(x₂ / y).arctan - ↑(x₁ / y).arctan)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ ∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * I) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(x₂ / y).arctan - ↑(x₁ / y).arctan)