ResidueTheoremAtOrigin'

lemma ResidueTheoremAtOrigin' {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 := by  simp only [RectangleIntegral, HIntegral, VIntegral, smul_eq_mul]  rw [integral_const_div_re_add_self h1.ne, integral_const_div_re_add_self h3.ne.symm]  rw [integral_const_div_self_add_im h2.ne, integral_const_div_self_add_im h4.ne.symm]  have l1 : z.im * w.re⁻¹ = (w.re * z.im⁻¹)⁻¹ := by group  have l3 := arctan_inv_of_neg <| mul_neg_of_pos_of_neg h3 <| inv_lt_zero.mpr h2  have l4 : w.im * z.re⁻¹ = (z.re * w.im⁻¹)⁻¹ := by group  have l6 := arctan_inv_of_neg <| mul_neg_of_neg_of_pos h1 <| inv_pos.mpr h4  have r1 : z.im * z.re⁻¹ = (z.re * z.im⁻¹)⁻¹ := by group  have r3 := arctan_inv_of_pos <| mul_pos_of_neg_of_neg h1 <| inv_lt_zero.mpr h2  have r4 : w.im * w.re⁻¹ = (w.re * w.im⁻¹)⁻¹ := by group  have r6 := arctan_inv_of_pos <| mul_pos h3 <| inv_pos.mpr h4  ring_nf  simp only [one_div, inv_I, mul_neg, neg_mul, I_sq, neg_neg, arctan_neg, ofReal_neg,    sub_neg_eq_add]  rw [l1, l3, l4, l6, r1, r3, r4, r6]  ring_nf  simp only [I_sq, ofReal_sub, ofReal_mul, ofReal_ofNat, ofReal_div, ofReal_neg, ofReal_one]  ring_nf