Theorem: ResidueTheoremAtOrigin' (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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
⊢ RectangleIntegral (fun s => c / s) z w = 2 * I * ↑π * c
Tactic:
simp only [RectangleIntegral, HIntegral, VIntegral, smul_eq_mul]
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
⊢ (((∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑w.im * I)) +
        I * ∫ (y : ℝ) in z.im..w.im, c / (↑w.re + ↑y * I)) -
      I * ∫ (y : ℝ) in z.im..w.im, c / (↑z.re + ↑y * I) =
    2 * I * ↑π * c

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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
⊢ (((∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑w.im * I)) +
        I * ∫ (y : ℝ) in z.im..w.im, c / (↑w.re + ↑y * I)) -
      I * ∫ (y : ℝ) in z.im..w.im, c / (↑z.re + ↑y * I) =
    2 * I * ↑π * c
Tactic:
rw [integral_const_div_re_add_self h1.ne, integral_const_div_re_add_self h3.ne.symm]
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
⊢ ((∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑w.im * I)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c

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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
⊢ ((∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑w.im * I)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
Tactic:
rw [integral_const_div_self_add_im h2.ne, integral_const_div_self_add_im h4.ne.symm]
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c

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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
Tactic:
have l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹ := by group
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c

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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
Tactic:
have l3 := arctan_inv_of_neg <| mul_neg_of_pos_of_neg h3 <| inv_lt_zero.mpr h2
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c

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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
Tactic:
have l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹ := by group
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c

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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
Tactic:
have l6 := arctan_inv_of_neg <| mul_neg_of_neg_of_pos h1 <| inv_pos.mpr h4
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c

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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
Tactic:
have r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹ := by group
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c

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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
Tactic:
have r3 := arctan_inv_of_pos <| mul_pos_of_neg_of_neg h1 <| inv_lt_zero.mpr h2
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c

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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
Tactic:
have r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹ := by group
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c

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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
Tactic:
have r6 := arctan_inv_of_pos <| mul_pos h3 <| inv_pos.mpr h4
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c

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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * (↑(w.re ^ 2 + z.im ^ 2).log / 2 - ↑(z.re ^ 2 + z.im ^ 2).log / 2) -
            c * I * (↑(w.re / z.im).arctan - ↑(z.re / z.im).arctan) -
          (c * (↑(w.re ^ 2 + w.im ^ 2).log / 2 - ↑(z.re ^ 2 + w.im ^ 2).log / 2) -
            c * I * (↑(w.re / w.im).arctan - ↑(z.re / w.im).arctan)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * (1 / 2) + c * ↑(w.re ^ 2 + z.im ^ 2).log * I * I⁻¹ * (-1 / 2) +
                          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
                        (c * ↑(z.im ^ 2 + z.re ^ 2).log * I * I⁻¹ * (1 / 2) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                      c * I * ↑(z.re * z.im⁻¹).arctan +
                    c * I * ↑(w.re ^ 2 + w.im ^ 2).log * I⁻¹ * (1 / 2) +
                  c * I * ↑(z.re ^ 2 + w.im ^ 2).log * I⁻¹ * (-1 / 2) +
                c * I * ↑(w.re * w.im⁻¹).arctan +
              (-(c * I * ↑(z.re * w.im⁻¹).arctan) - c * I ^ 2 * I⁻¹ * ↑(-(w.im * w.re⁻¹)).arctan) +
            c * I ^ 2 * I⁻¹ * ↑(-(z.im * w.re⁻¹)).arctan +
          (c * I ^ 2 * I⁻¹ * ↑(-(w.im * z.re⁻¹)).arctan - c * I ^ 2 * I⁻¹ * ↑(-(z.im * z.re⁻¹)).arctan) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) =
    c * I * ↑π * 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * (1 / 2) + c * ↑(w.re ^ 2 + z.im ^ 2).log * I * I⁻¹ * (-1 / 2) +
                          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
                        (c * ↑(z.im ^ 2 + z.re ^ 2).log * I * I⁻¹ * (1 / 2) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                      c * I * ↑(z.re * z.im⁻¹).arctan +
                    c * I * ↑(w.re ^ 2 + w.im ^ 2).log * I⁻¹ * (1 / 2) +
                  c * I * ↑(z.re ^ 2 + w.im ^ 2).log * I⁻¹ * (-1 / 2) +
                c * I * ↑(w.re * w.im⁻¹).arctan +
              (-(c * I * ↑(z.re * w.im⁻¹).arctan) - c * I ^ 2 * I⁻¹ * ↑(-(w.im * w.re⁻¹)).arctan) +
            c * I ^ 2 * I⁻¹ * ↑(-(z.im * w.re⁻¹)).arctan +
          (c * I ^ 2 * I⁻¹ * ↑(-(w.im * z.re⁻¹)).arctan - c * I ^ 2 * I⁻¹ * ↑(-(z.im * z.re⁻¹)).arctan) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) =
    c * I * ↑π * 2
Tactic:
simp only [one_div, inv_I, mul_neg, neg_mul, I_sq, one_mul, neg_neg, arctan_neg, ofReal_neg, sub_neg_eq_add]
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * 2⁻¹ + -(c * ↑(w.re ^ 2 + z.im ^ 2).log * I * I * (-1 / 2)) +
                          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
                        (-(c * ↑(z.im ^ 2 + z.re ^ 2).log * I * I * 2⁻¹) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                      c * I * ↑(z.re * z.im⁻¹).arctan +
                    -(c * I * ↑(w.re ^ 2 + w.im ^ 2).log * I * 2⁻¹) +
                  -(c * I * ↑(z.re ^ 2 + w.im ^ 2).log * I * (-1 / 2)) +
                c * I * ↑(w.re * w.im⁻¹).arctan +
              (-(c * I * ↑(z.re * w.im⁻¹).arctan) + c * 1 * I * ↑(w.im * w.re⁻¹).arctan) +
            -(c * 1 * I * ↑(z.im * w.re⁻¹).arctan) +
          (-(c * 1 * I * ↑(w.im * z.re⁻¹).arctan) + c * 1 * I * ↑(z.im * z.re⁻¹).arctan) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * 2⁻¹ =
    c * I * ↑π * 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * 2⁻¹ + -(c * ↑(w.re ^ 2 + z.im ^ 2).log * I * I * (-1 / 2)) +
                          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
                        (-(c * ↑(z.im ^ 2 + z.re ^ 2).log * I * I * 2⁻¹) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                      c * I * ↑(z.re * z.im⁻¹).arctan +
                    -(c * I * ↑(w.re ^ 2 + w.im ^ 2).log * I * 2⁻¹) +
                  -(c * I * ↑(z.re ^ 2 + w.im ^ 2).log * I * (-1 / 2)) +
                c * I * ↑(w.re * w.im⁻¹).arctan +
              (-(c * I * ↑(z.re * w.im⁻¹).arctan) + c * 1 * I * ↑(w.im * w.re⁻¹).arctan) +
            -(c * 1 * I * ↑(z.im * w.re⁻¹).arctan) +
          (-(c * 1 * I * ↑(w.im * z.re⁻¹).arctan) + c * 1 * I * ↑(z.im * z.re⁻¹).arctan) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * 2⁻¹ =
    c * I * ↑π * 2
Tactic:
rw [l1, l3, l4, l6, r1, r3, r4, r6]
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * 2⁻¹ + -(c * ↑(w.re ^ 2 + z.im ^ 2).log * I * I * (-1 / 2)) +
                          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
                        (-(c * ↑(z.im ^ 2 + z.re ^ 2).log * I * I * 2⁻¹) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                      c * I * ↑(z.re * z.im⁻¹).arctan +
                    -(c * I * ↑(w.re ^ 2 + w.im ^ 2).log * I * 2⁻¹) +
                  -(c * I * ↑(z.re ^ 2 + w.im ^ 2).log * I * (-1 / 2)) +
                c * I * ↑(w.re * w.im⁻¹).arctan +
              (-(c * I * ↑(z.re * w.im⁻¹).arctan) + c * 1 * I * ↑(π / 2 - (w.re * w.im⁻¹).arctan)) +
            -(c * 1 * I * ↑(-(π / 2) - (w.re * z.im⁻¹).arctan)) +
          (-(c * 1 * I * ↑(-(π / 2) - (z.re * w.im⁻¹).arctan)) + c * 1 * I * ↑(π / 2 - (z.re * z.im⁻¹).arctan)) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * 2⁻¹ =
    c * I * ↑π * 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * 2⁻¹ + -(c * ↑(w.re ^ 2 + z.im ^ 2).log * I * I * (-1 / 2)) +
                          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
                        (-(c * ↑(z.im ^ 2 + z.re ^ 2).log * I * I * 2⁻¹) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                      c * I * ↑(z.re * z.im⁻¹).arctan +
                    -(c * I * ↑(w.re ^ 2 + w.im ^ 2).log * I * 2⁻¹) +
                  -(c * I * ↑(z.re ^ 2 + w.im ^ 2).log * I * (-1 / 2)) +
                c * I * ↑(w.re * w.im⁻¹).arctan +
              (-(c * I * ↑(z.re * w.im⁻¹).arctan) + c * 1 * I * ↑(π / 2 - (w.re * w.im⁻¹).arctan)) +
            -(c * 1 * I * ↑(-(π / 2) - (w.re * z.im⁻¹).arctan)) +
          (-(c * 1 * I * ↑(-(π / 2) - (z.re * w.im⁻¹).arctan)) + c * 1 * I * ↑(π / 2 - (z.re * z.im⁻¹).arctan)) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * 2⁻¹ =
    c * I * ↑π * 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * (1 / 2) +
                            (c * ↑(w.re ^ 2 + z.im ^ 2).log * I ^ 2 * (1 / 2) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                          c * I * ↑(z.re * z.im⁻¹).arctan +
                        (c * I * ↑(w.re * w.im⁻¹).arctan - c * I * ↑(z.re * w.im⁻¹).arctan) +
                      c * I * ↑(π * (1 / 2) - (w.re * w.im⁻¹).arctan) +
                    (-(c * I * ↑(π * (-1 / 2) - (w.re * z.im⁻¹).arctan)) -
                      c * I * ↑(π * (-1 / 2) - (z.re * w.im⁻¹).arctan)) +
                  c * I * ↑(π * (1 / 2) - (z.re * z.im⁻¹).arctan) +
                c * I ^ 2 * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
              c * I ^ 2 * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
            c * I ^ 2 * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) +
          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) =
    c * I * ↑π * 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * (1 / 2) +
                            (c * ↑(w.re ^ 2 + z.im ^ 2).log * I ^ 2 * (1 / 2) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                          c * I * ↑(z.re * z.im⁻¹).arctan +
                        (c * I * ↑(w.re * w.im⁻¹).arctan - c * I * ↑(z.re * w.im⁻¹).arctan) +
                      c * I * ↑(π * (1 / 2) - (w.re * w.im⁻¹).arctan) +
                    (-(c * I * ↑(π * (-1 / 2) - (w.re * z.im⁻¹).arctan)) -
                      c * I * ↑(π * (-1 / 2) - (z.re * w.im⁻¹).arctan)) +
                  c * I * ↑(π * (1 / 2) - (z.re * z.im⁻¹).arctan) +
                c * I ^ 2 * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
              c * I ^ 2 * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
            c * I ^ 2 * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) +
          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) =
    c * I * ↑π * 2
Tactic:
simp only [I_sq, ofReal_sub, ofReal_mul, ofReal_ofNat, ofReal_div, ofReal_neg, ofReal_one]
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * (1 / 2) +
                            (c * ↑(w.re ^ 2 + z.im ^ 2).log * -1 * (1 / 2) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                          c * I * ↑(z.re * z.im⁻¹).arctan +
                        (c * I * ↑(w.re * w.im⁻¹).arctan - c * I * ↑(z.re * w.im⁻¹).arctan) +
                      c * I * (↑π * (1 / 2) - ↑(w.re * w.im⁻¹).arctan) +
                    (-(c * I * (↑π * (-1 / 2) - ↑(w.re * z.im⁻¹).arctan)) -
                      c * I * (↑π * (-1 / 2) - ↑(z.re * w.im⁻¹).arctan)) +
                  c * I * (↑π * (1 / 2) - ↑(z.re * z.im⁻¹).arctan) +
                c * -1 * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
              c * -1 * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
            c * -1 * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) +
          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) =
    c * I * ↑π * 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
r6 : (w.re * w.im⁻¹)⁻¹.arctan = π / 2 - (w.re * w.im⁻¹).arctan
⊢ c * ↑(w.re ^ 2 + z.im ^ 2).log * (1 / 2) +
                            (c * ↑(w.re ^ 2 + z.im ^ 2).log * -1 * (1 / 2) - c * I * ↑(w.re * z.im⁻¹).arctan) +
                          c * I * ↑(z.re * z.im⁻¹).arctan +
                        (c * I * ↑(w.re * w.im⁻¹).arctan - c * I * ↑(z.re * w.im⁻¹).arctan) +
                      c * I * (↑π * (1 / 2) - ↑(w.re * w.im⁻¹).arctan) +
                    (-(c * I * (↑π * (-1 / 2) - ↑(w.re * z.im⁻¹).arctan)) -
                      c * I * (↑π * (-1 / 2) - ↑(z.re * w.im⁻¹).arctan)) +
                  c * I * (↑π * (1 / 2) - ↑(z.re * z.im⁻¹).arctan) +
                c * -1 * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
              c * -1 * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
            c * -1 * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) +
          c * ↑(z.im ^ 2 + z.re ^ 2).log * (-1 / 2) +
        c * ↑(w.re ^ 2 + w.im ^ 2).log * (-1 / 2) +
      c * ↑(z.re ^ 2 + w.im ^ 2).log * (1 / 2) =
    c * I * ↑π * 2
Tactic:
ring_nf
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
⊢ z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
Tactic:
group
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
⊢ w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
Tactic:
group
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
⊢ z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
Tactic:
group
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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹
l3 : (w.re * z.im⁻¹)⁻¹.arctan = -(π / 2) - (w.re * z.im⁻¹).arctan
l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹
l6 : (z.re * w.im⁻¹)⁻¹.arctan = -(π / 2) - (z.re * w.im⁻¹).arctan
r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹
r3 : (z.re * z.im⁻¹)⁻¹.arctan = π / 2 - (z.re * z.im⁻¹).arctan
⊢ w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹
Tactic:
group
State after:
no goals