feat: port Data.Nat.Parity (#1661)

Backported in leanprover-community/mathlib#18221.



Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Mathlib.lean

@@ -413,6 +413,7 @@ import Mathlib.Data.Nat.Order.Basic
 import Mathlib.Data.Nat.Order.Lemmas
 import Mathlib.Data.Nat.PSub
 import Mathlib.Data.Nat.Pairing
+import Mathlib.Data.Nat.Parity
 import Mathlib.Data.Nat.Pow
 import Mathlib.Data.Nat.Prime
 import Mathlib.Data.Nat.PrimeFin

Mathlib/Algebra/Parity.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 
 ! This file was ported from Lean 3 source module algebra.parity
-! leanprover-community/mathlib commit dcf2250875895376a142faeeac5eabff32c48655
+! leanprover-community/mathlib commit 8631e2d5ea77f6c13054d9151d82b83069680cb1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -226,7 +226,6 @@ theorem Even.tsub [CanonicallyLinearOrderedAddMonoid α] [Sub α] [OrderedSub α
   · exact (tsub_add_tsub_comm h h).symm
 #align even.tsub Even.tsub
 
-
 set_option linter.deprecated false in
 theorem even_iff_exists_bit0 [Add α] {a : α} : Even a ↔ ∃ b, a = bit0 b :=
   Iff.rfl
@@ -236,8 +235,6 @@ alias even_iff_exists_bit0 ↔ Even.exists_bit0 _
 
 section Semiring
 
-set_option linter.deprecated false
-
 variable [Semiring α] [Semiring β] {m n : α}
 
 theorem even_iff_exists_two_mul (m : α) : Even m ↔ ∃ c, m = 2 * c := by
@@ -247,15 +244,25 @@ theorem even_iff_exists_two_mul (m : α) : Even m ↔ ∃ c, m = 2 * c := by
 theorem even_iff_two_dvd {a : α} : Even a ↔ 2 ∣ a := by simp [Even, Dvd.dvd, two_mul]
 #align even_iff_two_dvd even_iff_two_dvd
 
+alias even_iff_two_dvd ↔ Even.two_dvd _
+#align even.two_dvd Even.two_dvd
+
+theorem Even.trans_dvd (hm : Even m) (hn : m ∣ n) : Even n :=
+  even_iff_two_dvd.2 <| hm.two_dvd.trans hn
+#align even.trans_dvd Even.trans_dvd
+
+theorem Dvd.dvd.even (hn : m ∣ n) (hm : Even m) : Even n :=
+  hm.trans_dvd hn
+#align has_dvd.dvd.even Dvd.dvd.even
+
 @[simp]
-theorem range_two_mul (α : Type _) [Semiring α] :
-    (Set.range fun x : α => 2 * x) = { a | Even a } := by
+theorem range_two_mul (α) [Semiring α] : (Set.range fun x : α => 2 * x) = { a | Even a } := by
   ext x
   simp [eq_comm, two_mul, Even]
 #align range_two_mul range_two_mul
 
-@[simp]
-theorem even_bit0 (a : α) : Even (bit0 a) :=
+set_option linter.deprecated false in
+@[simp] theorem even_bit0 (a : α) : Even (bit0 a) :=
   ⟨a, rfl⟩
 #align even_bit0 even_bit0
 
@@ -292,6 +299,7 @@ def Odd (a : α) : Prop :=
   ∃ k, a = 2 * k + 1
 #align odd Odd
 
+set_option linter.deprecated false in
 theorem odd_iff_exists_bit1 {a : α} : Odd a ↔ ∃ b, a = bit1 b :=
   exists_congr fun b => by
     rw [two_mul]
@@ -300,8 +308,8 @@ theorem odd_iff_exists_bit1 {a : α} : Odd a ↔ ∃ b, a = bit1 b :=
 
 alias odd_iff_exists_bit1 ↔ Odd.exists_bit1 _
 
-@[simp]
-theorem odd_bit1 (a : α) : Odd (bit1 a) :=
+set_option linter.deprecated false in
+@[simp] theorem odd_bit1 (a : α) : Odd (bit1 a) :=
   odd_iff_exists_bit1.2 ⟨a, rfl⟩
 #align odd_bit1 odd_bit1
 
@@ -325,9 +333,8 @@ theorem Odd.add_even (hm : Odd m) (hn : Even n) : Odd (m + n) := by
 theorem Odd.add_odd : Odd m → Odd n → Even (m + n) := by
   rintro ⟨m, rfl⟩ ⟨n, rfl⟩
   refine' ⟨n + m + 1, _⟩
-  rw [← two_mul, ← add_assoc, add_comm _ (2 * n), ← add_assoc, ← mul_add, add_assoc,
-    mul_add _ (n + m), mul_one]
-  rw [one_add_one_eq_two]
+  rw [two_mul, two_mul]
+  ac_rfl
 #align odd.add_odd Odd.add_odd
 
 @[simp]
@@ -370,7 +377,6 @@ section Monoid
 
 variable [Monoid α] [HasDistribNeg α] {a : α} {n : ℕ}
 
-
 theorem Odd.neg_pow : Odd n → ∀ a : α, (-a) ^ n = -a ^ n := by
   rintro ⟨c, rfl⟩ a
   simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]
@@ -507,3 +513,6 @@ theorem Odd.strictMono_pow (hn : Odd n) : StrictMono fun a : R => a ^ n := by
 #align odd.strict_mono_pow Odd.strictMono_pow
 
 end Powers
+
+/-- Simp attribute for lemmas about `even` -/
+register_simp_attr parity_simps