Delta imag axis real

lemma Delta_imag_axis_real : ResToImagAxis.Real Δ := by  intro t ht  simp [ResToImagAxis, ht, Δ]  set g : ℕ → ℂ := fun n => (1 - cexp (2 * π * Complex.I * (n + 1) * (Complex.I * t))) ^ 24  have hArg (n : ℕ) :      2 * (π : ℂ) * Complex.I * (n + 1) * (Complex.I * t) = -(2 * (π : ℂ) * (n + 1) * t) := by    calc      2 * (π : ℂ) * Complex.I * (n + 1) * (Complex.I * t)        = 2 * (π : ℂ) * (Complex.I * Complex.I) * (n + 1) * t := by ring      _ = -(2 * (π : ℂ) * (n + 1) * t) := by simp  have him_g : ∀ n, (g n).im = 0 := fun n => by    have : (cexp (-(2 * (π : ℂ) * ((n + 1) : ℂ) * t))).im = 0 := by      simpa [mul_comm, mul_left_comm, mul_assoc] using (cexp_aux4 t n)    have : ((1 - cexp (2 * (π : ℂ) * Complex.I * (n + 1) * (Complex.I * t))) : ℂ).im = 0 := by      simpa [Complex.sub_im, hArg n] using this    simpa [g] using Complex.im_pow_eq_zero_of_im_eq_zero this 24  let z : ℍ := ⟨Complex.I * t, by simp [ht]⟩  have hmul : Multipliable g := by    have hz : (z : ℂ) = Complex.I * t := rfl    simpa [g, hz] using      (Multipliable.pow (by simpa using MultipliableEtaProductExpansion z) 24)  have htprod_im : (∏' n : ℕ, g n).im = 0 :=    Complex.im_tprod_eq_zero_of_im_eq_zero g hmul him_g  have him_pref : (cexp (2 * π * Complex.I * (Complex.I * t))).im = 0 := by    have : (cexp (-(2 * (π : ℂ) * t))).im = 0 := by simpa using cexp_aux5 t    simpa [by simpa using hArg 0] using this  simp [g, him_pref, htprod_im]