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

State before:
m n a : Nat
⊢ 1 < a → m < n → a ^ m < a ^ n
Tactic:
intro ha h
State after:
m n a : Nat
ha : 1 < a
h : m < n
⊢ a ^ m < a ^ n

State before:
m n a : Nat
ha : 1 < a
h : m < n
⊢ a ^ m < a ^ n
Tactic:
induction m, n using Nat.recDiag with try contradiction
| zero_succ n =>
have hpos := Nat.pos_pow_of_pos n (Nat.le_of_lt ha)
apply Nat.lt_of_le_of_lt hpos
have : a ^ n * 1 < a ^ n * a := Nat.mul_lt_mul_of_pos_left ha hpos
rwa [Nat.mul_one] at this
| succ_succ m n ih =>
apply Nat.mul_lt_mul_of_pos_right _ (Nat.le_of_lt ha)
exact ih (Nat.lt_of_succ_lt_succ h)
State after:
no goals

State before:
case succ_zero
a : Nat
ha : 1 < a
m✝ : Nat
a✝ : m✝ < 0 → a ^ m✝ < a ^ 0
h : m✝ + 1 < 0
⊢ a ^ (m✝ + 1) < a ^ 0
Tactic:
contradiction
State after:
no goals

State before:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
⊢ a ^ 0 < a ^ (n + 1)
Tactic:
have hpos := Nat.pos_pow_of_pos n (Nat.le_of_lt ha)
State after:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
hpos : 0 < a ^ n
⊢ a ^ 0 < a ^ (n + 1)

State before:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
hpos : 0 < a ^ n
⊢ a ^ 0 < a ^ (n + 1)
Tactic:
apply Nat.lt_of_le_of_lt hpos
State after:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
hpos : 0 < a ^ n
⊢ a ^ n < a ^ (n + 1)

State before:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
hpos : 0 < a ^ n
⊢ a ^ n < a ^ (n + 1)
Tactic:
have : a ^ n * 1 < a ^ n * a := Nat.mul_lt_mul_of_pos_left ha hpos
State after:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
hpos : 0 < a ^ n
this : a ^ n * 1 < a ^ n * a
⊢ a ^ n < a ^ (n + 1)

State before:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
hpos : 0 < a ^ n
this : a ^ n * 1 < a ^ n * a
⊢ a ^ n < a ^ (n + 1)
Tactic:
rwa [Nat.mul_one] at this
State after:
no goals

State before:
case succ_succ
a : Nat
ha : 1 < a
m n : Nat
ih : m < n → a ^ m < a ^ n
h : m + 1 < n + 1
⊢ a ^ (m + 1) < a ^ (n + 1)
Tactic:
apply Nat.mul_lt_mul_of_pos_right _ (Nat.le_of_lt ha)
State after:
a : Nat
ha : 1 < a
m n : Nat
ih : m < n → a ^ m < a ^ n
h : m + 1 < n + 1
⊢ a.pow m < a.pow n

State before:
a : Nat
ha : 1 < a
m n : Nat
ih : m < n → a ^ m < a ^ n
h : m + 1 < n + 1
⊢ a.pow m < a.pow n
Tactic:
exact ih (Nat.lt_of_succ_lt_succ h)
State after:
no goals