Theorem: ZerosOnesAndTwos.even_5_pow_plus_one (Compfiles/ZeroesOnesAndTwos.lean)

State before:
n : ℕ
⊢ 2 ∣ 5 ^ n + 1
Tactic:
apply Nat.dvd_of_mod_eq_zero
State after:
case H
n : ℕ
⊢ (5 ^ n + 1) % 2 = 0

State before:
case H
n : ℕ
⊢ (5 ^ n + 1) % 2 = 0
Tactic:
rw [Nat.add_mod, Nat.pow_mod]
State after:
case H
n : ℕ
⊢ ((5 % 2) ^ n % 2 + 1 % 2) % 2 = 0

State before:
case H
n : ℕ
⊢ ((5 % 2) ^ n % 2 + 1 % 2) % 2 = 0
Tactic:
norm_num
State after:
no goals