exact integral_congr <| λ x _ => by field_simp; ring
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..x₂ / y, y * (y / ((x * y) ^ 2 + y ^ 2)) = ∫ (x : ℝ) in x₁ / y..x₂ / y, 1 / (1 + x ^ 2)
no goals