Theorem: Bound.Real.rpow_le_rpow_of_exponent_le_or_ge (Ray/Tactic/Bound.lean)

State before:
α : Type
inst✝ : LinearOrder α
a b c : α
x y z : ℝ
h : 1 ≤ x ∧ y ≤ z ∨ 0 < x ∧ x ≤ 1 ∧ z ≤ y
⊢ x ^ y ≤ x ^ z
Tactic:
rcases h with ⟨x1, yz⟩ | ⟨x0, x1, zy⟩
State after:
case inl.intro
α : Type
inst✝ : LinearOrder α
a b c : α
x y z : ℝ
x1 : 1 ≤ x
yz : y ≤ z
⊢ x ^ y ≤ x ^ z

case inr.intro.intro
α : Type
inst✝ : LinearOrder α
a b c : α
x y z : ℝ
x0 : 0 < x
x1 : x ≤ 1
zy : z ≤ y
⊢ x ^ y ≤ x ^ z

State before:
case inl.intro
α : Type
inst✝ : LinearOrder α
a b c : α
x y z : ℝ
x1 : 1 ≤ x
yz : y ≤ z
⊢ x ^ y ≤ x ^ z
Tactic:
exact Real.rpow_le_rpow_of_exponent_le x1 yz
State after:
no goals

State before:
case inr.intro.intro
α : Type
inst✝ : LinearOrder α
a b c : α
x y z : ℝ
x0 : 0 < x
x1 : x ≤ 1
zy : z ≤ y
⊢ x ^ y ≤ x ^ z
Tactic:
exact Real.rpow_le_rpow_of_exponent_ge x0 x1 zy
State after:
no goals