chore(Data/Nat/{Bit, Bitwise}): make Nat.bit_mod_two `Nat.bit_eq_ze…

…ro_iff` be `simp` (#17924)

Also deprecate `Nat.bit_eq_zero`. It is identical to `Nat.bit_eq_zero_iff`.

Mathlib/Data/Nat/Bits.lean

@@ -328,6 +328,7 @@ theorem bit_cases_on_inj {motive : ℕ → Sort u} (H₁ H₂ : ∀ b n, motive
     ((fun n => bitCasesOn n H₁) = fun n => bitCasesOn n H₂) ↔ H₁ = H₂ :=
   bit_cases_on_injective.eq_iff
 
+@[simp]
 theorem bit_eq_zero_iff {n : ℕ} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
   constructor
   · cases b <;> simp [Nat.bit]; omega

Mathlib/Data/Nat/Bitwise.lean

@@ -88,19 +88,18 @@ lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by
   cases a <;> cases b <;> simp [h2, h4] <;> split_ifs
     <;> simp_all (config := {decide := true}) [two_mul]
 
+@[simp]
 lemma bit_mod_two (a : Bool) (x : ℕ) :
     bit a x % 2 = a.toNat := by
   cases a <;> simp [bit_val, mul_add_mod]
 
-@[simp]
 lemma bit_mod_two_eq_zero_iff (a x) :
     bit a x % 2 = 0 ↔ !a := by
-  simp [bit_mod_two]
+  simp
 
-@[simp]
 lemma bit_mod_two_eq_one_iff (a x) :
     bit a x % 2 = 1 ↔ a := by
-  simp [bit_mod_two]
+  simp
 
 @[simp]
 theorem lor_bit : ∀ a m b n, bit a m ||| bit b n = bit (a || b) (m ||| n) :=
@@ -142,12 +141,10 @@ theorem bit_false : bit false = (2 * ·) :=
 theorem bit_true : bit true = (2 * · + 1) :=
   rfl
 
-@[simp]
-theorem bit_eq_zero {n : ℕ} {b : Bool} : n.bit b = 0 ↔ n = 0 ∧ b = false := by
-  cases b <;> simp [bit, Nat.mul_eq_zero]
+@[deprecated (since := "2024-10-19")] alias bit_eq_zero := bit_eq_zero_iff
 
 theorem bit_ne_zero_iff {n : ℕ} {b : Bool} : n.bit b ≠ 0 ↔ n = 0 → b = true := by
-  simpa only [not_and, Bool.not_eq_false] using (@bit_eq_zero n b).not
+  simp
 
 /-- An alternative for `bitwise_bit` which replaces the `f false false = false` assumption
 with assumptions that neither `bit a m` nor `bit b n` are `0`

Mathlib/Data/Nat/Multiplicity.lean

@@ -6,7 +6,6 @@ Authors: Chris Hughes
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.GeomSum
 import Mathlib.Algebra.Order.Ring.Abs
-import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.Nat.Log
 import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.Data.Nat.Digits
@@ -282,10 +281,10 @@ theorem emultiplicity_two_factorial_lt : ∀ {n : ℕ} (_ : n ≠ 0), emultiplic
   · intro b n ih h
     by_cases hn : n = 0
     · subst hn
-      simp only [ne_eq, bit_eq_zero, true_and, Bool.not_eq_false] at h
-      simp only [h, bit_true, factorial, mul_one, Nat.isUnit_iff, cast_one]
+      simp only [ne_eq, bit_eq_zero_iff, true_and, Bool.not_eq_false] at h
+      simp only [h, factorial, mul_one, Nat.isUnit_iff, cast_one]
       rw [Prime.emultiplicity_one]
-      · simp [zero_lt_one]
+      · exact zero_lt_one
       · decide
     have : emultiplicity 2 (2 * n)! < (2 * n : ℕ) := by
       rw [prime_two.emultiplicity_factorial_mul]