Theorem: succLtTwoPow (FromTheBook/Ch02/Bertrand/Bertrand.lean)

State before:
a : ℕ
h2 : 2 ≤ a
⊢ Nat.succ a < 2 ^ a
Tactic:
replace h2 := Nat.exists_eq_add_of_le h2
State after:
a : ℕ
h2 : ∃ k, a = 2 + k
⊢ Nat.succ a < 2 ^ a

State before:
a : ℕ
h2 : ∃ k, a = 2 + k
⊢ Nat.succ a < 2 ^ a
Tactic:
cases h2 with | intro u hu =>
rw [hu]
clear a hu
induction u with
| zero => simp
| succ u h =>
  rw [Nat.add_succ, Nat.pow_succ, Nat.mul_two]
  rw [← Nat.add_one]
  apply Nat.add_lt_add h
  apply Nat.one_lt_pow <;> linarith
State after:
no goals

State before:
case intro
a u : ℕ
hu : a = 2 + u
⊢ Nat.succ a < 2 ^ a
Tactic:
rw [hu]
State after:
case intro
a u : ℕ
hu : a = 2 + u
⊢ Nat.succ (2 + u) < 2 ^ (2 + u)

State before:
case intro
a u : ℕ
hu : a = 2 + u
⊢ Nat.succ (2 + u) < 2 ^ (2 + u)
Tactic:
clear a hu
State after:
case intro
u : ℕ
⊢ Nat.succ (2 + u) < 2 ^ (2 + u)

State before:
case intro
u : ℕ
⊢ Nat.succ (2 + u) < 2 ^ (2 + u)
Tactic:
induction u with
| zero => simp
| succ u h =>
  rw [Nat.add_succ, Nat.pow_succ, Nat.mul_two]
  rw [← Nat.add_one]
  apply Nat.add_lt_add h
  apply Nat.one_lt_pow <;> linarith
State after:
no goals

State before:
case intro.zero

⊢ Nat.succ (2 + Nat.zero) < 2 ^ (2 + Nat.zero)
Tactic:
simp
State after:
no goals

State before:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ Nat.succ (2 + Nat.succ u) < 2 ^ (2 + Nat.succ u)
Tactic:
rw [Nat.add_succ, Nat.pow_succ, Nat.mul_two]
State after:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ Nat.succ (Nat.succ (2 + u)) < 2 ^ (2 + u) + 2 ^ (2 + u)

State before:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ Nat.succ (Nat.succ (2 + u)) < 2 ^ (2 + u) + 2 ^ (2 + u)
Tactic:
rw [← Nat.add_one]
State after:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ 2 + u + 1 + 1 < 2 ^ (2 + u) + 2 ^ (2 + u)

State before:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ 2 + u + 1 + 1 < 2 ^ (2 + u) + 2 ^ (2 + u)
Tactic:
apply Nat.add_lt_add h
State after:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ 1 < 2 ^ (2 + u)

State before:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ 1 < 2 ^ (2 + u)
Tactic:
apply Nat.one_lt_pow <;> linarith
State after:
no goals