chore(Init/Data/Nat/Lemmas): remove more bit01 lemmas (#14788)

Deletions:
- bit0_eq_zero
- bit0_inj
- bit0_le
- bit0_le_bit
- bit0_le_bit1_iff
- bit0_lt
- bit0_lt_bit0
- bit0_lt_bit1
- bit0_lt_bit1_iff
- bit0_ne
- bit0_ne_bit1
- bit0_ne_one
- bit1_eq_succ_bit0
- bit1_inj
- bit1_le
- bit1_le_bit0_iff
- bit1_lt
- bit1_lt_bit0
- bit1_lt_bit0_iff
- bit1_ne
- bit1_ne_bit0
- bit1_ne_one
- bit1_succ_eq
- bit_le_bit1
- bit_lt_bit0
- one_le_bit0
- one_le_bit1
- one_lt_bit0
- one_lt_bit1
- one_ne_bit0
- one_ne_bit1
- zero_ne_bit0
- zero_ne_bit1

Author: jcommelin

Mathlib/Algebra/Polynomial/UnitTrinomial.lean

@@ -150,7 +150,7 @@ theorem card_support_eq_three (hp : p.IsUnitTrinomial) : p.support.card = 3 := b
 
 theorem ne_zero (hp : p.IsUnitTrinomial) : p ≠ 0 := by
   rintro rfl
-  exact Nat.zero_ne_bit1 1 hp.card_support_eq_three
+  simpa using hp.card_support_eq_three
 #align polynomial.is_unit_trinomial.ne_zero Polynomial.IsUnitTrinomial.ne_zero
 
 theorem coeff_isUnit (hp : p.IsUnitTrinomial) {k : ℕ} (hk : k ∈ p.support) :

Mathlib/Data/Nat/Bits.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Nat
 import Mathlib.Data.Nat.Defs
 import Mathlib.Init.Data.List.Basic
-import Mathlib.Init.Data.Nat.Lemmas
+import Mathlib.Init.Data.Nat.Basic
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.GeneralizeProofs
 import Mathlib.Tactic.Says
@@ -398,74 +398,36 @@ theorem bit_cases_on_inj {C : ℕ → Sort u} (H₁ H₂ : ∀ b n, C (bit b n))
   bit_cases_on_injective.eq_iff
 #align nat.bit_cases_on_inj Nat.bit_cases_on_inj
 
-protected theorem bit0_eq_zero {n : ℕ} : 2 * n = 0 ↔ n = 0 := by
-  omega
-#align nat.bit0_eq_zero Nat.bit0_eq_zero
+#noalign nat.bit0_eq_zero
 
 theorem bit_eq_zero_iff {n : ℕ} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
   constructor
-  · cases b <;> simp [Nat.bit, Nat.bit0_eq_zero, Nat.bit1_ne_zero]; omega
+  · cases b <;> simp [Nat.bit]; omega
   · rintro ⟨rfl, rfl⟩
     rfl
 #align nat.bit_eq_zero_iff Nat.bit_eq_zero_iff
 
-protected lemma bit0_le (h : n ≤ m) : 2 * n ≤ 2 * m := by
-  omega
-#align nat.bit0_le Nat.bit0_le
-
-protected lemma bit1_le {n m : ℕ} (h : n ≤ m) : 2 * n + 1 ≤ 2 * m + 1 := by
-  omega
-#align nat.bit1_le Nat.bit1_le
+#noalign nat.bit0_le
+#noalign nat.bit1_le
 
 lemma bit_le : ∀ (b : Bool) {m n : ℕ}, m ≤ n → bit b m ≤ bit b n
-  | true, _, _, h => Nat.bit1_le h
-  | false, _, _, h => Nat.bit0_le h
+  | true, _, _, h => by dsimp [bit]; omega
+  | false, _, _, h => by dsimp [bit]; omega
 #align nat.bit_le Nat.bit_le
 
-lemma bit0_le_bit : ∀ (b) {m n : ℕ}, m ≤ n → 2 * m ≤ bit b n
-  | true, _, _, h => le_of_lt <| Nat.bit0_lt_bit1 h
-  | false, _, _, h => Nat.bit0_le h
-#align nat.bit0_le_bit Nat.bit0_le_bit
-
-lemma bit_le_bit1 : ∀ (b) {m n : ℕ}, m ≤ n → bit b m ≤ 2 * n + 1
-  | false, _, _, h => le_of_lt <| Nat.bit0_lt_bit1 h
-  | true, _, _, h => Nat.bit1_le h
-#align nat.bit_le_bit1 Nat.bit_le_bit1
-
-lemma bit_lt_bit0 : ∀ (b) {m n : ℕ}, m < n → bit b m < 2 * n
-  | true, _, _, h => Nat.bit1_lt_bit0 h
-  | false, _, _, h => Nat.bit0_lt h
-#align nat.bit_lt_bit0 Nat.bit_lt_bit0
+#noalign nat.bit0_le_bit
+#noalign nat.bit_le_bit1
+#noalign nat.bit_lt_bit0
 
-protected lemma bit0_lt_bit0 : 2 * m < 2 * n ↔ m < n := by omega
-
-lemma bit_lt_bit (a b) (h : m < n) : bit a m < bit b n :=
-  lt_of_lt_of_le (bit_lt_bit0 _ h) (bit0_le_bit _ (le_refl _))
+lemma bit_lt_bit (a b) (h : m < n) : bit a m < bit b n := calc
+  bit a m < 2 * n   := by cases a <;> dsimp [bit] <;> omega
+        _ ≤ bit b n := by cases b <;> dsimp [bit] <;> omega
 #align nat.bit_lt_bit Nat.bit_lt_bit
 
-@[simp]
-lemma bit0_le_bit1_iff : 2 * m ≤ 2 * n + 1 ↔ m ≤ n := by
-  refine ⟨fun h ↦ ?_, fun h ↦ le_of_lt (Nat.bit0_lt_bit1 h)⟩
-  rwa [← Nat.lt_succ_iff, n.bit1_eq_succ_bit0, ← n.bit0_succ_eq, Nat.bit0_lt_bit0, Nat.lt_succ_iff]
-    at h
-#align nat.bit0_le_bit1_iff Nat.bit0_le_bit1_iff
-
-@[simp]
-lemma bit0_lt_bit1_iff : 2 * m < 2 * n + 1 ↔ m ≤ n :=
-  ⟨fun h => bit0_le_bit1_iff.1 (le_of_lt h), Nat.bit0_lt_bit1⟩
-#align nat.bit0_lt_bit1_iff Nat.bit0_lt_bit1_iff
-
-@[simp]
-lemma bit1_le_bit0_iff : 2 * m + 1 ≤ 2 * n ↔ m < n :=
-  ⟨fun h ↦ by rwa [m.bit1_eq_succ_bit0, Nat.succ_le_iff, Nat.bit0_lt_bit0] at h,
-     fun h ↦ le_of_lt (Nat.bit1_lt_bit0 h)⟩
-#align nat.bit1_le_bit0_iff Nat.bit1_le_bit0_iff
-
-@[simp]
-lemma bit1_lt_bit0_iff : 2 * m + 1 < 2 * n ↔ m < n :=
-  ⟨fun h ↦ bit1_le_bit0_iff.1 (le_of_lt h), Nat.bit1_lt_bit0⟩
-#align nat.bit1_lt_bit0_iff Nat.bit1_lt_bit0_iff
-
+#noalign nat.bit0_le_bit1_iff
+#noalign nat.bit0_lt_bit1_iff
+#noalign nat.bit1_le_bit0_iff
+#noalign nat.bit1_lt_bit0_iff
 #noalign nat.one_le_bit0_iff
 #noalign nat.one_lt_bit0_iff
 #noalign nat.bit_le_bit_iff

Mathlib/Data/Nat/Bitwise.lean

@@ -162,7 +162,7 @@ theorem bit_true : bit true = (2 * · + 1) :=
 
 @[simp]
 theorem bit_eq_zero {n : ℕ} {b : Bool} : n.bit b = 0 ↔ n = 0 ∧ b = false := by
-  cases b <;> simp [Nat.bit0_eq_zero, Nat.bit1_ne_zero]
+  cases b <;> simp [bit, Nat.mul_eq_zero]
 #align nat.bit_eq_zero Nat.bit_eq_zero
 
 theorem bit_ne_zero_iff {n : ℕ} {b : Bool} : n.bit b ≠ 0 ↔ n = 0 → b = true := by

Mathlib/Data/Nat/Size.lean

@@ -105,7 +105,7 @@ theorem lt_size_self (n : ℕ) : n < 2 ^ size n := by
   by_cases h : bit b n = 0
   · apply this h
   rw [size_bit h, shiftLeft_succ, shiftLeft_eq, one_mul]
-  exact bit_lt_bit0 _ (by simpa [shiftLeft_eq, shiftRight_eq_div_pow] using IH)
+  cases b <;> dsimp [bit] <;> omega
 #align nat.lt_size_self Nat.lt_size_self
 
 theorem size_le {m n : ℕ} : size m ≤ n ↔ m < 2 ^ n :=
@@ -123,7 +123,8 @@ theorem size_le {m n : ℕ} : size m ≤ n ↔ m < 2 ^ n :=
       · apply succ_le_succ (IH _)
         apply Nat.lt_of_mul_lt_mul_left (a := 2)
         simp only [shiftLeft_succ] at *
-        exact lt_of_le_of_lt (bit0_le_bit b rfl.le) h⟩
+        refine lt_of_le_of_lt ?_ h
+        cases b <;> dsimp [bit] <;> omega⟩
 #align nat.size_le Nat.size_le
 
 theorem lt_size {m n : ℕ} : m < size n ↔ 2 ^ m ≤ n := by

Mathlib/Data/Num/Lemmas.lean

@@ -1600,10 +1600,9 @@ theorem divMod_to_nat (d n : PosNum) :
     -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
     revert IH; cases' divMod d n with q r; intro IH
     simp only [divMod] at IH ⊢
-    apply divMod_to_nat_aux <;> simp
-    · rw [← add_assoc, ← add_assoc, ← two_mul, ← two_mul, add_right_comm,
-        mul_left_comm, ← mul_add, IH.1]
-    · exact IH.2
+    apply divMod_to_nat_aux <;> simp only [Num.cast_bit1, cast_bit1]
+    · rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]
+    · omega
   · unfold divMod
     -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
     revert IH; cases' divMod d n with q r; intro IH

