Complex.gamma_half_vertical_norm_sq

theorem gamma_half_vertical_norm_sq (τ : ℝ) :    ‖Complex.Gamma (((1 / 2 : ℝ) : ℂ) + (τ : ℂ) * I)‖ ^ 2 =      Real.pi / Real.cosh (Real.pi * τ) := by  let z : ℂ := ((1 / 2 : ℝ) : ℂ) + (τ : ℂ) * I  have hconj : (starRingEnd ℂ) z = 1 - z := by    apply Complex.ext <;> norm_num [z, Complex.sub_re, Complex.sub_im, Complex.add_re,      Complex.add_im, Complex.mul_re, Complex.mul_im]  have hleft :      Complex.Gamma z * Complex.Gamma (1 - z) = ((‖Complex.Gamma z‖ ^ 2 : ℝ) : ℂ) := by    rw [← hconj, Complex.Gamma_conj, Complex.mul_conj, Complex.normSq_eq_norm_sq]  have hsin : Complex.sin (Real.pi * z) = (Real.cosh (Real.pi * τ) : ℂ) := by    simpa [z] using sin_pi_half_add_mul_I τ  have hcomplex :      ((‖Complex.Gamma z‖ ^ 2 : ℝ) : ℂ) =        ((Real.pi / Real.cosh (Real.pi * τ) : ℝ) : ℂ) := by    calc      ((‖Complex.Gamma z‖ ^ 2 : ℝ) : ℂ)          = Complex.Gamma z * Complex.Gamma (1 - z) := hleft.symm      _ = (Real.pi : ℂ) / Complex.sin (Real.pi * z) := Complex.Gamma_mul_Gamma_one_sub z      _ = ((Real.pi / Real.cosh (Real.pi * τ) : ℝ) : ℂ) := by        simp [hsin, Complex.ofReal_div]  simpa [z] using Complex.ofReal_injective hcomplex