case none
z : ℝ
hz : z < 0
hx : 1 ≤ none
⊢ none ^ z ≤ 1

case some
z : ℝ
hz : z < 0
val✝ : ℝ≥0
hx : 1 ≤ Option.some val✝
⊢ Option.some val✝ ^ z ≤ 1
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
hz : z < 0
⊢ x ^ z ≤ 1
cases x
no goals
case none
z : ℝ
hz : z < 0
hx : 1 ≤ none
⊢ none ^ z ≤ 1
simp [top_rpow_of_neg hz, zero_lt_one]
case some
z : ℝ
hz : z < 0
val✝ : ℝ≥0
hx : 1 ≤ val✝
⊢ Option.some val✝ ^ z ≤ 1
case some
z : ℝ
hz : z < 0
val✝ : ℝ≥0
hx : 1 ≤ Option.some val✝
⊢ Option.some val✝ ^ z ≤ 1
simp only [one_le_coe_iff, some_eq_coe] at hx
no goals
case some
z : ℝ
hz : z < 0
val✝ : ℝ≥0
hx : 1 ≤ val✝
⊢ Option.some val✝ ^ z ≤ 1
simp [coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)),
  NNReal.rpow_le_one_of_one_le_of_nonpos hx (le_of_lt hz)]