Has Sum X eval

theorem hasSum_X_eval {u q : ℂ} (hu : Transcendental ℚ u) (h0 : 0 < ‖q‖)    (h1 : ‖q‖ < ‖u‖) (h2 : ‖u‖ < 1) :    HasSum (fun n : ℕ ↦ evalAt u ((PowerSeries.coeff n) X) * q ^ n) (XAn 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 : ℂ)) (fun v ↦ v / (1 - v) ^ 2)    cast_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 : ℂ)) (fun v ↦ v / (1 - v) ^ 2)    cast_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 : ℂ) * (u ^ d + u⁻¹ ^ d - 2))    (((hA.add hB).sub ((hasSum_prodC hq1).mul_left 2)).congr_fun fun p ↦ by ring)  have hfull := hasSum_nat_of_pnat_add    (f := fun n : ℕ ↦ evalAt u ((PowerSeries.coeff n) X) * q ^ n)    (hdiv.congr_fun fun N ↦ by rw [evalAt_coeff_X hu N.pos.ne'])  -- identify the value with `XAn u q`  have hposEq : ∀ n : ℕ+, q ^ (((n : ℕ) : ℤ)) * u / (1 - q ^ (((n : ℕ) : ℤ)) * u) ^ 2      = q ^ (n : ℕ) * u / (1 - q ^ (n : ℕ) * u) ^ 2 := fun n ↦ by rw [zpow_natCast]  have hnegEq : ∀ n : ℕ+, q ^ (-((n : ℕ) : ℤ)) * u / (1 - q ^ (-((n : ℕ) : ℤ)) * u) ^ 2      = q ^ (n : ℕ) * u⁻¹ / (1 - q ^ (n : ℕ) * u⁻¹) ^ 2 := fun n ↦ by    rw [zpow_neg_natCast_mul, inv_div_one_sub_inv_sq      (mul_ne_zero (pow_ne_zero _ hq0) (inv_ne_zero hu0))]  convert hfull using 1  rw [XAn, tsum_int_decomp (summable_V hq0 h1 h2),    show q ^ (0 : ℤ) * u / (1 - q ^ (0 : ℤ) * u) ^ 2 = u / (1 - u) ^ 2 by      rw [zpow_zero, one_mul],    tsum_congr hposEq, tsum_congr hnegEq, evalAt_coeff_X_zero hu, pow_zero, mul_one]  ring