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 [one_le_coe_iff, some_eq_coe] 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_le_rpow hx (le_of_lt hz)]