Proving that n < 2^(n+1) for a natural number n

Stream: new members

[Colin Jones ⚛️]

Is there a more efficient way to prove this statement?

import Mathlib

open Nat

example (n : ℕ) : n < 2^(n+1) := by
  have h2 : 1 < 2^(n+1) := by
    induction n
    norm_num
    rename_i n hn
    rw [Nat.succ_eq_add_one]
    calc
      1 < 2^(n+1) := by exact hn
      _ < 2^(n+1+1) := by exact Nat.pow_lt_pow_succ le.refl (n + 1)
  have hn : n < 2^(n+1) := by
    induction n
    norm_num
    rename_i n hn
    rw [Nat.succ_eq_add_one, two_pow_succ]
    have hn' : n < 2 ^ (n + 1) := by simp_all only [ne_eq, add_eq_zero, one_ne_zero, and_false, not_false_eq_true,
                                       Nat.one_lt_pow_iff, lt_succ_self, forall_true_left, succ_ne_zero, and_self]
    have h2' : 1 < 2 ^ (n + 1) := by simp_all only [ne_eq, add_eq_zero, one_ne_zero, and_false, not_false_eq_true,
                                       Nat.one_lt_pow_iff, lt_succ_self, forall_true_left, succ_ne_zero, and_self]
    rel [hn', h2']
  exact hn

[Yaël Dillies]

Do you count knowing the existence of docs#Nat.lt_two_pow as cheating? :grinning:

[Colin Jones ⚛️]

Lol that would work. Thanks! For some reason aesop? and apply? didn't show this option to me.

[Damiano Testa]

Here is a possible explanation of why aesop and apply? failed you:

import Mathlib

open Nat

example (n : ℕ) : n < 2^(n+1) := by
  trans (n + 1) <;>  -- creative human input: computers will never beat humans at math...
  apply?  -- this now works