Theorem: integral_const_div_re_add_self (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₂ σ : ℝ
hx : x ≠ 0
⊢ ∫ (y : ℝ) in y₁..y₂, A / (↑x + ↑y * I) =
    A / I * (↑(y₂ ^ 2 + (-x) ^ 2).log / 2 - ↑(y₁ ^ 2 + (-x) ^ 2).log / 2) -
      A / I * I * (↑(y₂ / -x).arctan - ↑(y₁ / -x).arctan)
Tactic:
have l1 {y : ℝ} : A / (x + y * I) = A / I / (y + ↑(-x) * I) := by
  have e1 : x + y * I ≠ 0 := by contrapose! hx ; simpa using congr_arg re hx
  have e2 : y + -(x * I) ≠ 0 := by contrapose! hx ; simpa using congr_arg im hx
  field_simp ; ring_nf ; 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₂ σ : ℝ
hx : x ≠ 0
l1 : ∀ {y : ℝ}, A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
⊢ ∫ (y : ℝ) in y₁..y₂, A / (↑x + ↑y * I) =
    A / I * (↑(y₂ ^ 2 + (-x) ^ 2).log / 2 - ↑(y₁ ^ 2 + (-x) ^ 2).log / 2) -
      A / I * I * (↑(y₂ / -x).arctan - ↑(y₁ / -x).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₂ σ : ℝ
hx : x ≠ 0
l1 : ∀ {y : ℝ}, A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
⊢ ∫ (y : ℝ) in y₁..y₂, A / (↑x + ↑y * I) =
    A / I * (↑(y₂ ^ 2 + (-x) ^ 2).log / 2 - ↑(y₁ ^ 2 + (-x) ^ 2).log / 2) -
      A / I * I * (↑(y₂ / -x).arctan - ↑(y₁ / -x).arctan)
Tactic:
have l2 : -x ≠ 0 := by rwa [neg_ne_zero]
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₂ σ : ℝ
hx : x ≠ 0
l1 : ∀ {y : ℝ}, A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
l2 : -x ≠ 0
⊢ ∫ (y : ℝ) in y₁..y₂, A / (↑x + ↑y * I) =
    A / I * (↑(y₂ ^ 2 + (-x) ^ 2).log / 2 - ↑(y₁ ^ 2 + (-x) ^ 2).log / 2) -
      A / I * I * (↑(y₂ / -x).arctan - ↑(y₁ / -x).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₂ σ : ℝ
hx : x ≠ 0
l1 : ∀ {y : ℝ}, A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
l2 : -x ≠ 0
⊢ ∫ (y : ℝ) in y₁..y₂, A / (↑x + ↑y * I) =
    A / I * (↑(y₂ ^ 2 + (-x) ^ 2).log / 2 - ↑(y₁ ^ 2 + (-x) ^ 2).log / 2) -
      A / I * I * (↑(y₂ / -x).arctan - ↑(y₁ / -x).arctan)
Tactic:
simp_rw [l1, integral_const_div_self_add_im l2]
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
⊢ A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
Tactic:
have e1 : x + y * I ≠ 0 := by contrapose! hx ; simpa using congr_arg re hx
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
⊢ A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)

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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
⊢ A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
Tactic:
have e2 : y + -(x * I) ≠ 0 := by contrapose! hx ; simpa using congr_arg im hx
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
e2 : ↑y + -(↑x * I) ≠ 0
⊢ A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)

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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
e2 : ↑y + -(↑x * I) ≠ 0
⊢ A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
e2 : ↑y + -(↑x * I) ≠ 0
⊢ A * (↑y + -(↑x * I)) = -(A * I * (↑x + ↑y * I))

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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
e2 : ↑y + -(↑x * I) ≠ 0
⊢ A * (↑y + -(↑x * I)) = -(A * I * (↑x + ↑y * I))
Tactic:
ring_nf
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
e2 : ↑y + -(↑x * I) ≠ 0
⊢ A * ↑y - A * ↑x * I = -(A * ↑y * I ^ 2) - A * ↑x * I

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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
e2 : ↑y + -(↑x * I) ≠ 0
⊢ A * ↑y - A * ↑x * I = -(A * ↑y * I ^ 2) - A * ↑x * I
Tactic:
simp
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
⊢ ↑x + ↑y * I ≠ 0
Tactic:
contrapose! hx
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₂ σ y : ℝ
hx : ↑x + ↑y * I = 0
⊢ x = 0

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₂ σ y : ℝ
hx : ↑x + ↑y * I = 0
⊢ x = 0
Tactic:
simpa using congr_arg re hx
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₂ σ : ℝ
hx : x ≠ 0
y : ℝ
e1 : ↑x + ↑y * I ≠ 0
⊢ ↑y + -(↑x * I) ≠ 0
Tactic:
contrapose! hx
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₂ σ y : ℝ
e1 : ↑x + ↑y * I ≠ 0
hx : ↑y + -(↑x * I) = 0
⊢ x = 0

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₂ σ y : ℝ
e1 : ↑x + ↑y * I ≠ 0
hx : ↑y + -(↑x * I) = 0
⊢ x = 0
Tactic:
simpa using congr_arg im hx
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₂ σ : ℝ
hx : x ≠ 0
l1 : ∀ {y : ℝ}, A / (↑x + ↑y * I) = A / I / (↑y + ↑(-x) * I)
⊢ -x ≠ 0
Tactic:
rwa [neg_ne_zero]
State after:
no goals