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 [some_eq_coe, one_lt_coe_iff] 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_trans zero_lt_one hx)),
  NNReal.rpow_lt_one_of_one_lt_of_neg hx hz]