case none
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
⊢ none ^ y ≤ none ^ z

case some
y z : ℝ
hyz : y ≤ z
val✝ : ℝ≥0
hx : 1 ≤ Option.some val✝
⊢ Option.some val✝ ^ y ≤ Option.some val✝ ^ z
x : ℝ≥0∞
y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ x ^ y ≤ x ^ z
cases x
no goals
case none
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ none
⊢ none ^ y ≤ none ^ z
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos, le_refl] <;>
linarith
case some
y z : ℝ
hyz : y ≤ z
val✝ : ℝ≥0
hx : 1 ≤ val✝
⊢ Option.some val✝ ^ y ≤ Option.some val✝ ^ z
case some
y z : ℝ
hyz : y ≤ z
val✝ : ℝ≥0
hx : 1 ≤ Option.some val✝
⊢ Option.some val✝ ^ y ≤ Option.some val✝ ^ z
simp only [one_le_coe_iff, some_eq_coe] at hx
no goals
case some
y z : ℝ
hyz : y ≤ z
val✝ : ℝ≥0
hx : 1 ≤ val✝
⊢ Option.some val✝ ^ y ≤ Option.some val✝ ^ z
simp [coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)),
  NNReal.rpow_le_rpow_of_exponent_le hx hyz]