Complex.Gamma.norm_le_Gamma_re

theorem norm_le_Gamma_re {z : ℂ} (hz : 0 < z.re) : ‖Gamma z‖ ≤ Real.Gamma z.re := by  rw [Gamma_eq_integral hz, Real.Gamma_eq_integral hz]  have h_norm_eq : ∀ t ∈ Set.Ioi (0 : ℝ),      ‖((-t).exp : ℂ) * (t : ℂ) ^ (z - 1)‖ = Real.exp (-t) * t ^ (z.re - 1) := by    intro t ht    have hcpow : ‖(t : ℂ) ^ (z - 1)‖ = t ^ (z.re - 1) := by      simpa using norm_cpow_eq_rpow_re_of_pos ht (z - 1)    simp [norm_exp, hcpow]  calc    ‖GammaIntegral z‖        ≤ ∫ t in Set.Ioi (0 : ℝ), ‖((-t).exp : ℂ) * (t : ℂ) ^ (z - 1)‖ := by          unfold GammaIntegral          exact norm_integral_le_integral_norm _    _ = ∫ t in Set.Ioi (0 : ℝ), Real.exp (-t) * t ^ (z.re - 1) := by          exact setIntegral_congr_fun measurableSet_Ioi h_norm_eq