Simple factorial proof

Stream: general

[James Li]

I'm a beginner to Lean and am trying to prove that n! > 2^n for n >= 4. Here is my proof so far, but I'm getting a bit stuck:

theorem factorial_power2 (n : ℕ) (hn : 4 <= n) : Nat.factorial n > 2 ^ n := by
  intros
  by_cases h : n = 4
  . rw [h]
    simp [Nat.factorial]
  . induction n with
    | zero =>
      exfalso
      contradiction
    | succ nn ih =>
      simp [Nat.factorial]
      rw [Nat.pow_succ, Nat.mul_comm]
      refine Nat.mul_lt_mul_of_le_of_lt' ?succ.hac ?succ.hbd ?succ.ha

I can't get either of the first two subgoals, even though I know how I would prove them on paper (the first one is relatively straightforward, for the second just use the inductive hypothesis). Any help on how to express it in Lean? Thanks in advance!

[Ruben Van de Velde]

It does not appear provable at this point, because the induction hypothesis is too weak

[Ruben Van de Velde]

Instead, you can use Nat.le_induction:

import Mathlib
theorem factorial_power2 (n : ℕ) (hn : 4 <= n) : Nat.factorial n > 2 ^ n := by
  induction n, hn using Nat.le_induction with
  | base => simp [Nat.factorial]
  | succ n hn ih =>
    simp [Nat.factorial]
    rw [Nat.pow_succ, Nat.mul_comm]
    refine Nat.mul_lt_mul_of_le_of_lt' ?succ.hac ?succ.hbd ?succ.ha
    all_goals sorry

[Vincent Beffara]

Or you can do this (where ih is strong enough):

example {n : ℕ} : 2 ^ (n + 4) ≤ (n + 4).factorial := by
  induction n with
  | zero => simp [Nat.factorial]
  | succ n ih =>
    sorry

[Vincent Beffara]

Spoiler

example {n : ℕ} : 2 ^ (n + 4) ≤ (n + 4).factorial := by
induction n with
| zero => simp [Nat.factorial]
| succ n ih =>
rw [Nat.factorial_succ, pow_succ']
gcongr ; linarith

[James Li]

Thanks, didn't realize there was le_induction! I'm still stuck at this last part of the proof... it should be trivial but I'm not sure what the right tactic is. "simp" doesn't work, and I remember there used to be "ring" but it doesn't seem to be a valid tactic anymore! What's the right way to finish it off?

hn : 4 ≤ n
ih : Nat.factorial n > 2 ^ n
⊢ 1 ≤ n

[Kevin Buzzard]

ring is a valid tactic (did you import Mathlib.Tactic?) but what you need here is linarith or omega.

[Chris Wong]

If you want to prove it by hand, there is also docs#le_trans.