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

State before:
n i : Nat
⊢ n ≥ 2 → i < n ^ i
Tactic:
intro h
State after:
n i : Nat
h : n ≥ 2
⊢ i < n ^ i

State before:
n i : Nat
h : n ≥ 2
⊢ i < n ^ i
Tactic:
induction i
State after:
case zero
n : Nat
h : n ≥ 2
⊢ zero < n ^ zero

case succ
n : Nat
h : n ≥ 2
n✝ : Nat
n_ih✝ : n✝ < n ^ n✝
⊢ succ n✝ < n ^ succ n✝

State before:
n : Nat
h : n ≥ 2
⊢ zero < n ^ zero
Tactic:
case zero => exact Nat.le.refl
State after:
no goals

State before:
n : Nat
h : n ≥ 2
i : Nat
h_ind : i < n ^ i
⊢ succ i < n ^ succ i
Tactic:
case succ i h_ind =>
have : n^i > 0 := Nat.pos_pow_of_pos i (Nat.lt_of_succ_lt h)
calc
  i+1 < n^i + 1 := succ_lt_succ h_ind
  _   ≤ n^i + n^i := Nat.add_le_add_left this _
  _   = n^i*2 := (Nat.mul_two _).symm
  _   ≤ n^i*n := Nat.mul_le_mul_left _ h
  _   = n^(i+1) := rfl
State after:
no goals

State before:
n : Nat
h : n ≥ 2
⊢ zero < n ^ zero
Tactic:
exact Nat.le.refl
State after:
no goals

State before:
n : Nat
h : n ≥ 2
i : Nat
h_ind : i < n ^ i
⊢ succ i < n ^ succ i
Tactic:
have : n^i > 0 := Nat.pos_pow_of_pos i (Nat.lt_of_succ_lt h)
State after:
n : Nat
h : n ≥ 2
i : Nat
h_ind : i < n ^ i
this : n ^ i > 0
⊢ succ i < n ^ succ i

State before:
n : Nat
h : n ≥ 2
i : Nat
h_ind : i < n ^ i
this : n ^ i > 0
⊢ succ i < n ^ succ i
Tactic:
calc
  i+1 < n^i + 1 := succ_lt_succ h_ind
  _   ≤ n^i + n^i := Nat.add_le_add_left this _
  _   = n^i*2 := (Nat.mul_two _).symm
  _   ≤ n^i*n := Nat.mul_le_mul_left _ h
  _   = n^(i+1) := rfl
State after:
no goals