Mathlib/Data/Num/Prime.lean

@@ -98,11 +98,12 @@ instance decidablePrime : DecidablePred PosNum.Prime
         rw [← minFac_to_nat, to_nat_inj]
         exact ⟨bit0.inj, congr_arg _⟩)
   | bit1 n =>
-    decidable_of_iff' (minFacAux (bit1 n) n 1 = bit1 n)
-      (by
+    decidable_of_iff' (minFacAux (bit1 n) n 1 = bit1 n) <| by
         refine Nat.prime_def_minFac.trans ((and_iff_right ?_).trans ?_)
-        · exact (Nat.bit0_le_bit1_iff.2 (to_nat_pos n)).trans <| by simp [two_mul]
-        rw [← minFac_to_nat, to_nat_inj]; rfl)
+        · simp only [cast_bit1]
+          have := to_nat_pos n
+          omega
+        rw [← minFac_to_nat, to_nat_inj]; rfl
 #align pos_num.decidable_prime PosNum.decidablePrime
 
 end PosNum

Mathlib/Init/Data/Nat/Lemmas.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad
 -/
 import Batteries.Data.Nat.Lemmas
-import Batteries.Logic
 import Batteries.WF
-import Mathlib.Init.Data.Nat.Basic
 import Mathlib.Util.AssertExists
