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

case some
z : ℝ
hz : 0 < z
val✝ : ℝ≥0
hx : 1 < Option.some val✝
⊢ 1 < Option.some val✝ ^ z
x : ℝ≥0∞
z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 < x ^ z
cases x
no goals
case none
z : ℝ
hz : 0 < z
hx : 1 < none
⊢ 1 < none ^ z
simp [top_rpow_of_pos hz]
case some
z : ℝ
hz : 0 < z
val✝ : ℝ≥0
hx : 1 < val✝
⊢ 1 < Option.some val✝ ^ z
case some
z : ℝ
hz : 0 < z
val✝ : ℝ≥0
hx : 1 < Option.some val✝
⊢ 1 < Option.some val✝ ^ z
simp only [some_eq_coe, one_lt_coe_iff] at hx
no goals
case some
z : ℝ
hz : 0 < z
val✝ : ℝ≥0
hx : 1 < val✝
⊢ 1 < Option.some val✝ ^ z
simp [coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.one_lt_rpow hx hz]