Theorem: Nat.pow_lt_pow_of_gt_one_left (GMLInit/Data/Nat/Pow.lean)

State before:
case zero_right
z x : Nat
h : x < 0
⊢ z > 1 → z ^ x < z ^ 0
Tactic:
intro
State after:
case zero_right
z x : Nat
h : x < 0
a✝ : z > 1
⊢ z ^ x < z ^ 0

State before:
case zero_right
z x : Nat
h : x < 0
a✝ : z > 1
⊢ z ^ x < z ^ 0
Tactic:
contradiction
State after:
no goals

State before:
case zero_left
z y : Nat
h : 0 < y
⊢ z > 1 → z ^ 0 < z ^ y
Tactic:
intro hz
State after:
case zero_left
z y : Nat
h : 0 < y
hz : z > 1
⊢ z ^ 0 < z ^ y

State before:
case zero_left
z y : Nat
h : 0 < y
hz : z > 1
⊢ z ^ 0 < z ^ y
Tactic:
transitivity z using LT.lt, LE.le
State after:
case zero_left.left
z y : Nat
h : 0 < y
hz : z > 1
⊢ z ^ 0 < z

case zero_left.right
z y : Nat
h : 0 < y
hz : z > 1
⊢ z ≤ z ^ y

State before:
case zero_left.left
z y : Nat
h : 0 < y
hz : z > 1
⊢ z ^ 0 < z
Tactic:
rw [Nat.pow_zero]
State after:
case zero_left.left
z y : Nat
h : 0 < y
hz : z > 1
⊢ 1 < z

State before:
case zero_left.left
z y : Nat
h : 0 < y
hz : z > 1
⊢ 1 < z
Tactic:
exact hz
State after:
no goals

State before:
case zero_left.right
z y : Nat
h : 0 < y
hz : z > 1
⊢ z ≤ z ^ y
Tactic:
exact Nat.le_pow_right _ _
State after:
no goals

State before:
case succ_succ
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
⊢ z > 1 → z ^ (x + 1) < z ^ (y + 1)
Tactic:
intro hz
State after:
case succ_succ
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ (x + 1) < z ^ (y + 1)

State before:
case succ_succ
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ (x + 1) < z ^ (y + 1)
Tactic:
rw [Nat.pow_succ, Nat.pow_succ]
State after:
case succ_succ
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ x * z < z ^ y * z

State before:
case succ_succ
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ x * z < z ^ y * z
Tactic:
apply Nat.mul_lt_mul_of_pos_right
State after:
case succ_succ.h
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ x < z ^ y

case succ_succ.hk
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z > 0

State before:
case succ_succ.h
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ x < z ^ y

case succ_succ.hk
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z > 0
Tactic:
apply H
State after:
case succ_succ.h.h
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ x < y

case succ_succ.h.a
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z > 1

case succ_succ.hk
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z > 0

State before:
case succ_succ.h.h
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ x < y
Tactic:
exact Nat.lt_of_succ_lt_succ h
State after:
no goals

State before:
case succ_succ.h.a
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z > 1
Tactic:
exact hz
State after:
no goals

State before:
case succ_succ.hk
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z > 0
Tactic:
transitivity 1 using LT.lt
State after:
case succ_succ.hk.left
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ 0 < 1

case succ_succ.hk.right
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ 1 < z

State before:
case succ_succ.hk.left
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ 0 < 1
Tactic:
exact Nat.zero_lt_one
State after:
no goals

State before:
case succ_succ.hk.right
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ 1 < z
Tactic:
exact hz
State after:
no goals