case inl
x y : ℝ
hx : 0 ≤ x
⊢ abs (x ^ y) ≤ abs x ^ y

case inr
x y : ℝ
hx : x < 0
⊢ abs (x ^ y) ≤ abs x ^ y
x y : ℝ
⊢ abs (x ^ y) ≤ abs x ^ y
cases' le_or_lt 0 x with hx hx
no goals
case inl
x y : ℝ
hx : 0 ≤ x
⊢ abs (x ^ y) ≤ abs x ^ y
rw [abs_rpow_of_nonneg hx]
case inr
x y : ℝ
hx : x < 0
⊢ exp (log x * y) * abs (cos (y * π)) ≤ exp (log x * y)
case inr
x y : ℝ
hx : x < 0
⊢ abs (x ^ y) ≤ abs x ^ y
rw [abs_of_neg hx, rpow_def_of_neg hx, rpow_def_of_pos (neg_pos.2 hx), log_neg_eq_log, abs_mul,
  abs_of_pos (exp_pos _)]
no goals
case inr
x y : ℝ
hx : x < 0
⊢ exp (log x * y) * abs (cos (y * π)) ≤ exp (log x * y)
exact mul_le_of_le_one_right (exp_pos _).le (abs_cos_le_one _)