integral_const_div_self_add_im

lemma integral_const_div_self_add_im (hy : y ≠ 0) :    ∫ x : ℝ in x₁..x₂, A / (x + y * I) =    A * (Real.log (x₂ ^ 2 + y ^ 2) / 2 - Real.log (x₁ ^ 2 + y ^ 2) / 2) -    A * I * (arctan (x₂ / y) - arctan (x₁ / y)) := by  have e1 {x : ℝ} : A / (x + y * I) = A * x / (x ^ 2 + y ^ 2) - A * I * y / (x ^ 2 + y ^ 2) := by    ring_nf    simp_rw [inv_re_add_im]    ring  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))  have e3 : IntervalIntegrable (fun x ↦ A * I * y / (x ^ 2 + y ^ 2)) volume x₁ x₂ := by    apply Continuous.intervalIntegrable    refine continuous_const.div (by fun_prop) (fun x => ?_)    norm_cast    exact sq_add_sq_ne_zero hy  simp_rw [integral_congr (fun _ _ => e1), integral_sub e2 e3, mul_div_assoc]  norm_cast  simp_rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_ofReal,    integral_self_div_sq_add_sq hy, integral_const_div_sq_add_sq hy]