+import Mathlib.Mathport.Rename
+import Mathlib.Data.Nat.Notation
 
 #align_import init.data.nat.lemmas from "leanprover-community/lean"@"38b59111b2b4e6c572582b27e8937e92fc70ac02"
 
@@ -227,107 +227,32 @@ protected def ltByCases {a b : ℕ} {C : Sort u} (h₁ : a < b → C) (h₂ : a
 
 /-! bit0/bit1 properties -/
 section bit
-set_option linter.deprecated false
 
-protected theorem bit1_eq_succ_bit0 (n : ℕ) : 2 * n + 1 = succ (2 * n) :=
-  rfl
-#align nat.bit1_eq_succ_bit0 Nat.bit1_eq_succ_bit0
-
-protected theorem bit1_succ_eq (n : ℕ) : 2 * (succ n) + 1 = succ (succ (2 * n + 1)) :=
-  Eq.trans (Nat.bit1_eq_succ_bit0 (succ n)) (congr_arg succ (Nat.bit0_succ_eq n))
-#align nat.bit1_succ_eq Nat.bit1_succ_eq
-
-protected theorem bit1_ne_one : ∀ {n : ℕ}, n ≠ 0 → 2 * n + 1 ≠ 1
-  | 0, h, _h1 => absurd rfl h
-  | _n + 1, _h, h1 => Nat.noConfusion h1 fun h2 => absurd h2 (succ_ne_zero _)
-#align nat.bit1_ne_one Nat.bit1_ne_one
-
-protected theorem bit0_ne_one : ∀ n : ℕ, 2 * n ≠ 1 := by
-  omega
-#align nat.bit0_ne_one Nat.bit0_ne_one
+#noalign nat.bit1_eq_succ_bit0
+#noalign nat.bit1_succ_eq
+#noalign nat.bit1_ne_one
+#noalign nat.bit0_ne_one
 
 #align nat.add_self_ne_one Nat.add_self_ne_one
 
-protected theorem bit1_ne_bit0 : ∀ n m : ℕ, 2 * n + 1 ≠ 2 * m := by
-  omega
-#align nat.bit1_ne_bit0 Nat.bit1_ne_bit0
-
-protected theorem bit0_ne_bit1 : ∀ n m : ℕ, 2 * n ≠ 2 * m + 1 := by
-  omega
-#align nat.bit0_ne_bit1 Nat.bit0_ne_bit1
-
-protected theorem bit0_inj : ∀ {n m : ℕ}, 2 * n = 2 * m → n = m := by
-  omega
-#align nat.bit0_inj Nat.bit0_inj
-
-protected theorem bit1_inj : ∀ {n m : ℕ}, 2 * n + 1 = 2 * m + 1 → n = m := @fun n m h => by
-  omega
-#align nat.bit1_inj Nat.bit1_inj
-
-protected theorem bit0_ne {n m : ℕ} : n ≠ m → 2 * n ≠ 2 * m := fun h₁ h₂ =>
-  absurd (Nat.bit0_inj h₂) h₁
-#align nat.bit0_ne Nat.bit0_ne
-
-protected theorem bit1_ne {n m : ℕ} : n ≠ m → 2 * n + 1 ≠ 2 * m + 1 := fun h₁ h₂ =>
-  absurd (Nat.bit1_inj h₂) h₁
-#align nat.bit1_ne Nat.bit1_ne
-
-protected theorem zero_ne_bit0 {n : ℕ} : n ≠ 0 → 0 ≠ 2 * n := fun h => Ne.symm (Nat.bit0_ne_zero h)
-#align nat.zero_ne_bit0 Nat.zero_ne_bit0
-
-protected theorem zero_ne_bit1 (n : ℕ) : 0 ≠ 2 * n + 1 :=
-  Ne.symm (Nat.bit1_ne_zero n)
-#align nat.zero_ne_bit1 Nat.zero_ne_bit1
-
-protected theorem one_ne_bit0 (n : ℕ) : 1 ≠ 2 * n :=
-  Ne.symm (Nat.bit0_ne_one n)
-#align nat.one_ne_bit0 Nat.one_ne_bit0
-
-protected theorem one_ne_bit1 {n : ℕ} : n ≠ 0 → 1 ≠ 2 * n + 1 := fun h => Ne.symm (Nat.bit1_ne_one h)
-#align nat.one_ne_bit1 Nat.one_ne_bit1
-
-protected theorem one_lt_bit1 : ∀ {n : Nat}, n ≠ 0 → 1 < 2 * n + 1
-  | 0, h => by contradiction
-  | succ n, _h => by
-    rw [Nat.bit1_succ_eq]
-    apply succ_lt_succ
-    apply zero_lt_succ
-#align nat.one_lt_bit1 Nat.one_lt_bit1
-
-protected theorem one_lt_bit0 : ∀ {n : Nat}, n ≠ 0 → 1 < 2 * n
-  | 0, h => by contradiction
-  | succ n, _h => by
-    rw [Nat.bit0_succ_eq]
-    apply succ_lt_succ
-    apply zero_lt_succ
-#align nat.one_lt_bit0 Nat.one_lt_bit0
-
-protected theorem bit0_lt {n m : Nat} (h : n < m) : 2 * n < 2 * m := by
-  omega
-#align nat.bit0_lt Nat.bit0_lt
-
-protected theorem bit1_lt {n m : Nat} (h : n < m) : 2 * n + 1 < 2 * m + 1 := by
-  omega
-#align nat.bit1_lt Nat.bit1_lt
-
-protected theorem bit0_lt_bit1 {n m : Nat} (h : n ≤ m) : 2 * n < 2 * m + 1 := by
-  omega
-#align nat.bit0_lt_bit1 Nat.bit0_lt_bit1
-
-protected theorem bit1_lt_bit0 : ∀ {n m : Nat}, n < m → 2 * n + 1 < 2 * m := by
-  omega
-#align nat.bit1_lt_bit0 Nat.bit1_lt_bit0
-
-protected theorem one_le_bit1 (n : ℕ) : 1 ≤ 2 * n + 1 :=
-  show 1 ≤ succ (2 * n) from succ_le_succ (2 * n).zero_le
-#align nat.one_le_bit1 Nat.one_le_bit1
-
-protected theorem one_le_bit0 : ∀ n : ℕ, n ≠ 0 → 1 ≤ 2 * n
-  | 0, h => absurd rfl h
-  | n + 1, _h =>
-    suffices 1 ≤ succ (succ (2 * n)) from Eq.symm (Nat.bit0_succ_eq n) ▸ this
-    succ_le_succ (2 * n).succ.zero_le
-#align nat.one_le_bit0 Nat.one_le_bit0
+#noalign nat.bit1_ne_bit0
+#noalign nat.bit0_ne_bit1
+#noalign nat.bit0_inj
+#noalign nat.bit1_inj
+#noalign nat.bit0_ne
+#noalign nat.bit1_ne
+#noalign nat.zero_ne_bit0
+#noalign nat.zero_ne_bit1
+#noalign nat.one_ne_bit0
+#noalign nat.one_ne_bit1
+#noalign nat.one_lt_bit1
+#noalign nat.one_lt_bit0
+#noalign nat.bit0_lt
+#noalign nat.bit1_lt
+#noalign nat.bit0_lt_bit1
+#noalign nat.bit1_lt_bit0
+#noalign nat.one_le_bit1
+#noalign nat.one_le_bit0
 
 end bit