let f (x : ℝ) : ℝ := Real.log (x ^ 2 + y ^ 2) / 2
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₂, x / (x ^ 2 + y ^ 2) = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2
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
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
⊢ ∫ (x : ℝ) in x₁..x₂, x / (x ^ 2 + y ^ 2) = (x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2