Theorem: integral_const_div_self_add_im (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₂, A / (↑x + ↑y * I) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(x₂ / y).arctan - ↑(x₁ / y).arctan)
Tactic:
have e1 {x : ℝ} : A / (x + y * I) = A * x / (x ^ 2 + y ^ 2) - A * I * y / (x ^ 2 + y ^ 2) := by
  ring_nf ; simp_rw [inv_re_add_im] ; ring
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ ∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * I) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ ∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * I) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(x₂ / y).arctan - ↑(x₁ / y).arctan)
Tactic:
have e2 : IntervalIntegrable (fun x ↦ A * x / (x ^ 2 + y ^ 2)) volume x₁ x₂ := by
  apply Continuous.intervalIntegrable
  simp_rw [mul_div_assoc] ; norm_cast
  exact continuous_const.mul <| continuous_ofReal.comp <| continuous_self_div_sq_add_sq 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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ ∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * I) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ ∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * I) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(x₂ / y).arctan - ↑(x₁ / y).arctan)
Tactic:
have e3 : IntervalIntegrable (fun x ↦ A * I * y / (x ^ 2 + y ^ 2)) volume x₁ x₂ := by
  apply Continuous.intervalIntegrable
  refine continuous_const.div (by continuity) (λ x => ?_)
  norm_cast ; exact sq_add_sq_ne_zero 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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ ∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * I) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ ∫ (x : ℝ) in x₁..x₂, A / (↑x + ↑y * I) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(x₂ / y).arctan - ↑(x₁ / y).arctan)
Tactic:
simp_rw [integral_congr (λ _ _ => e1), integral_sub e2 e3, mul_div_assoc]
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ (∫ (x : ℝ) in x₁..x₂, A * (↑x / (↑x ^ 2 + ↑y ^ 2))) - ∫ (x : ℝ) in x₁..x₂, A * I * (↑y / (↑x ^ 2 + ↑y ^ 2)) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ (∫ (x : ℝ) in x₁..x₂, A * (↑x / (↑x ^ 2 + ↑y ^ 2))) - ∫ (x : ℝ) in x₁..x₂, A * I * (↑y / (↑x ^ 2 + ↑y ^ 2)) =
    A * (↑(x₂ ^ 2 + y ^ 2).log / 2 - ↑(x₁ ^ 2 + y ^ 2).log / 2) - A * I * (↑(x₂ / y).arctan - ↑(x₁ / y).arctan)
Tactic:
norm_cast
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ (∫ (x : ℝ) in x₁..x₂, A * ↑(x / (x ^ 2 + y ^ 2))) - ∫ (x : ℝ) in x₁..x₂, A * I * ↑(y / (x ^ 2 + y ^ 2)) =
    A * ↑((x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2) - A * I * ↑((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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
e3 : IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ (∫ (x : ℝ) in x₁..x₂, A * ↑(x / (x ^ 2 + y ^ 2))) - ∫ (x : ℝ) in x₁..x₂, A * I * ↑(y / (x ^ 2 + y ^ 2)) =
    A * ↑((x₂ ^ 2 + y ^ 2).log / 2 - (x₁ ^ 2 + y ^ 2).log / 2) - A * I * ↑((x₂ / y).arctan - (x₁ / y).arctan)
Tactic:
simp_rw [integral_const_mul, intervalIntegral.integral_ofReal, integral_self_div_sq_add_sq hy,
  integral_const_div_sq_add_sq hy]
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 : ℝ
⊢ A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
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₂ σ : ℝ
hy : y ≠ 0
x : ℝ
⊢ A * (↑x + ↑y * I)⁻¹ = A * ↑x * (↑x ^ 2 + ↑y ^ 2)⁻¹ - A * ↑y * I * (↑x ^ 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 : ℝ
⊢ A * (↑x + ↑y * I)⁻¹ = A * ↑x * (↑x ^ 2 + ↑y ^ 2)⁻¹ - A * ↑y * I * (↑x ^ 2 + ↑y ^ 2)⁻¹
Tactic:
simp_rw [inv_re_add_im]
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 : ℝ
⊢ A * ((↑x - I * ↑y) / (↑x ^ 2 + ↑y ^ 2)) = A * ↑x * (↑x ^ 2 + ↑y ^ 2)⁻¹ - A * ↑y * I * (↑x ^ 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 : ℝ
⊢ A * ((↑x - I * ↑y) / (↑x ^ 2 + ↑y ^ 2)) = A * ↑x * (↑x ^ 2 + ↑y ^ 2)⁻¹ - A * ↑y * I * (↑x ^ 2 + ↑y ^ 2)⁻¹
Tactic:
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
Tactic:
apply Continuous.intervalIntegrable
State after:
case hu
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ Continuous fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)

State before:
case hu
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ Continuous fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)
Tactic:
simp_rw [mul_div_assoc]
State after:
case hu
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ Continuous fun x => A * (↑x / (↑x ^ 2 + ↑y ^ 2))

State before:
case hu
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ Continuous fun x => A * (↑x / (↑x ^ 2 + ↑y ^ 2))
Tactic:
norm_cast
State after:
case hu
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ Continuous fun x => A * ↑(x / (x ^ 2 + y ^ 2))

State before:
case hu
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
⊢ Continuous fun x => A * ↑(x / (x ^ 2 + y ^ 2))
Tactic:
exact continuous_const.mul <| continuous_ofReal.comp <| continuous_self_div_sq_add_sq hy
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ IntervalIntegrable (fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
Tactic:
apply Continuous.intervalIntegrable
State after:
case hu
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ Continuous fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)

State before:
case hu
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ Continuous fun x => A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
Tactic:
refine continuous_const.div (by continuity) (λ x => ?_)
State after:
case hu
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
x : ℝ
⊢ ↑x ^ 2 + ↑y ^ 2 ≠ 0

State before:
case hu
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
x : ℝ
⊢ ↑x ^ 2 + ↑y ^ 2 ≠ 0
Tactic:
norm_cast
State after:
case hu
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
x : ℝ
⊢ ¬x ^ 2 + y ^ 2 = 0

State before:
case hu
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
x : ℝ
⊢ ¬x ^ 2 + y ^ 2 = 0
Tactic:
exact sq_add_sq_ne_zero hy
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
e1 : ∀ {x : ℝ}, A / (↑x + ↑y * I) = A * ↑x / (↑x ^ 2 + ↑y ^ 2) - A * I * ↑y / (↑x ^ 2 + ↑y ^ 2)
e2 : IntervalIntegrable (fun x => A * ↑x / (↑x ^ 2 + ↑y ^ 2)) volume x₁ x₂
⊢ Continuous fun x => ↑x ^ 2 + ↑y ^ 2
Tactic:
continuity
State after:
no goals