Theorem: fermat_stricly_monotone (FormalBook/Chapter_01.lean)

State before:
n : ℕ
⊢ F n < F n.succ
Tactic:
have : NeZero 1 := by infer_instance
State after:
n : ℕ
this : NeZero 1
⊢ F n < F n.succ

State before:
n : ℕ
this : NeZero 1
⊢ F n < F n.succ
Tactic:
rw [F, F]
State after:
n : ℕ
this : NeZero 1
⊢ 2 ^ 2 ^ n + 1 < 2 ^ 2 ^ n.succ + 1

State before:
n : ℕ
this : NeZero 1
⊢ 2 ^ 2 ^ n + 1 < 2 ^ 2 ^ n.succ + 1
Tactic:
simp only [add_lt_add_iff_right, Nat.pow_succ]
State after:
n : ℕ
this : NeZero 1
⊢ 2 ^ 2 ^ n < 2 ^ (2 ^ n * 2)

State before:
n : ℕ
this : NeZero 1
⊢ 2 ^ 2 ^ n < 2 ^ (2 ^ n * 2)
Tactic:
refine' (pow_lt_pow_iff_right one_lt_two).mpr _
State after:
n : ℕ
this : NeZero 1
⊢ 2 ^ n < 2 ^ n * 2

State before:
n : ℕ
this : NeZero 1
⊢ 2 ^ n < 2 ^ n * 2
Tactic:
norm_num
State after:
no goals

State before:
n : ℕ
⊢ NeZero 1
Tactic:
infer_instance
State after:
no goals