Has Sum Y eval

theorem hasSum_Y_eval {u q : ℂ} (hu : Transcendental ℚ u) (h0 : 0 < ‖q‖)    (h1 : ‖q‖ < ‖u‖) (h2 : ‖u‖ < 1) :    HasSum (fun n : ℕ ↦ evalAt u ((PowerSeries.coeff n) Y) * q ^ n) (YAn u q) := by  have hu0 : u ≠ 0 := norm_pos_iff.mp (h0.trans h1)  have hq0 : q ≠ 0 := norm_pos_iff.mp h0  have hq1 : ‖q‖ < 1 := h1.trans h2  -- the two `u`-dependent Lambert double series  have hA := hasSum_prod_lambert (y := u) (fun m ↦ ((m.choose 2 : ℕ) : ℂ))    (fun v ↦ v ^ 2 / (1 - v) ^ 3) choose_two_le_sq hq1 (norm_mul_lt_one h1 h2)    fun v hv ↦ hasSum_pnat_lambert₂ hv  have hB := hasSum_prod_lambert (y := u⁻¹) (fun m ↦ (((m + 1).choose 2 : ℕ) : ℂ))    (fun v ↦ v / (1 - v) ^ 3) choose_add_one_two_le_sq hq1 (norm_mul_inv_lt_one h0 h1)    fun v hv ↦ hasSum_pnat_lambert₂' hv  -- combine, collect by divisors, and restore the `n = 0` term  have hdiv := hasSum_divisor_collect (x := q)    (fun d : ℕ ↦ ((d.choose 2 : ℕ) : ℂ) * u ^ d - (((d + 1).choose 2 : ℕ) : ℂ) * u⁻¹ ^ d      + (d : ℂ))    (((hA.sub hB).add (hasSum_prodC hq1)).congr_fun fun p ↦ by ring)  have hfull := hasSum_nat_of_pnat_add    (f := fun n : ℕ ↦ evalAt u ((PowerSeries.coeff n) Y) * q ^ n)    (hdiv.congr_fun fun N ↦ by rw [evalAt_coeff_Y hu N.pos.ne'])  -- identify the value with `YAn u q`  have hposEq : ∀ n : ℕ+,      (q ^ (((n : ℕ) : ℤ)) * u) ^ 2 / (1 - q ^ (((n : ℕ) : ℤ)) * u) ^ 3        = (q ^ (n : ℕ) * u) ^ 2 / (1 - q ^ (n : ℕ) * u) ^ 3 := fun n ↦ by rw [zpow_natCast]  have hnegEq : ∀ n : ℕ+,      (q ^ (-((n : ℕ) : ℤ)) * u) ^ 2 / (1 - q ^ (-((n : ℕ) : ℤ)) * u) ^ 3        = -(q ^ (n : ℕ) * u⁻¹ / (1 - q ^ (n : ℕ) * u⁻¹) ^ 3) := fun n ↦ by    rw [zpow_neg_natCast_mul, inv_sq_div_one_sub_inv_cube      (mul_ne_zero (pow_ne_zero _ hq0) (inv_ne_zero hu0))]  convert hfull using 1  rw [YAn, tsum_int_decomp (summable_V₂ hq0 h1 h2),    show (q ^ (0 : ℤ) * u) ^ 2 / (1 - q ^ (0 : ℤ) * u) ^ 3 = u ^ 2 / (1 - u) ^ 3 by      rw [zpow_zero, one_mul],    tsum_congr hposEq, tsum_congr hnegEq, tsum_neg, evalAt_coeff_Y_zero hu, pow_zero,    mul_one]  ring