Is there a shorter way to solve task

Stream: new members

[Boris]

Hello, I'm new to Lean 4, so I'm trying to solve some simple tasks right now. Today I proved that $n! < (n+1)^n$ and I ran into the problem that my assumption ($1 \le n$), after applying induction, is rewritten into ($1 \le n+1$). Can you please tell me if there is a way to write down this proof in a shorter way?

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

theorem factorial_pow (n : ℕ) (hn : 1 ≤ n) : Nat.factorial n < (n+1)^n := by
  induction n with
  | zero => cases hn
  | succ n ih =>
    by_cases hn_eq_zero : n = 0
    · -- case n = 0
      subst hn_eq_zero
      simp [Nat.factorial]
    · -- case n ≥ 1
      rw [Nat.succ_eq_add_one] at *
      specialize ih (Nat.pos_of_ne_zero hn_eq_zero)
      -- adding new theorem for (0 < n+1)
      have h_zero_lt : 0 < n+1 := Nat.succ_le_iff.mp hn
      -- final theorem proving steps
      calc
      Nat.factorial (n+1) = (n+1) * Nat.factorial n := by rw [Nat.factorial_succ]
      _ < (n+1) * (n+1) ^ n := by
        apply (mul_lt_mul_left h_zero_lt).2 ih
      _ = (n+1) ^ (n+1) := by rw [← pow_succ]
      _ < (n+1+1) ^ (n+1) := by
        apply Nat.pow_lt_pow_of_lt_left
        · exact Nat.lt_succ_self (n + 1)
        · exact h_zero_lt

[Henrik Böving]

I ran into the problem that my assumption ($1 \le n$), after applying induction, is rewritten into ($1 \le n+1$).

what else did you expect to happen?

[Notification Bot]

This topic was moved here from #lean4 > Is there a shorter way to solve task by Kevin Buzzard.

[Kevin Buzzard]

@Boris your question is not about core Lean but about definitions in mathlib so I've moved it to a more appropriate channel. You might also want to consider changing the title to something more helpful. You might also want to consider editing your post so that it becomes a #mwe -- right now there are missing imports, and when I add them I get other errors.

[Boris]

Henrik Böving said:

what else did you expect to happen?

I expected that I would still have the original hn theorem, which I could apply without dividing n into cases 0 and ≥ 1. I don't understand why Lean changes it?

[Henrik Böving]

That's just how induction works in pen and paper mathematics as well, if you do induction on some variable n it won't only change in the thing you are trying to prove but also all your assumptions.

[Yiming Fu]

Boris said:

Henrik Böving said:

what else did you expect to happen?

I expected that I would still have the original hn theorem, which I could apply without dividing n into cases 0 and ≥ 1. I don't understand why Lean changes it?

I guess you mean doing induction on n starting from n = 1?

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

theorem factorial_pow (n : ℕ) (hn : 1 ≤ n) : Nat.factorial n < (n+1)^n := by
  induction n, hn using Nat.le_induction with
  | base => simp
  | succ n hmn ih => sorry