Theorem: Nat.pow_lt_pow_of_pos_right (Extra/Nat/Lemmas.lean)

State before:
case zero
x y : Nat
h : x < y
⊢ 0 > 0 → x ^ 0 < y ^ 0
Tactic:
intro
State after:
case zero
x y : Nat
h : x < y
a✝ : 0 > 0
⊢ x ^ 0 < y ^ 0

State before:
case zero
x y : Nat
h : x < y
a✝ : 0 > 0
⊢ x ^ 0 < y ^ 0
Tactic:
contradiction
State after:
no goals

State before:
case succ
x y : Nat
h : x < y
z : Nat
⊢ z + 1 > 0 → x ^ (z + 1) < y ^ (z + 1)
Tactic:
intro
State after:
case succ
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ^ (z + 1) < y ^ (z + 1)

State before:
case succ
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ^ (z + 1) < y ^ (z + 1)
Tactic:
rw [Nat.pow_succ, Nat.pow_succ]
State after:
case succ
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ^ z * x < y ^ z * y

State before:
case succ
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ^ z * x < y ^ z * y
Tactic:
apply Nat.mul_lt_mul_of_le_of_lt
State after:
case succ.hac
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ^ z ≤ y ^ z

case succ.hbd
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x < y

case succ.hc
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ 0 < y ^ z

State before:
case succ.hac
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ^ z ≤ y ^ z
Tactic:
apply Nat.pow_le_pow_left
State after:
case succ.hac.h
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ≤ y

State before:
case succ.hac.h
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ≤ y
Tactic:
apply Nat.le_of_lt
State after:
case succ.hac.h.a
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x < y

State before:
case succ.hac.h.a
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x < y
Tactic:
exact h
State after:
no goals

State before:
case succ.hbd
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x < y
Tactic:
exact h
State after:
no goals

State before:
case succ.hc
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ 0 < y ^ z
Tactic:
apply Nat.pos_pow_of_pos
State after:
case succ.hc.h
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ 0 < y

State before:
case succ.hc.h
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ 0 < y
Tactic:
apply Nat.lt_of_le_of_lt
State after:
case succ.hc.h.h₁
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ 0 ≤ ?succ.hc.h.m

case succ.hc.h.h₂
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ ?succ.hc.h.m < y

case succ.hc.h.m
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ Nat

State before:
case succ.hc.h.h₁
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ 0 ≤ ?succ.hc.h.m
Tactic:
apply Nat.zero_le
State after:
no goals

State before:
case succ.hc.h.h₂
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ ?succ.hc.h.m < y
Tactic:
exact h
State after:
no goals