Theorem: fermat_odd (FormalBook/Chapter_01.lean)

State before:
n : ℕ
⊢ Odd (F n)
Tactic:
rw [F, odd_iff_not_even, even_add_one, not_not, even_pow]
State after:
n : ℕ
⊢ Even 2 ∧ 2 ^ n ≠ 0

State before:
n : ℕ
⊢ Even 2 ∧ 2 ^ n ≠ 0
Tactic:
refine' ⟨even_two, Nat.ne_of_gt (pow_pos _ _)⟩
State after:
n : ℕ
⊢ 0 < 2

State before:
n : ℕ
⊢ 0 < 2
Tactic:
exact zero_lt_two
State after:
no goals