Theorem: Bound.pow_le_pow_right_of_le_one_or_one_le (Ray/Tactic/Bound.lean)

State before:
α : Type
inst✝¹ : LinearOrder α
a✝ b c : α
R : Type
inst✝ : OrderedSemiring R
a : R
n m : ℕ
h : 1 ≤ a ∧ n ≤ m ∨ 0 ≤ a ∧ a ≤ 1 ∧ m ≤ n
⊢ a ^ n ≤ a ^ m
Tactic:
rcases h with ⟨a1, nm⟩ | ⟨a0, a1, mn⟩
State after:
case inl.intro
α : Type
inst✝¹ : LinearOrder α
a✝ b c : α
R : Type
inst✝ : OrderedSemiring R
a : R
n m : ℕ
a1 : 1 ≤ a
nm : n ≤ m
⊢ a ^ n ≤ a ^ m

case inr.intro.intro
α : Type
inst✝¹ : LinearOrder α
a✝ b c : α
R : Type
inst✝ : OrderedSemiring R
a : R
n m : ℕ
a0 : 0 ≤ a
a1 : a ≤ 1
mn : m ≤ n
⊢ a ^ n ≤ a ^ m

State before:
case inl.intro
α : Type
inst✝¹ : LinearOrder α
a✝ b c : α
R : Type
inst✝ : OrderedSemiring R
a : R
n m : ℕ
a1 : 1 ≤ a
nm : n ≤ m
⊢ a ^ n ≤ a ^ m
Tactic:
exact pow_le_pow_right a1 nm
State after:
no goals

State before:
case inr.intro.intro
α : Type
inst✝¹ : LinearOrder α
a✝ b c : α
R : Type
inst✝ : OrderedSemiring R
a : R
n m : ℕ
a0 : 0 ≤ a
a1 : a ≤ 1
mn : m ≤ n
⊢ a ^ n ≤ a ^ m
Tactic:
exact pow_le_pow_of_le_one a0 a1 mn
State after:
no goals