E₂ imag axis real

@[fun_prop]theorem E₂_imag_axis_real : ResToImagAxis.Real E₂ := by  intro t ht  simp only [Function.resToImagAxis, ResToImagAxis, ht, ↓reduceDIte]  let z : ℍ := ⟨Complex.I * t, by simp [ht]⟩  change (E₂ z).im = 0  have hq := E₂_eq z  rw [hq]  simp only [sub_im, one_im, zero_sub]  -- Step 1: Show each term in the sum is real on the imaginary axis  have hterm_im : ∀ n : ℕ+, (↑n * cexp (2 * ↑Real.pi * Complex.I * n * z) /      (1 - cexp (2 * ↑Real.pi * Complex.I * n * z))).im = 0 := by    intro n    have hexp_arg : 2 * ↑Real.pi * Complex.I * n * z = (-(2 * Real.pi * (n : ℝ) * t) : ℝ) := by      have h1 : 2 * ↑Real.pi * Complex.I * z * n = (-(2 * Real.pi * (n : ℝ) * t) : ℝ) := by        simpa [z] using exp_imag_axis_arg (t := t) ht n      simpa [mul_assoc, mul_left_comm, mul_comm] using h1    -- Using simp only: `simp` gives false positive linter warning but args are needed    have hone_sub_real : (1 - cexp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)).im = 0 := by      simp only [Complex.sub_im, Complex.one_im, hexp_arg, exp_ofReal_im, sub_zero]    have hnum_real : (↑n * cexp (2 * ↑Real.pi * Complex.I * n * z)).im = 0 := by      simp only [mul_im, natCast_im, hexp_arg, exp_ofReal_im, mul_zero, zero_mul, add_zero]    simp [Complex.div_im, hnum_real, hone_sub_real]  -- Step 2: Summability of the series  have hsum : Summable fun n : ℕ+ => ↑n * cexp (2 * ↑Real.pi * Complex.I * n * z) /      (1 - cexp (2 * ↑Real.pi * Complex.I * n * z)) := by    set r : ℂ := cexp (2 * ↑Real.pi * Complex.I * z) with hr    have hr_norm : ‖r‖ < 1 := by      simpa [hr] using exp_upperHalfPlane_lt_one z    have hs : Summable fun n : ℕ => (n : ℂ) * r ^ n / (1 - r ^ n) := by      simpa [pow_one] using        (summable_norm_pow_mul_geometric_div_one_sub (k := 1) (r := r) hr_norm)    refine (hs.comp_injective PNat.coe_injective).congr ?_    intro n    have hpow : r ^ (n : ℕ) = cexp (2 * ↑Real.pi * Complex.I * (↑n : ℂ) * z) := by      rw [hr]      simpa [mul_assoc, mul_left_comm, mul_comm] using        (Complex.exp_nat_mul (2 * ↑Real.pi * Complex.I * z) (n : ℕ)).symm    simp [hpow]  -- Step 3: The sum has zero imaginary part  have hsum_im : (∑' (n : ℕ+), ↑n * cexp (2 * ↑Real.pi * Complex.I * n * z) /      (1 - cexp (2 * ↑Real.pi * Complex.I * n * z))).im = 0 := by    rw [Complex.im_tsum hsum]    simp [hterm_im]  -- Step 4: 24 * sum is real, so -(24 * sum).im = 0  simp [Complex.mul_im, hsum_im]