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

State before:
case zero_right
x : Nat
⊢ 0 > 0 → x ≤ x ^ 0
Tactic:
intro
State after:
case zero_right
x : Nat
a✝ : 0 > 0
⊢ x ≤ x ^ 0

State before:
case zero_right
x : Nat
a✝ : 0 > 0
⊢ x ≤ x ^ 0
Tactic:
contradiction
State after:
no goals

State before:
case zero_left
y : Nat
⊢ y > 0 → 0 ≤ 0 ^ y
Tactic:
intro
State after:
case zero_left
y : Nat
a✝ : y > 0
⊢ 0 ≤ 0 ^ y

State before:
case zero_left
y : Nat
a✝ : y > 0
⊢ 0 ≤ 0 ^ y
Tactic:
apply Nat.zero_le
State after:
no goals

State before:
case succ_succ
x y : Nat
a✝ : y > 0 → x ≤ x ^ y
⊢ y + 1 > 0 → x + 1 ≤ (x + 1) ^ (y + 1)
Tactic:
intro
State after:
case succ_succ
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ x + 1 ≤ (x + 1) ^ (y + 1)

State before:
case succ_succ
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ x + 1 ≤ (x + 1) ^ (y + 1)
Tactic:
transitivity (1 * (x + 1)) using Eq, LE.le
State after:
case succ_succ.left
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ x + 1 = 1 * (x + 1)

case succ_succ.right
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 * (x + 1) ≤ (x + 1) ^ (y + 1)

State before:
case succ_succ.left
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ x + 1 = 1 * (x + 1)
Tactic:
rw [Nat.one_mul]
State after:
no goals

State before:
case succ_succ.right
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 * (x + 1) ≤ (x + 1) ^ (y + 1)
Tactic:
rw [Nat.pow_succ]
State after:
case succ_succ.right
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 * (x + 1) ≤ (x + 1) ^ y * (x + 1)

State before:
case succ_succ.right
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 * (x + 1) ≤ (x + 1) ^ y * (x + 1)
Tactic:
apply Nat.mul_le_mul_right
State after:
case succ_succ.right.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 ≤ (x + 1) ^ y

State before:
case succ_succ.right.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 ≤ (x + 1) ^ y
Tactic:
apply Nat.succ_le_of_lt
State after:
case succ_succ.right.h.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 0 < (x + 1) ^ y

State before:
case succ_succ.right.h.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 0 < (x + 1) ^ y
Tactic:
apply Nat.pos_pow_of_pos
State after:
case succ_succ.right.h.h.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 0 < x + 1

State before:
case succ_succ.right.h.h.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 0 < x + 1
Tactic:
apply Nat.zero_lt_succ
State after:
no goals