Theorem: fermat_bounded (FormalBook/Chapter_01.lean)

State before:
n : ℕ
⊢ 2 < F n
Tactic:
induction' n with n h
State after:
case zero

⊢ 2 < F 0

case succ
n : ℕ
h : 2 < F n
⊢ 2 < F (n + 1)

State before:
case zero

⊢ 2 < F 0
Tactic:
rw [F₀]
State after:
case zero

⊢ 2 < 3

State before:
case zero

⊢ 2 < 3
Tactic:
norm_num
State after:
no goals

State before:
case succ
n : ℕ
h : 2 < F n
⊢ 2 < F (n + 1)
Tactic:
exact lt_trans h fermat_stricly_monotone
State after:
no goals