case none

⊢ none ^ 1 = none

case some
val✝ : ℝ≥0
⊢ Option.some val✝ ^ 1 = Option.some val✝
x : ℝ≥0∞
⊢ x ^ 1 = x
cases x
no goals
case none

⊢ none ^ 1 = none
exact dif_pos zero_lt_one
case some
val✝ : ℝ≥0
⊢ (if val✝ = 0 ∧ 1 < 0 then ⊤ else ↑(val✝ ^ 1)) = Option.some val✝
case some
val✝ : ℝ≥0
⊢ Option.some val✝ ^ 1 = Option.some val✝
change ite _ _ _ = _
case some
val✝ : ℝ≥0
⊢ val✝ = 0 → 1 < 0 → False
case some
val✝ : ℝ≥0
⊢ (if val✝ = 0 ∧ 1 < 0 then ⊤ else ↑(val✝ ^ 1)) = Option.some val✝
simp only [NNReal.rpow_one, some_eq_coe, ite_eq_right_iff, top_ne_coe, and_imp]
no goals
case some
val✝ : ℝ≥0
⊢ val✝ = 0 → 1 < 0 → False
exact fun _ => zero_le_one.not_lt