[GOAL]
m n : ℤ
⊢ ¬n % 2 = 1 ↔ n % 2 = 0
[PROOFSTEP]
cases' emod_two_eq_zero_or_one n with h h
[GOAL]
case inl
m n : ℤ
h : n % 2 = 0
⊢ ¬n % 2 = 1 ↔ n % 2 = 0
[PROOFSTEP]
simp [h]
[GOAL]
case inr
m n : ℤ
h : n % 2 = 1
⊢ ¬n % 2 = 1 ↔ n % 2 = 0
[PROOFSTEP]
simp [h]
[GOAL]
m n : ℤ
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
[PROOFSTEP]
cases' emod_two_eq_zero_or_one n with h h
[GOAL]
case inl
m n : ℤ
h : n % 2 = 0
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
[PROOFSTEP]
simp [h]
[GOAL]
case inr
m n : ℤ
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
[PROOFSTEP]
simp [h]
[GOAL]
m✝ n : ℤ
x✝ : Even n
m : ℤ
hm : n = m + m
⊢ n % 2 = 0
[PROOFSTEP]
simp [← two_mul, hm]
[GOAL]
m n : ℤ
h : n % 2 = 0
⊢ n % 2 + 2 * (n / 2) = n / 2 + n / 2
[PROOFSTEP]
simp [← two_mul, h]
[GOAL]
m✝ n : ℤ
x✝ : Odd n
m : ℤ
hm : n = 2 * m + 1
⊢ n % 2 = 1
[PROOFSTEP]
rw [hm, add_emod]
[GOAL]
m✝ n : ℤ
x✝ : Odd n
m : ℤ
hm : n = 2 * m + 1
⊢ (2 * m % 2 + 1 % 2) % 2 = 1
[PROOFSTEP]
norm_num
[GOAL]
m n : ℤ
h : n % 2 = 1
⊢ n % 2 + 2 * (n / 2) = 2 * (n / 2) + 1
[PROOFSTEP]
rw [h]
[GOAL]
m n : ℤ
h : n % 2 = 1
⊢ 1 + 2 * (n / 2) = 2 * (n / 2) + 1
[PROOFSTEP]
abel
[GOAL]
m n : ℤ
h : n % 2 = 1
⊢ 1 + 2 * (n / 2) = 2 * (n / 2) + 1
[PROOFSTEP]
abel
[GOAL]
m n : ℤ
⊢ ¬Even n ↔ n % 2 = 1
[PROOFSTEP]
rw [even_iff, emod_two_ne_zero]
[GOAL]
m n : ℤ
⊢ ¬Odd n ↔ n % 2 = 0
[PROOFSTEP]
rw [odd_iff, emod_two_ne_one]
[GOAL]
m n : ℤ
⊢ Even n ↔ ¬Odd n
[PROOFSTEP]
rw [not_odd_iff, even_iff]
[GOAL]
m n : ℤ
⊢ Odd n ↔ ¬Even n
[PROOFSTEP]
rw [not_even_iff, odd_iff]
[GOAL]
m n : ℤ
⊢ IsCompl {n | Even n} {n | Odd n}
[PROOFSTEP]
simp [← Set.compl_setOf, isCompl_compl]
[GOAL]
m n✝ n : ℤ
⊢ ∃ k, n = 2 * k ∨ n = 2 * k + 1
[PROOFSTEP]
simpa only [two_mul, exists_or, Odd, Even] using even_or_odd n
[GOAL]
m n✝ n : ℤ
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]
cases even_or_odd n with
| inl h => exact Or.inl ⟨h, even_iff_not_odd.mp h⟩
| inr h => exact Or.inr ⟨h, odd_iff_not_even.mp h⟩
[GOAL]
m n✝ n : ℤ
x✝ : Even n ∨ Odd n
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]
cases even_or_odd n with
| inl h => exact Or.inl ⟨h, even_iff_not_odd.mp h⟩
| inr h => exact Or.inr ⟨h, odd_iff_not_even.mp h⟩
[GOAL]
case inl
m n✝ n : ℤ
h : Even n
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]

| inl h => exact Or.inl ⟨h, even_iff_not_odd.mp h⟩
[GOAL]
case inl
m n✝ n : ℤ
h : Even n
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]
exact Or.inl ⟨h, even_iff_not_odd.mp h⟩
[GOAL]
case inr
m n✝ n : ℤ
h : Odd n
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]

