a b : ℝ
ha : a ≤ 0
z : ℂ
hz : Abs.abs z.im ≤ b
hb : b ≤ π / 2
⊢ a * ((Real.exp z.re + Real.exp (-z.re)) * Real.cos (Abs.abs z.im)) ≤ a * (Real.exp (Abs.abs z.re) * Real.cos b)
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : Abs.abs z.im ≤ b
hb : b ≤ π / 2
⊢ ↑abs (exp (↑a * (exp z + exp (-z)))) ≤ Real.exp (a * Real.cos b * Real.exp (Abs.abs z.re))
simp only [abs_exp, Real.exp_le_exp, ofReal_mul_re, add_re, exp_re, neg_im, Real.cos_neg, ←
  add_mul, mul_assoc, mul_comm (Real.cos b), neg_re, ← Real.cos_abs z.im]
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : Abs.abs z.im ≤ b
hb : b ≤ π / 2
this : Real.exp (Abs.abs z.re) ≤ Real.exp z.re + Real.exp (-z.re)
⊢ a * ((Real.exp z.re + Real.exp (-z.re)) * Real.cos (Abs.abs z.im)) ≤ a * (Real.exp (Abs.abs z.re) * Real.cos b)
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : Abs.abs z.im ≤ b
hb : b ≤ π / 2
⊢ a * ((Real.exp z.re + Real.exp (-z.re)) * Real.cos (Abs.abs z.im)) ≤ a * (Real.exp (Abs.abs z.re) * Real.cos b)
have : Real.exp (|z.re|) ≤ Real.exp z.re + Real.exp (-z.re) :=
  apply_abs_le_add_of_nonneg (fun x => (Real.exp_pos x).le) z.re
case refine'_1
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : Abs.abs z.im ≤ b
hb : b ≤ π / 2
this : Real.exp (Abs.abs z.re) ≤ Real.exp z.re + Real.exp (-z.re)
⊢ Real.cos b ≤ Real.cos (Abs.abs z.im)

case refine'_2
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : Abs.abs z.im ≤ b
hb : b ≤ π / 2
this : Real.exp (Abs.abs z.re) ≤ Real.exp z.re + Real.exp (-z.re)
⊢ 0 ≤ Real.cos b
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : Abs.abs z.im ≤ b
hb : b ≤ π / 2
this : Real.exp (Abs.abs z.re) ≤ Real.exp z.re + Real.exp (-z.re)
⊢ a * ((Real.exp z.re + Real.exp (-z.re)) * Real.cos (Abs.abs z.im)) ≤ a * (Real.exp (Abs.abs z.re) * Real.cos b)
refine' mul_le_mul_of_nonpos_left (mul_le_mul this _ _ ((Real.exp_pos _).le.trans this)) ha
no goals
case refine'_1
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : Abs.abs z.im ≤ b
hb : b ≤ π / 2
this : Real.exp (Abs.abs z.re) ≤ Real.exp z.re + Real.exp (-z.re)
⊢ Real.cos b ≤ Real.cos (Abs.abs z.im)
exact
  Real.cos_le_cos_of_nonneg_of_le_pi (_root_.abs_nonneg _)
    (hb.trans <| half_le_self <| Real.pi_pos.le) hz
case refine'_2
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : Abs.abs z.im ≤ b
hb : b ≤ π / 2
this : Real.exp (Abs.abs z.re) ≤ Real.exp z.re + Real.exp (-z.re)
⊢ -(π / 2) ≤ b
case refine'_2
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : Abs.abs z.im ≤ b
hb : b ≤ π / 2
this : Real.exp (Abs.abs z.re) ≤ Real.exp z.re + Real.exp (-z.re)
⊢ 0 ≤ Real.cos b
refine' Real.cos_nonneg_of_mem_Icc ⟨_, hb⟩
no goals
case refine'_2
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : Abs.abs z.im ≤ b
hb : b ≤ π / 2
this : Real.exp (Abs.abs z.re) ≤ Real.exp z.re + Real.exp (-z.re)
⊢ -(π / 2) ≤ b
exact (neg_nonpos.2 <| Real.pi_div_two_pos.le).trans ((_root_.abs_nonneg _).trans hz)