Theorem: integral_const_div_sq_add_sq (PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean)

State before:
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
Tactic:
nth_rewrite 1 [← div_mul_cancel₀ x₁ hy, ← div_mul_cancel₀ x₂ hy]
State after:
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

State before:
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
Tactic:
simp_rw [← mul_integral_comp_mul_right, ← integral_const_mul, ← integral_one_div_one_add_sq]
State after:
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)

State before:
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)
Tactic:
exact integral_congr <| λ x _ => by field_simp; ring
State after:
no goals

State before:
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 : ℝ
x✝ : x ∈ [[x₁ / y, x₂ / y]]
⊢ y * (y / ((x * y) ^ 2 + y ^ 2)) = 1 / (1 + x ^ 2)
Tactic:
field_simp
State after:
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 : ℝ
x✝ : x ∈ [[x₁ / y, x₂ / y]]
⊢ y * y * (1 + x ^ 2) = (x * y) ^ 2 + y ^ 2

State before:
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 : ℝ
x✝ : x ∈ [[x₁ / y, x₂ / y]]
⊢ y * y * (1 + x ^ 2) = (x * y) ^ 2 + y ^ 2
Tactic:
ring
State after:
no goals