| inr h => exact Or.inr ⟨h, odd_iff_not_even.mp h⟩
[GOAL]
case inr
m n✝ n : ℤ
h : Odd n
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]
exact Or.inr ⟨h, odd_iff_not_even.mp h⟩
[GOAL]
m n✝ n : ℤ
⊢ ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)
[PROOFSTEP]
rcases even_or_odd n with (⟨k, rfl⟩ | ⟨k, rfl⟩)
[GOAL]
case inl.intro
m n k : ℤ
⊢ ∃ k_1, Xor' (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)
[PROOFSTEP]
use k
[GOAL]
case inr.intro
m n k : ℤ
⊢ ∃ k_1, Xor' (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
[PROOFSTEP]
use k
[GOAL]
case h
m n k : ℤ
⊢ Xor' (k + k = 2 * k) (k + k = 2 * k + 1)
[PROOFSTEP]
simpa only [← two_mul, Xor', true_and_iff, eq_self_iff_true, not_true, or_false_iff, and_false_iff] using
  (succ_ne_self (2 * k)).symm
[GOAL]
case h
m n k : ℤ
⊢ Xor' (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
[PROOFSTEP]
simp only [Xor', add_right_eq_self, false_or_iff, eq_self_iff_true, not_true, not_false_iff, one_ne_zero, and_self_iff]
[GOAL]
m n : ℤ
⊢ ¬Even 1
[PROOFSTEP]
rw [even_iff]
[GOAL]
m n : ℤ
⊢ ¬1 % 2 = 0
[PROOFSTEP]
norm_num
[GOAL]
m n : ℤ
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
cases' emod_two_eq_zero_or_one m with h₁ h₁
[GOAL]
case inl
m n : ℤ
h₁ : m % 2 = 0
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
cases' emod_two_eq_zero_or_one n with h₂ h₂
[GOAL]
case inr
m n : ℤ
h₁ : m % 2 = 1
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
cases' emod_two_eq_zero_or_one n with h₂ h₂
[GOAL]
case inl.inl
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.add_emod]
[GOAL]
case inl.inr
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.add_emod]
[GOAL]
case inr.inl
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.add_emod]
[GOAL]
case inr.inr
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.add_emod]
[GOAL]
m n : ℤ
⊢ Even (m + n) ↔ (Odd m ↔ Odd n)
[PROOFSTEP]
rw [even_add, even_iff_not_odd, even_iff_not_odd, not_iff_not]
[GOAL]
m n✝ n : ℤ
⊢ ¬Even (bit1 n)
[PROOFSTEP]
simp [bit1, parity_simps]
[GOAL]
m n✝ n : ℤ
⊢ ¬2 ∣ 2 * n + 1
[PROOFSTEP]
simp [add_emod]
[GOAL]
m n : ℤ
⊢ Even (m - n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
simp [sub_eq_add_neg, parity_simps]
[GOAL]
m n : ℤ
⊢ Even (m - n) ↔ (Odd m ↔ Odd n)
[PROOFSTEP]
rw [even_sub, even_iff_not_odd, even_iff_not_odd, not_iff_not]
[GOAL]
m n : ℤ
⊢ Even (n + 1) ↔ ¬Even n
[PROOFSTEP]
simp [even_add]
[GOAL]
m n : ℤ
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
cases' emod_two_eq_zero_or_one m with h₁ h₁
[GOAL]
case inl
m n : ℤ
h₁ : m % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
cases' emod_two_eq_zero_or_one n with h₂ h₂
[GOAL]
case inr
m n : ℤ
h₁ : m % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
cases' emod_two_eq_zero_or_one n with h₂ h₂
[GOAL]
case inl.inl
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.mul_emod]
[GOAL]
case inl.inr
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.mul_emod]
[GOAL]
case inr.inl
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.mul_emod]
[GOAL]
case inr.inr
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
simp [even_iff, h₁, h₂, Int.mul_emod]
[GOAL]
m n : ℤ
⊢ Odd (m * n) ↔ Odd m ∧ Odd n
[PROOFSTEP]
simp [not_or, parity_simps]
[GOAL]
m n✝ : ℤ
n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
m n : ℤ
⊢ Even (m ^ Nat.zero) ↔ Even m ∧ Nat.zero ≠ 0
[PROOFSTEP]
simp [*, even_mul, pow_succ]
[GOAL]
case succ
m n✝ : ℤ
n : ℕ
ih : Even (m ^ n) ↔ Even m ∧ n ≠ 0
⊢ Even (m ^ Nat.succ n) ↔ Even m ∧ Nat.succ n ≠ 0
[PROOFSTEP]
simp [*, even_mul, pow_succ]
[GOAL]
case succ
m n✝ : ℤ
n : ℕ
ih : Even (m ^ n) ↔ Even m ∧ n ≠ 0
⊢ Even m → ¬n = 0 → Even m
[PROOFSTEP]
tauto
[GOAL]
m n✝ : ℤ
n : ℕ
⊢ Odd (m ^ n) ↔ Odd m ∨ n = 0
[PROOFSTEP]
rw [← not_iff_not, ← Int.even_iff_not_odd, not_or, ← Int.even_iff_not_odd, Int.even_pow]
[GOAL]
m n : ℤ
⊢ Odd (m + n) ↔ (Odd m ↔ Even n)
[PROOFSTEP]
rw [odd_iff_not_even, even_add, not_iff, odd_iff_not_even]
[GOAL]
m n : ℤ
⊢ Odd (m + n) ↔ (Odd n ↔ Even m)
[PROOFSTEP]
rw [add_comm, odd_add]
[GOAL]
m n : ℤ
h : Odd (m + n)
hnot : m = n
⊢ False
[PROOFSTEP]
simp [hnot, parity_simps] at h 
[GOAL]
m n : ℤ
⊢ Odd (m - n) ↔ (Odd m ↔ Even n)
[PROOFSTEP]
rw [odd_iff_not_even, even_sub, not_iff, odd_iff_not_even]
[GOAL]
m n : ℤ
⊢ Odd (m - n) ↔ (Odd n ↔ Even m)
[PROOFSTEP]
rw [odd_iff_not_even, even_sub, not_iff, not_iff_comm, odd_iff_not_even]
[GOAL]
m n✝ n : ℤ
⊢ Even (n * (n + 1))
[PROOFSTEP]
simpa [even_mul, parity_simps] using n.even_or_odd
[GOAL]
m n✝ : ℤ
n : ℕ
⊢ Even ↑n ↔ Even n
[PROOFSTEP]
rw_mod_cast [even_iff, Nat.even_iff]
[GOAL]
m n✝ : ℤ
n : ℕ
⊢ Odd ↑n ↔ Odd n
[PROOFSTEP]
rw [odd_iff_not_even, Nat.odd_iff_not_even, even_coe_nat]
[GOAL]
m n : ℤ
⊢ Even (natAbs n) ↔ Even n
[PROOFSTEP]
simp [even_iff_two_dvd, dvd_natAbs, coe_nat_dvd_left.symm]
[GOAL]
m n : ℤ
⊢ Odd (natAbs n) ↔ Odd n
[PROOFSTEP]
rw [odd_iff_not_even, Nat.odd_iff_not_even, natAbs_even]
[GOAL]
m n a b : ℤ
ha : Odd a
hb : Odd b
⊢ 4 ∣ a + b ∨ 4 ∣ a - b
[PROOFSTEP]
obtain ⟨m, rfl⟩ := ha
[GOAL]
case intro
m✝ n b : ℤ
hb : Odd b
m : ℤ
⊢ 4 ∣ 2 * m + 1 + b ∨ 4 ∣ 2 * m + 1 - b
[PROOFSTEP]
obtain ⟨n, rfl⟩ := hb
[GOAL]
case intro.intro
m✝ n✝ m n : ℤ
⊢ 4 ∣ 2 * m + 1 + (2 * n + 1) ∨ 4 ∣ 2 * m + 1 - (2 * n + 1)
[PROOFSTEP]
obtain h | h := Int.even_or_odd (m + n)
[GOAL]
case intro.intro.inl
m✝ n✝ m n : ℤ
h : Even (m + n)
⊢ 4 ∣ 2 * m + 1 + (2 * n + 1) ∨ 4 ∣ 2 * m + 1 - (2 * n + 1)
[PROOFSTEP]
right
[GOAL]
case intro.intro.inl.h
m✝ n✝ m n : ℤ
h : Even (m + n)
⊢ 4 ∣ 2 * m + 1 - (2 * n + 1)
[PROOFSTEP]
rw [Int.even_add, ← Int.even_sub] at h 
[GOAL]
case intro.intro.inl.h
m✝ n✝ m n : ℤ
h : Even (m - n)
⊢ 4 ∣ 2 * m + 1 - (2 * n + 1)
[PROOFSTEP]
obtain ⟨k, hk⟩ := h
[GOAL]
case intro.intro.inl.h.intro
m✝ n✝ m n k : ℤ
hk : m - n = k + k
⊢ 4 ∣ 2 * m + 1 - (2 * n + 1)
[PROOFSTEP]
convert dvd_mul_right 4 k using 1
[GOAL]
case h.e'_4
m✝ n✝ m n k : ℤ
hk : m - n = k + k
⊢ 2 * m + 1 - (2 * n + 1) = 4 * k
[PROOFSTEP]
rw [eq_add_of_sub_eq hk, mul_add, add_assoc, add_sub_cancel, ← two_mul, ← mul_assoc]
[GOAL]
case h.e'_4
m✝ n✝ m n k : ℤ
hk : m - n = k + k
⊢ 2 * 2 * k = 4 * k
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.inr
m✝ n✝ m n : ℤ
h : Odd (m + n)
⊢ 4 ∣ 2 * m + 1 + (2 * n + 1) ∨ 4 ∣ 2 * m + 1 - (2 * n + 1)
[PROOFSTEP]
left
[GOAL]
case intro.intro.inr.h
m✝ n✝ m n : ℤ
h : Odd (m + n)
⊢ 4 ∣ 2 * m + 1 + (2 * n + 1)
[PROOFSTEP]
obtain ⟨k, hk⟩ := h
[GOAL]
case intro.intro.inr.h.intro
m✝ n✝ m n k : ℤ
hk : m + n = 2 * k + 1
⊢ 4 ∣ 2 * m + 1 + (2 * n + 1)
[PROOFSTEP]
convert dvd_mul_right 4 (k + 1) using 1
[GOAL]
case h.e'_4
m✝ n✝ m n k : ℤ
hk : m + n = 2 * k + 1
⊢ 2 * m + 1 + (2 * n + 1) = 4 * (k + 1)
[PROOFSTEP]
rw [eq_sub_of_add_eq hk, add_right_comm, ← add_sub, mul_add, mul_sub, add_assoc, add_assoc, sub_add, add_assoc, ←
  sub_sub (2 * n), sub_self, zero_sub, sub_neg_eq_add, ← mul_assoc, mul_add]
