[GOAL]
n : ℕ
⊢ ↑n = 1 ↔ Odd n
[PROOFSTEP]
rw [← @Nat.cast_one (ZMod 2), ZMod.eq_iff_modEq_nat, Nat.odd_iff, Nat.ModEq]
[GOAL]
n : ℕ
⊢ n % 2 = 1 % 2 ↔ n % 2 = 1
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ ↑n ≠ 0 ↔ Odd n
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
⊢ ↑n ≠ 0 → Odd n
[PROOFSTEP]
contrapose
[GOAL]
case mp
n : ℕ
⊢ ¬Odd n → ¬↑n ≠ 0
[PROOFSTEP]
simp [eq_zero_iff_even]
[GOAL]
case mpr
n : ℕ
⊢ Odd n → ↑n ≠ 0
[PROOFSTEP]
contrapose
[GOAL]
case mpr
n : ℕ
⊢ ¬↑n ≠ 0 → ¬Odd n
[PROOFSTEP]
simp [eq_zero_iff_even]
