Complex.norm_cos_le_exp_abs_im

lemma norm_cos_le_exp_abs_im (z : ℂ) : ‖cos z‖ ≤ Real.exp |z.im| := by  have hcos :      cos z = (exp (z * I) + exp (-z * I)) / 2 := by    simp [cos]  have htri :      ‖exp (z * I) + exp (-z * I)‖ ≤ ‖exp (z * I)‖ + ‖exp (-z * I)‖ :=    norm_add_le _ _  have hdiv :      ‖(exp (z * I) + exp (-z * I)) / 2‖        ≤ (‖exp (z * I)‖ + ‖exp (-z * I)‖) / 2 := by    have : ‖exp (z * I) + exp (-z * I)‖ / 2          ≤ (‖exp (z * I)‖ + ‖exp (-z * I)‖) / 2 :=      div_le_div_of_nonneg_right htri (by norm_num)    simpa [Complex.norm_div, Complex.norm_ofNat] using this  have h1 : ‖exp (z * I)‖ = Real.exp (-(z.im)) := by    simp [norm_exp, mul_re, I_re, I_im]  have h2 : ‖exp (-(z * I))‖ = Real.exp (z.im) := by    simp [norm_exp, mul_re, I_re, I_im]  have habs1 : Real.exp (-(z.im)) ≤ Real.exp |z.im| :=    Real.exp_le_exp.mpr (neg_le_abs z.im)  have habs2 : Real.exp (z.im) ≤ Real.exp |z.im| :=    Real.exp_le_exp.mpr (le_abs_self z.im)  have hsum :      (‖exp (z * I)‖ + ‖exp (-(z * I))‖) / 2 ≤ Real.exp |z.im| := by    have : ‖exp (z * I)‖ + ‖exp (-(z * I))‖        ≤ Real.exp |z.im| + Real.exp |z.im| := by      simpa [h1, h2] using add_le_add habs1 habs2    have : (‖exp (z * I)‖ + ‖exp (-(z * I))‖) / 2        ≤ (Real.exp |z.im| + Real.exp |z.im|) / 2 :=      div_le_div_of_nonneg_right this (by norm_num)    simpa [two_mul] using this  have :      ‖cos z‖ ≤ (‖exp (z * I)‖ + ‖exp (-(z * I))‖) / 2 := by    simpa [hcos] using hdiv  exact le_trans this hsum