internlm/Lean-Github huggingface dataset:
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⁻¹)⁻¹
⊢ 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
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
⊢ 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
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
⊢ 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
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⁻¹)⁻¹
⊢ 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
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⁻¹)⁻¹
⊢ 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
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
⊢ 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
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
⊢ 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
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⁻¹)⁻¹
⊢ 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
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⁻¹)⁻¹
⊢ 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
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
⊢ 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
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
⊢ 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
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⁻¹)⁻¹
⊢ 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
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⁻¹)⁻¹
⊢ 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
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 / 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
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 / 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
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 * 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
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 * 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]
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 * 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