Theorem: F₀ (FormalBook/Chapter_01.lean)

State before:
⊢ F 0 = 3
Tactic:
rw [F]
State after:
⊢ 2 ^ 2 ^ 0 + 1 = 3

State before:
⊢ 2 ^ 2 ^ 0 + 1 = 3
Tactic:
simp only [Nat.pow_zero, pow_one]
State after:
no goals