Theorem: ResidueTheoremAtOrigin'
Proof 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]
Proof 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