Theorem: Pos.pow_lt_pow_of_pos_left (Extra/Pos/Lemmas.lean)

State before:
x y : Pos
⊢ x < y → ∀ {z : Nat}, z > 0 → x ^ z < y ^ z
Tactic:
by_toNat
State after:
x y : Pos
⊢ y.toNat > x.toNat → ∀ {z : Nat}, z > 0 → y.toNat ^ z > x.toNat ^ z

State before:
x y : Pos
⊢ y.toNat > x.toNat → ∀ {z : Nat}, z > 0 → y.toNat ^ z > x.toNat ^ z
Tactic:
exact Nat.pow_lt_pow_of_pos_right
State after:
no goals