[GOAL]
case h.e'_4
m✝ n✝ m n k : ℤ
hk : m + n = 2 * k + 1
⊢ 2 * 2 * k + (2 * 1 + (1 + 1)) = 4 * k + 4 * 1
[PROOFSTEP]
rfl
[GOAL]
m n : ℤ
⊢ Odd n → 2 * (n / 2) + 1 = n
[PROOFSTEP]
rintro ⟨c, rfl⟩
[GOAL]
case intro
m c : ℤ
⊢ 2 * ((2 * c + 1) / 2) + 1 = 2 * c + 1
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case intro
m c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1
[PROOFSTEP]
convert Int.ediv_add_emod' (2 * c + 1) 2
[GOAL]
case h.e'_2.h.e'_6
m c : ℤ
⊢ 1 = (2 * c + 1) % 2
[PROOFSTEP]
simp [Int.add_emod]
[GOAL]
m n : ℤ
⊢ Odd n → n / 2 * 2 + 1 = n
[PROOFSTEP]
rintro ⟨c, rfl⟩
[GOAL]
case intro
m c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1
[PROOFSTEP]
convert Int.ediv_add_emod' (2 * c + 1) 2
[GOAL]
case h.e'_2.h.e'_6
m c : ℤ
⊢ 1 = (2 * c + 1) % 2
[PROOFSTEP]
simp [Int.add_emod]
[GOAL]
m n : ℤ
⊢ Odd n → 1 + n / 2 * 2 = n
[PROOFSTEP]
rintro ⟨c, rfl⟩
[GOAL]
case intro
m c : ℤ
⊢ 1 + (2 * c + 1) / 2 * 2 = 2 * c + 1
[PROOFSTEP]
rw [add_comm]
[GOAL]
case intro
m c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1
[PROOFSTEP]
convert Int.ediv_add_emod' (2 * c + 1) 2
[GOAL]
case h.e'_2.h.e'_6
m c : ℤ
⊢ 1 = (2 * c + 1) % 2
[PROOFSTEP]
simp [Int.add_emod]
[GOAL]
m✝ n✝ m n : ℤ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (m ^ 2 + m + n)
[PROOFSTEP]
simp [*, (by decide : ¬2 = 0), parity_simps]
[GOAL]
m✝ n✝ m n : ℤ
h : Even m
⊢ ¬2 = 0
[PROOFSTEP]
decide
[GOAL]
m n : ℤ
⊢ ¬Even 25394535
[PROOFSTEP]
simp
