simp_rw [integral_congr (λ _ _ => e1), integral_sub e2 e3, mul_div_assoc]
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₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑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)
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₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ (∫ (x : ℝ) in x₁..x₂, A * (↑x / (↑x ^ 2 + ↑y ^ 2))) - ∫ (x : ℝ) in x₁..x₂, A * I * (↑y / (↑x ^ 2 + ↑y ^ 2)) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(x₂ / y).arctan - ↑(x₁ / y).arctan)