nth_rewrite 1 [← div_mul_cancel₀ x₁ hy, ← div_mul_cancel₀ x₂ 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
⊢ ∫ (x : ℝ) in x₁..x₂, y / (x ^ 2 + y ^ 2) = (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
⊢ ∫ (x : ℝ) in x₁ / y * y..x₂ / y * y, y / (x ^ 2 + y ^ 2) = (x₂ / y).arctan - (x₁ / y).arctan