Theorem: Nat.pow_lt_pow_left (Algdata/Init/Nat.lean)

State before:
m n i : Nat
⊢ m < n → i > 0 → m ^ i < n ^ i
Tactic:
intro hmn hi
State after:
m n i : Nat
hmn : m < n
hi : i > 0
⊢ m ^ i < n ^ i

State before:
m n i : Nat
hmn : m < n
hi : i > 0
⊢ m ^ i < n ^ i
Tactic:
cases i
State after:
case zero
m n : Nat
hmn : m < n
hi : zero > 0
⊢ m ^ zero < n ^ zero

case succ
m n : Nat
hmn : m < n
n✝ : Nat
hi : succ n✝ > 0
⊢ m ^ succ n✝ < n ^ succ n✝

State before:
m n : Nat
hmn : m < n
hi : zero > 0
⊢ m ^ zero < n ^ zero
Tactic:
case zero => cases hi
State after:
no goals

State before:
m n : Nat
hmn : m < n
i : Nat
hi : succ i > 0
⊢ m ^ succ i < n ^ succ i
Tactic:
case succ i => calc
  m^i.succ = m^i * m := rfl
  _        ≤ n^i * m := Nat.mul_le_mul_right m (Nat.pow_le_pow_of_le_left (Nat.le_of_lt hmn) i)
  _        < n^i * n := Nat.mul_lt_mul_of_pos_left hmn (Nat.pos_pow_of_pos i (trans m.zero_le hmn))
State after:
no goals

State before:
m n : Nat
hmn : m < n
hi : zero > 0
⊢ m ^ zero < n ^ zero
Tactic:
cases hi
State after:
no goals

State before:
m n : Nat
hmn : m < n
i : Nat
hi : succ i > 0
⊢ m ^ succ i < n ^ succ i
Tactic:
calc
m^i.succ = m^i * m := rfl
_        ≤ n^i * m := Nat.mul_le_mul_right m (Nat.pow_le_pow_of_le_left (Nat.le_of_lt hmn) i)
_        < n^i * n := Nat.mul_lt_mul_of_pos_left hmn (Nat.pos_pow_of_pos i (trans m.zero_le hmn))
State after:
no goals