[GOAL]
m n : ℕ
⊢ ¬n % 2 = 1 ↔ n % 2 = 0
[PROOFSTEP]
cases' mod_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' mod_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_mod, mul_mod_right]
[GOAL]
m✝ n : ℕ
x✝ : Odd n
m : ℕ
hm : n = 2 * m + 1
⊢ (0 + 1 % 2) % 2 = 1
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
h : n % 2 = 1
⊢ n % 2 + 2 * (n / 2) = 2 * (n / 2) + 1
[PROOFSTEP]
rw [h, add_comm]
[GOAL]
m n : ℕ
⊢ ¬Even n ↔ n % 2 = 1
[PROOFSTEP]
rw [even_iff, mod_two_ne_zero]
[GOAL]
m n : ℕ
⊢ ¬Odd n ↔ n % 2 = 0
[PROOFSTEP]
rw [odd_iff, mod_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 : ℕ
h : Odd n
⊢ ¬2 ∣ n
[PROOFSTEP]
rwa [← even_iff_two_dvd, ← odd_iff_not_even]
[GOAL]
m n : ℕ
⊢ IsCompl {n | Even n} {n | Odd n}
[PROOFSTEP]
simp only [← Set.compl_setOf, isCompl_compl, odd_iff_not_even]
[GOAL]
m n✝ n : ℕ
⊢ Xor' (Even n) (Odd n)
[PROOFSTEP]
simp [Xor', odd_iff_not_even, Decidable.em (Even n)]
[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 : ℕ
⊢ ∃ 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, eq_self_iff_true, xor_true] 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]
simpa only [xor_true, xor_comm] using (succ_ne_self _)
[GOAL]
m✝ n✝ m n : ℕ
hn : Odd n
hm : Even m
⊢ m % 2 + (m + n) % 2 = 1
[PROOFSTEP]
rw [even_iff.1 hm, odd_iff.1 (hm.add_odd hn)]
[GOAL]
m✝ n✝ m n : ℕ
hn : Odd n
hm : Odd m
⊢ m % 2 + (m + n) % 2 = 1
[PROOFSTEP]
rw [odd_iff.1 hm, even_iff.1 (hm.add_odd hn)]
[GOAL]
m✝ n m : ℕ
⊢ (m + 1) % 2 + m % 2 = 1
[PROOFSTEP]
rw [add_comm, mod_two_add_succ_mod_two]
[GOAL]
m n : ℕ
⊢ Even (m + n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
cases' mod_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' mod_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' mod_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₂, Nat.add_mod]
[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₂, Nat.add_mod]
[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₂, Nat.add_mod]
[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₂, Nat.add_mod]
[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 : ℕ
⊢ Even (n + 1) ↔ ¬Even n
[PROOFSTEP]
simp [even_add]
[GOAL]
m n✝ n : ℕ
⊢ ¬Even (bit1 n)
[PROOFSTEP]
simp [bit1, parity_simps]
[GOAL]
m n✝ n : ℕ
⊢ ¬2 ∣ 2 * n + 1
[PROOFSTEP]
simp [add_mod]
[GOAL]
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ (Even m ↔ Even n)
[PROOFSTEP]
conv_rhs => rw [← tsub_add_cancel_of_le h, even_add]
[GOAL]
m n : ℕ
h : n ≤ m
| Even m ↔ Even n
[PROOFSTEP]
rw [← tsub_add_cancel_of_le h, even_add]
[GOAL]
m n : ℕ
h : n ≤ m
| Even m ↔ Even n
[PROOFSTEP]
rw [← tsub_add_cancel_of_le h, even_add]
[GOAL]
m n : ℕ
h : n ≤ m
| Even m ↔ Even n
[PROOFSTEP]
rw [← tsub_add_cancel_of_le h, even_add]
[GOAL]
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ ((Even (m - n) ↔ Even n) ↔ Even n)
[PROOFSTEP]
by_cases h : Even n
[GOAL]
case pos
m n : ℕ
h✝ : n ≤ m
h : Even n
⊢ Even (m - n) ↔ ((Even (m - n) ↔ Even n) ↔ Even n)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
m n : ℕ
h✝ : n ≤ m
h : ¬Even n
⊢ Even (m - n) ↔ ((Even (m - n) ↔ Even n) ↔ Even n)
[PROOFSTEP]
simp [h]
[GOAL]
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ (Odd m ↔ Odd n)
[PROOFSTEP]
rw [even_sub h, even_iff_not_odd, even_iff_not_odd, not_iff_not]
[GOAL]
m n : ℕ
hm : Odd m
hn : Odd n
h : n ≤ m
⊢ Even (m - n)
[PROOFSTEP]
simp only [even_sub' h, *]
[GOAL]
m n : ℕ
hm : Odd m
hn : Odd n
h : m ≤ n
⊢ Even (m - n)
[PROOFSTEP]
simp only [tsub_eq_zero_iff_le.mpr h, even_zero]
[GOAL]
m n : ℕ
⊢ Even (m * n) ↔ Even m ∨ Even n
[PROOFSTEP]
cases' mod_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' mod_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' mod_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₂, Nat.mul_mod]
[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₂, Nat.mul_mod]
[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₂, Nat.mul_mod]
[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₂, Nat.mul_mod]
[GOAL]
m n : ℕ
⊢ Odd (m * n) ↔ Odd m ∧ Odd n
[PROOFSTEP]
simp [not_or, even_mul]
[GOAL]
m n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
m n : ℕ
⊢ Even (m ^ zero) ↔ Even m ∧ zero ≠ 0
[PROOFSTEP]
simp (config := { contextual := true }) [*, pow_succ', even_mul]
[GOAL]
case succ
m n✝ n : ℕ
ih : Even (m ^ n) ↔ Even m ∧ n ≠ 0
⊢ Even (m ^ succ n) ↔ Even m ∧ succ n ≠ 0
[PROOFSTEP]
simp (config := { contextual := true }) [*, pow_succ', even_mul]
[GOAL]
m n : ℕ
⊢ Even (m / n) ↔ m % (2 * n) / n = 0
[PROOFSTEP]
rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, Nat.div_mod_eq_mod_mul_div, mul_comm]
[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] at h 
[GOAL]
m n : ℕ
h : n ≤ m
⊢ Odd (m - n) ↔ (Odd m ↔ Even n)
[PROOFSTEP]
rw [odd_iff_not_even, even_sub h, not_iff, odd_iff_not_even]
[GOAL]
m n : ℕ
h : n ≤ m
⊢ Odd (m - n) ↔ (Odd n ↔ Even m)
[PROOFSTEP]
rw [odd_iff_not_even, even_sub h, not_iff, not_iff_comm, odd_iff_not_even]
[GOAL]
m n✝ n : ℕ
⊢ Even (n * (n + 1))
[PROOFSTEP]
rw [even_mul, even_add_one]
[GOAL]
m n✝ n : ℕ
⊢ Even n ∨ ¬Even n
[PROOFSTEP]
exact em _
[GOAL]
m n : ℕ
h : Odd n
⊢ 2 * (n / 2) + 1 = n
[PROOFSTEP]
rw [← odd_iff.mp h, div_add_mod]
[GOAL]
m n : ℕ
h : Odd n
⊢ n / 2 * 2 + 1 = n
[PROOFSTEP]
rw [← odd_iff.mp h, div_add_mod']
[GOAL]
m n : ℕ
h : Odd n
⊢ 1 + n / 2 * 2 = n
[PROOFSTEP]
rw [← odd_iff.mp h, mod_add_div']
[GOAL]
m n : ℕ
⊢ bit0 n / 2 = n
[PROOFSTEP]
rw [← Nat.bit0_eq_bit0, bit0_eq_two_mul, two_mul_div_two_of_even (even_bit0 n)]
[GOAL]
m n : ℕ
⊢ bit1 n / 2 = n
[PROOFSTEP]
rw [← Nat.bit1_eq_bit1, bit1, bit0_eq_two_mul, Nat.two_mul_div_two_add_one_of_odd (odd_bit1 n)]
[GOAL]
m n : ℕ
⊢ bit0 n / bit0 m = n / m
[PROOFSTEP]
rw [bit0_eq_two_mul m, ← Nat.div_div_eq_div_mul, bit0_div_two]
[GOAL]
m n : ℕ
⊢ bit1 n / bit0 m = n / m
[PROOFSTEP]
rw [bit0_eq_two_mul, ← Nat.div_div_eq_div_mul, bit1_div_two]
[GOAL]
m n : ℕ
⊢ bit0 n % bit0 m = bit0 (n % m)
[PROOFSTEP]
rw [bit0_eq_two_mul n, bit0_eq_two_mul m, bit0_eq_two_mul (n % m), Nat.mul_mod_mul_left]
[GOAL]
m n : ℕ
⊢ bit1 n % bit0 m = bit1 (n % m)
[PROOFSTEP]
have h₁ :=
  congr_arg bit1
    (Nat.div_add_mod n m)
      -- `∀ m n : ℕ, bit0 m * n = bit0 (m * n)` seems to be missing...
[GOAL]
m n : ℕ
h₁ : bit1 (m * (n / m) + n % m) = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
[PROOFSTEP]
rw [bit1_add, bit0_eq_two_mul, ← mul_assoc, ← bit0_eq_two_mul] at h₁ 
[GOAL]
m n : ℕ
h₁ : bit0 m * (n / m) + bit1 (n % m) = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
[PROOFSTEP]
have h₂ := Nat.div_add_mod (bit1 n) (bit0 m)
[GOAL]
m n : ℕ
h₁ : bit0 m * (n / m) + bit1 (n % m) = bit1 n
h₂ : bit0 m * (bit1 n / bit0 m) + bit1 n % bit0 m = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
[PROOFSTEP]
rw [bit1_div_bit0] at h₂ 
[GOAL]
m n : ℕ
h₁ : bit0 m * (n / m) + bit1 (n % m) = bit1 n
h₂ : bit0 m * (n / m) + bit1 n % bit0 m = bit1 n
⊢ bit1 n % bit0 m = bit1 (n % m)
[PROOFSTEP]
exact add_left_cancel (h₂.trans h₁.symm)
[GOAL]
m✝ n✝ m n : ℕ
h : Even m
⊢ ¬Even (n + 3) ↔ Even (m ^ 2 + m + n)
[PROOFSTEP]
simp [*, two_ne_zero, parity_simps]
  /- Porting note: the `simp` lemmas about `bit*` no longer apply, but `simp` in Lean 4 currently
  simplifies decidable propositions. This may change in the future. -/
[GOAL]
m n : ℕ
⊢ ¬Even 25394535
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
f : α → α
n✝ : ℕ
hf : Involutive f
n : ℕ
⊢ f^[bit0 n] = id
[PROOFSTEP]
rw [bit0, ← two_mul, iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]
[GOAL]
α : Type u_1
f : α → α
n✝ : ℕ
hf : Involutive f
n : ℕ
⊢ f^[bit1 n] = f
[PROOFSTEP]
rw [bit1, ← succ_eq_add_one, iterate_succ, hf.iterate_bit0, comp.left_id]
[GOAL]
α : Type u_1
f : α → α
n✝ : ℕ
hf : Involutive f
n : ℕ
⊢ f^[2 * n] = id
[PROOFSTEP]
rw [iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]
[GOAL]
α : Type u_1
f : α → α
n : ℕ
hf : Involutive f
hn : Even n
⊢ f^[n] = id
[PROOFSTEP]
rcases hn with ⟨m, rfl⟩
[GOAL]
case intro
α : Type u_1
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[m + m] = id
[PROOFSTEP]
rw [← two_mul, hf.iterate_two_mul]
[GOAL]
α : Type u_1
f : α → α
n : ℕ
hf : Involutive f
hn : Odd n
⊢ f^[n] = f
[PROOFSTEP]
rcases hn with ⟨m, rfl⟩
[GOAL]
case intro
α : Type u_1
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[2 * m + 1] = f
[PROOFSTEP]
rw [iterate_add, hf.iterate_two_mul, comp.left_id, iterate_one]
[GOAL]
α : Type u_1
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = f
hn : Even n
⊢ f = id
[PROOFSTEP]
rwa [hf.iterate_even hn, eq_comm] at H 
[GOAL]
α : Type u_1
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = id
hn : Odd n
⊢ f = id
[PROOFSTEP]
rwa [hf.iterate_odd hn] at H 
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n✝ m n : ℕ
hn : Odd n
hm : m ∣ n
⊢ m ≠ 2
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n✝ n : ℕ
hn : Odd n
hm : 2 ∣ n
⊢ False
[PROOFSTEP]
exact absurd (hn.of_dvd_nat hm) (by decide)
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n✝ n : ℕ
hn : Odd n
hm : 2 ∣ n
⊢ ¬Odd 2
[PROOFSTEP]
decide
