Deriv Weierstrass P q expansion

theorem derivWeierstrassP_q_expansion (τ : ℂ) (hτ : 0 < τ.im) (z : ℂ) (hz : 0 < z.im)    (hzτ : z.im < τ.im) :    ℘'[periodPair τ hτ.ne'] z =      (2 * (Real.pi : ℂ) * I) ^ 3 * (XAn (e z) (e τ) + 2 * YAn (e z) (e τ)) := by  have hq0 : e τ ≠ 0 := e_ne_zero τ  have hu1 : ‖e z‖ < 1 := norm_e_lt_one hz  have hqu : ‖e τ‖ < ‖e z‖ := norm_e_lt_norm_e hzτ  -- Step 1: reindex the lattice sum by `ℤ × ℤ`  have h0 : HasSum (fun p : ℤ × ℤ ↦ -2 / (z - (p.1 * τ + p.2)) ^ 3)      (℘'[periodPair τ hτ.ne'] z) :=    hasSum_lattice_prod hτ.ne' (f := fun w ↦ -2 / (z - w) ^ 3)      ((periodPair τ hτ.ne').hasSum_derivWeierstrassP z)  -- Step 2: summability of rows (for Fubini)  have hrowsumm : ∀ n : ℤ, Summable fun m : ℤ ↦ -2 / (z - (n * τ + m)) ^ 3 := fun n ↦    ((summable_int_inv_pow_sub (z - n * τ) (k := 3) (by norm_num)).mul_left (-2)).congr fun m ↦ by      rw [div_eq_mul_inv, show z - (n * τ + m) = z - n * τ - m by ring]  -- Step 3: evaluate each row  have hrowval : ∀ n : ℤ,      ∑' m : ℤ, -2 / (z - (n * τ + m)) ^ 3      = (2 * (Real.pi : ℂ) * I) ^ 3 *          (e τ ^ (-n) * e z * (1 + e τ ^ (-n) * e z) / (1 - e τ ^ (-n) * e z) ^ 3) := by    intro n    rw [show ∑' m : ℤ, -2 / (z - (n * τ + m)) ^ 3        = -2 * ∑' m : ℤ, (((z - n * τ) - m) ^ 3)⁻¹ by      rw [← tsum_mul_left]      exact tsum_congr fun m ↦ by        rw [div_eq_mul_inv, show z - (n * τ + m) = z - n * τ - m by ring],      tsum_int_inv_pow_sub, sum_int_inv_cube' _ (im_sub_int_mul_ne_zero hτ hz hzτ n),      e_sub_intCast_mul]    ring  -- Step 4: sum the rows (Fubini) and recombine into `XAn + 2YAn`  rw [← h0.tsum_eq, h0.summable.tsum_prod' fun n ↦ hrowsumm n, tsum_congr hrowval,    tsum_mul_left, tsum_comp_neg      fun n : ℤ ↦ e τ ^ n * e z * (1 + e τ ^ n * e z) / (1 - e τ ^ n * e z) ^ 3,    tsum_congr fun n : ℤ ↦ (div_sq_add_two_mul_div_cube (e τ ^ n * e z)).symm,    Summable.tsum_add (summable_V hq0 hqu hu1) ((summable_V₂ hq0 hqu hu1).mul_left 2),    tsum_mul_left, XAn, YAn]  ring