From b8c1db6b378c95d1d7bcd2ab06a443461f23ab3b Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sun, 30 Jul 2023 16:27:33 -0700
Subject: [PATCH 01/17] removed shiftl and shiftr

---
 Mathlib/Init/Data/Nat/Bitwise.lean | 102 +++++++++++------------------
 1 file changed, 37 insertions(+), 65 deletions(-)

diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index 8303d8b97c6e3..6bab5e9cfec5e 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -1,12 +1,7 @@
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
-
-! This file was ported from Lean 3 source module init.data.nat.bitwise
-! leanprover-community/lean commit 53e8520d8964c7632989880372d91ba0cecbaf00
-! Please do not edit these lines, except to modify the commit id
-! if you have ported upstream changes.
+Authors: Mario Carneiro, Harun Khan
 -/
 import Mathlib.Init.Data.Nat.Lemmas
 import Init.WFTactics
@@ -16,6 +11,8 @@ import Mathlib.Init.ZeroOne
 import Mathlib.Tactic.Cases
 import Mathlib.Tactic.PermuteGoals
 
+#align_import init.data.nat.bitwise from "leanprover-community/lean"@"53e8520d8964c7632989880372d91ba0cecbaf00"
+
 /-!
 # Lemmas about bitwise operations on natural numbers.
 
@@ -181,49 +178,32 @@ theorem bit_zero : bit false 0 = 0 :=
   rfl
 #align nat.bit_zero Nat.bit_zero
 
-/--`shiftl' b m n` performs a left shift of `m` `n` times
- and adds the bit `b` as the least significant bit each time.
- Returns the corresponding natural number-/
-def shiftl' (b : Bool) (m : ℕ) : ℕ → ℕ
-  | 0 => m
-  | n + 1 => bit b (shiftl' b m n)
-#align nat.shiftl' Nat.shiftl'
+@[simp] lemma bit_0 (b : Bool) : Nat.bit b 0 = b.toNat := by
+  cases' b <;> simp
 
-/-- `shiftl m n` produces a natural number whose binary representation
-  is obtained by left-shifting the binary representation of `m` by `n` places -/
-def shiftl : ℕ → ℕ → ℕ :=
-  shiftl' false
-#align nat.shiftl Nat.shiftl
+@[simp] lemma bit_1 (b : Bool) : Nat.bit b 1 = 2 + b.toNat:= by
+  cases' b <;> simp
 
 @[simp]
-theorem shiftl_zero (m) : shiftl m 0 = m :=
+theorem shiftLeft_zero (m) : shiftLeft m 0 = m :=
   rfl
-#align nat.shiftl_zero Nat.shiftl_zero
 
 @[simp]
-theorem shiftl_succ (m n) : shiftl m (n + 1) = bit0 (shiftl m n) :=
-  rfl
-#align nat.shiftl_succ Nat.shiftl_succ
+theorem shiftLeft_succ (m n) : m <<< (n + 1) = bit0 (m <<< n) := by
+  simp only [shiftLeft_eq, bit0, pow_succ, ← Nat.mul_add, Nat.mul_two]
 
-/--`shiftr n m` performs returns the `m`-step right shift operation on `n` and
-returns the resultant number. This is equivalent to performing `⌊n/2ᵐ⌋`-/
-def shiftr : ℕ → ℕ → ℕ
-  | m, 0 => m
-  | m, n + 1 => div2 (shiftr m n)
-#align nat.shiftr Nat.shiftr
-
-theorem shiftr_zero : ∀ n, shiftr 0 n = 0 := by
+theorem shiftRight_zero : ∀ n, shiftRight 0 n = 0 := by
   intro n
   induction' n with n IH
   case zero =>
-    rw [shiftr]
+    rw [shiftRight]
   case succ =>
-    rw [shiftr, div2, IH]
+    rw [shiftRight, IH]
     rfl
 
 /-- `testBit m n` returns whether the `(n+1)ˢᵗ` least significant bit is `1` or `0`-/
 def testBit (m n : ℕ) : Bool :=
-  bodd (shiftr m n)
+  bodd (shiftRight m n)
 #align nat.test_bit Nat.testBit
 
 
@@ -285,7 +265,7 @@ def land' : ℕ → ℕ → ℕ :=
 
 /--`ldiff' a b` performs bitwise set difference. For each corresponding
   pair of bits taken as booleans, say `aᵢ` and `bᵢ`, it applies the
-  boolean operation `aᵢ  ∧ bᵢ` to obtain the `iᵗʰ` bit of the result.-/
+  boolean operation `aᵢ ∧ bᵢ` to obtain the `iᵗʰ` bit of the result.-/
 def ldiff' : ℕ → ℕ → ℕ :=
   bitwise' fun a b => a && not b
 #align nat.ldiff Nat.ldiff'
@@ -316,32 +296,24 @@ theorem div2_bit (b n) : div2 (bit b n) = n := by
   <;> exact by decide
 #align nat.div2_bit Nat.div2_bit
 
-theorem shiftl'_add (b m n) : ∀ k, shiftl' b m (n + k) = shiftl' b (shiftl' b m n) k
+theorem shiftLeft_add (m n) : ∀ k, shiftLeft m (n + k) = shiftLeft (shiftLeft m n) k
   | 0 => rfl
-  | k + 1 => congr_arg (bit b) (shiftl'_add b m n k)
-#align nat.shiftl'_add Nat.shiftl'_add
-
-theorem shiftl_add : ∀ m n k, shiftl m (n + k) = shiftl (shiftl m n) k :=
-  shiftl'_add _
-#align nat.shiftl_add Nat.shiftl_add
+  | k + 1 => congr_arg (bit true) (shiftLeft_add m n k)
+#align nat.shiftl'_add Nat.shiftLeft_add
 
-theorem shiftr_add (m n) : ∀ k, shiftr m (n + k) = shiftr (shiftr m n) k
+theorem shiftRight_add (m n) : ∀ k, shiftRight m (n + k) = shiftRight (shiftRight m n) k
   | 0 => rfl
-  | k + 1 => congr_arg div2 (shiftr_add m n k)
-#align nat.shiftr_add Nat.shiftr_add
-
-theorem shiftl'_sub (b m) : ∀ {n k}, k ≤ n → shiftl' b m (n - k) = shiftr (shiftl' b m n) k
-  | n, 0, _ => rfl
-  | n + 1, k + 1, h => by
-    simp [shiftl']
-    rw [Nat.add_comm, shiftr_add]
-    simp [shiftr, div2_bit]
-    simp [shiftl'_sub, (Nat.le_of_succ_le_succ h)]
-#align nat.shiftl'_sub Nat.shiftl'_sub
-
-theorem shiftl_sub : ∀ (m) {n k}, k ≤ n → shiftl m (n - k) = shiftr (shiftl m n) k :=
-  shiftl'_sub _
-#align nat.shiftl_sub Nat.shiftl_sub
+  | k + 1 => congr_arg (fun n => n/2) (shiftRight_add m n k)
+
+theorem shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → shiftLeft m (n - k) = shiftRight (shiftLeft m n) k
+  | m, n, 0, _ => rfl
+  | m, n + 1, k + 1, h => by
+    simp [shiftLeft]
+    rw [Nat.add_comm, shiftRight_add]
+    simp [shiftRight, div2_bit]
+    rw [shiftLeft_sub]
+    simp [shiftLeft_sub, (Nat.le_of_succ_le_succ h)]
+#align nat.shiftl'_sub Nat.shiftLeft_sub
 
 @[simp]
 theorem testBit_zero (b n) : testBit (bit b n) 0 = b :=
@@ -349,10 +321,10 @@ theorem testBit_zero (b n) : testBit (bit b n) 0 = b :=
 #align nat.test_bit_zero Nat.testBit_zero
 
 theorem testBit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by
-  have : bodd (shiftr (shiftr (bit b n) 1) m) = bodd (shiftr n m) := by
-    dsimp [shiftr]
-    rw [div2_bit]
-  rw [← shiftr_add, Nat.add_comm] at this
+  have : bodd (shiftRight (shiftRight (bit b n) 1) m) = bodd (shiftRight n m) := by
+    dsimp [shiftRight]
+    simp [← div2_val, div2_bit]
+  rw [← shiftRight_add, Nat.add_comm] at this
   exact this
 #align nat.test_bit_succ Nat.testBit_succ
 
@@ -380,7 +352,7 @@ theorem binaryRec_eq {C : Nat → Sort u} {z : C 0} {f : ∀ b n, C n → C (bit
       (Eq.symm (bit_decomp (bit b n)) ▸ Eq.refl (C (bit b n))) = e
     revert e
     rw [bodd_bit, div2_bit]
-    intros ; rfl
+    intros; rfl
 #align nat.binary_rec_eq Nat.binaryRec_eq
 
 theorem bitwise'_bit_aux {f : Bool → Bool → Bool} (h : f false false = false) :
@@ -413,8 +385,8 @@ theorem bitwise'_zero_left (f : Bool → Bool → Bool) (n) :
 @[simp]
 theorem bitwise'_zero_right (f : Bool → Bool → Bool) (h : f false false = false) (m) :
     bitwise' f m 0 = cond (f true false) m 0 := by
-  unfold bitwise'; apply bitCasesOn m; intros; rw [binaryRec_eq, binaryRec_zero];
-    exact bitwise'_bit_aux h
+  unfold bitwise'; apply bitCasesOn m; intros; rw [binaryRec_eq, binaryRec_zero]
+  exact bitwise'_bit_aux h
 #align nat.bitwise_zero_right Nat.bitwise'_zero_right
 
 @[simp]

From af42dd28069d60d66272be61f557be0efa93c754 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Thu, 3 Aug 2023 18:12:35 -0700
Subject: [PATCH 02/17] deleted shiftl, shfitr and fixed proofs

---
 Mathlib/Init/Data/Nat/Bitwise.lean | 48 +++++++++++++++++-------------
 1 file changed, 28 insertions(+), 20 deletions(-)

diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index 6bab5e9cfec5e..c80e5f2f486ae 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -184,26 +184,34 @@ theorem bit_zero : bit false 0 = 0 :=
 @[simp] lemma bit_1 (b : Bool) : Nat.bit b 1 = 2 + b.toNat:= by
   cases' b <;> simp
 
+@[simp] lemma shiftLeft_eq' {m n : Nat} : shiftLeft n m = n <<< m := rfl
+
+@[simp] lemma shiftRight_eq {m n : Nat} : shiftRight n m = n >>> m := rfl
+
 @[simp]
-theorem shiftLeft_zero (m) : shiftLeft m 0 = m :=
-  rfl
+theorem shiftLeft_zero (m) : m <<< 0 = m := rfl
+
+@[simp]
+theorem shiftLeft_succ (m n) : m <<< (n + 1) = 2 * (m <<< n) := by
+  simp only [shiftLeft_eq, Nat.pow_add, Nat.pow_one, ← Nat.mul_assoc, Nat.mul_comm]
 
 @[simp]
-theorem shiftLeft_succ (m n) : m <<< (n + 1) = bit0 (m <<< n) := by
-  simp only [shiftLeft_eq, bit0, pow_succ, ← Nat.mul_add, Nat.mul_two]
+theorem shiftRight_zero : n >>> 0 = n := rfl
 
-theorem shiftRight_zero : ∀ n, shiftRight 0 n = 0 := by
+@[simp]
+theorem shiftRight_succ (m n) : m >>> (n + 1) = (m >>> n) / 2 := rfl
+
+theorem zero_shiftRight : ∀ n, 0 >>> n = 0 := by
   intro n
   induction' n with n IH
   case zero =>
-    rw [shiftRight]
+    simp [shiftRight]
   case succ =>
-    rw [shiftRight, IH]
-    rfl
+    simp [shiftRight, IH]
 
 /-- `testBit m n` returns whether the `(n+1)ˢᵗ` least significant bit is `1` or `0`-/
 def testBit (m n : ℕ) : Bool :=
-  bodd (shiftRight m n)
+  bodd (m >>> n)
 #align nat.test_bit Nat.testBit
 
 
@@ -296,23 +304,23 @@ theorem div2_bit (b n) : div2 (bit b n) = n := by
   <;> exact by decide
 #align nat.div2_bit Nat.div2_bit
 
-theorem shiftLeft_add (m n) : ∀ k, shiftLeft m (n + k) = shiftLeft (shiftLeft m n) k
+theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k
   | 0 => rfl
-  | k + 1 => congr_arg (bit true) (shiftLeft_add m n k)
+  | k + 1 => by
+    simp only [shiftLeft_eq, Nat.mul_assoc, Nat.pow_add]
 #align nat.shiftl'_add Nat.shiftLeft_add
 
-theorem shiftRight_add (m n) : ∀ k, shiftRight m (n + k) = shiftRight (shiftRight m n) k
+theorem shiftRight_add (m n : Nat) : ∀ k, m >>> (n + k) = (m >>> n) >>> k
   | 0 => rfl
-  | k + 1 => congr_arg (fun n => n/2) (shiftRight_add m n k)
+  | k + 1 => by simp [add_succ, shiftRight_add]
 
-theorem shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → shiftLeft m (n - k) = shiftRight (shiftLeft m n) k
+theorem shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<< n) >>> k
   | m, n, 0, _ => rfl
   | m, n + 1, k + 1, h => by
-    simp [shiftLeft]
-    rw [Nat.add_comm, shiftRight_add]
-    simp [shiftRight, div2_bit]
-    rw [shiftLeft_sub]
-    simp [shiftLeft_sub, (Nat.le_of_succ_le_succ h)]
+    rw [succ_sub_succ_eq_sub, shiftLeft_succ, Nat.add_comm, shiftRight_add]
+    simp only [shiftLeft_sub, Nat.le_of_succ_le_succ h]
+    simp
+
 #align nat.shiftl'_sub Nat.shiftLeft_sub
 
 @[simp]
@@ -321,7 +329,7 @@ theorem testBit_zero (b n) : testBit (bit b n) 0 = b :=
 #align nat.test_bit_zero Nat.testBit_zero
 
 theorem testBit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by
-  have : bodd (shiftRight (shiftRight (bit b n) 1) m) = bodd (shiftRight n m) := by
+  have : bodd (((bit b n) >>> 1) >>> m) = bodd (n >>> m) := by
     dsimp [shiftRight]
     simp [← div2_val, div2_bit]
   rw [← shiftRight_add, Nat.add_comm] at this

From c6f29aa89d26e9923cdde95ec78062be48a70884 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Thu, 3 Aug 2023 18:25:01 -0700
Subject: [PATCH 03/17] minor changes

---
 Mathlib/Init/Data/Nat/Bitwise.lean | 24 ++++++++++++++----------
 1 file changed, 14 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index c80e5f2f486ae..165875f772ffb 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -1,7 +1,12 @@
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Harun Khan
+Authors: Mario Carneiro
+
+! This file was ported from Lean 3 source module init.data.nat.bitwise
+! leanprover-community/lean commit 53e8520d8964c7632989880372d91ba0cecbaf00
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Init.Data.Nat.Lemmas
 import Init.WFTactics
@@ -11,8 +16,6 @@ import Mathlib.Init.ZeroOne
 import Mathlib.Tactic.Cases
 import Mathlib.Tactic.PermuteGoals
 
-#align_import init.data.nat.bitwise from "leanprover-community/lean"@"53e8520d8964c7632989880372d91ba0cecbaf00"
-
 /-!
 # Lemmas about bitwise operations on natural numbers.
 
@@ -178,15 +181,19 @@ theorem bit_zero : bit false 0 = 0 :=
   rfl
 #align nat.bit_zero Nat.bit_zero
 
-@[simp] lemma bit_0 (b : Bool) : Nat.bit b 0 = b.toNat := by
+@[simp]
+lemma bit_0 (b : Bool) : Nat.bit b 0 = b.toNat := by
   cases' b <;> simp
 
-@[simp] lemma bit_1 (b : Bool) : Nat.bit b 1 = 2 + b.toNat:= by
+@[simp]
+lemma bit_1 (b : Bool) : Nat.bit b 1 = 2 + b.toNat:= by
   cases' b <;> simp
 
-@[simp] lemma shiftLeft_eq' {m n : Nat} : shiftLeft n m = n <<< m := rfl
+@[simp]
+lemma shiftLeft_eq' {m n : Nat} : shiftLeft n m = n <<< m := rfl
 
-@[simp] lemma shiftRight_eq {m n : Nat} : shiftRight n m = n >>> m := rfl
+@[simp]
+lemma shiftRight_eq {m n : Nat} : shiftRight n m = n >>> m := rfl
 
 @[simp]
 theorem shiftLeft_zero (m) : m <<< 0 = m := rfl
@@ -308,7 +315,6 @@ theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k
   | 0 => rfl
   | k + 1 => by
     simp only [shiftLeft_eq, Nat.mul_assoc, Nat.pow_add]
-#align nat.shiftl'_add Nat.shiftLeft_add
 
 theorem shiftRight_add (m n : Nat) : ∀ k, m >>> (n + k) = (m >>> n) >>> k
   | 0 => rfl
@@ -321,8 +327,6 @@ theorem shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<<
     simp only [shiftLeft_sub, Nat.le_of_succ_le_succ h]
     simp
 
-#align nat.shiftl'_sub Nat.shiftLeft_sub
-
 @[simp]
 theorem testBit_zero (b n) : testBit (bit b n) 0 = b :=
   bodd_bit _ _

From 16cde413dc15237384747bf4c9b2a93d8461c81f Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Fri, 4 Aug 2023 03:01:28 -0700
Subject: [PATCH 04/17] brougth back shiftl'

---
 Mathlib/Init/Data/Nat/Bitwise.lean | 40 +++++++++++++++++++++++-------
 1 file changed, 31 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index 165875f772ffb..3598159954558 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -181,6 +181,21 @@ theorem bit_zero : bit false 0 = 0 :=
   rfl
 #align nat.bit_zero Nat.bit_zero
 
+/--`shiftl' b m n` performs a left shift of `m` `n` times
+ and adds the bit `b` as the least significant bit each time.
+ Returns the corresponding natural number-/
+def shiftl' (b : Bool) (m : ℕ) : ℕ → ℕ
+  | 0 => m
+  | n + 1 => bit b (shiftl' b m n)
+#align nat.shiftl' Nat.shiftl'
+
+theorem shiftLeft_eq_shiftl'_false : ∀ n, shiftl' false m n = m <<< n
+  | 0 => rfl
+  | n + 1 => by
+    have : 2 * (m * 2^n) = 2^(n+1)*m := by
+      rw [Nat.mul_comm, Nat.mul_assoc, ← pow_succ]; simp
+    simp [shiftl', bit_val, shiftLeft_eq_shiftl'_false, this]
+
 @[simp]
 lemma bit_0 (b : Bool) : Nat.bit b 0 = b.toNat := by
   cases' b <;> simp
@@ -311,21 +326,28 @@ theorem div2_bit (b n) : div2 (bit b n) = n := by
   <;> exact by decide
 #align nat.div2_bit Nat.div2_bit
 
-theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k
+theorem shiftl'_add (b m n) : ∀ k, shiftl' b m (n + k) = shiftl' b (shiftl' b m n) k
   | 0 => rfl
-  | k + 1 => by
-    simp only [shiftLeft_eq, Nat.mul_assoc, Nat.pow_add]
+  | k + 1 => congr_arg (bit b) (shiftl'_add b m n k)
+#align nat.shiftl'_add Nat.shiftl'_add
+
+theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k := by
+  intro k; simp only [← shiftLeft_eq_shiftl'_false, shiftl'_add]
 
 theorem shiftRight_add (m n : Nat) : ∀ k, m >>> (n + k) = (m >>> n) >>> k
   | 0 => rfl
   | k + 1 => by simp [add_succ, shiftRight_add]
 
-theorem shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<< n) >>> k
-  | m, n, 0, _ => rfl
-  | m, n + 1, k + 1, h => by
-    rw [succ_sub_succ_eq_sub, shiftLeft_succ, Nat.add_comm, shiftRight_add]
-    simp only [shiftLeft_sub, Nat.le_of_succ_le_succ h]
-    simp
+theorem shiftl'_sub (b m) : ∀ {n k}, k ≤ n → shiftl' b m (n - k) = (shiftl' b m n) >>> k
+  | n, 0, _ => rfl
+  | n + 1, k + 1, h => by
+    rw [succ_sub_succ_eq_sub, shiftl', Nat.add_comm, shiftRight_add]
+    simp only [shiftl'_sub, Nat.le_of_succ_le_succ h, shiftRight_succ, shiftRight_zero]
+    simp [← div2_val, div2_bit]
+#align nat.shiftl'_sub Nat.shiftl'_sub
+
+theorem shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<< n) >>> k :=
+  fun _ _ _ hk => by simp only [← shiftLeft_eq_shiftl'_false, shiftl'_sub false _ hk]
 
 @[simp]
 theorem testBit_zero (b n) : testBit (bit b n) 0 = b :=

From a072dc622760901ac071ebf15c54ba009b51862a Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sat, 5 Aug 2023 01:43:21 -0700
Subject: [PATCH 05/17] fixed all bugs due to removing shiftl shiftr

---
 Mathlib/Data/Int/Bitwise.lean      | 38 ++++++++++---------
 Mathlib/Data/Nat/Bitwise.lean      |  9 +++--
 Mathlib/Data/Nat/Size.lean         | 51 ++++++++++---------------
 Mathlib/Data/Num/Lemmas.lean       | 60 ++++++++++++++----------------
 Mathlib/Init/Data/Int/Bitwise.lean |  4 +-
 Mathlib/Init/Data/Nat/Bitwise.lean |  6 ++-
 6 files changed, 78 insertions(+), 90 deletions(-)

diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean
index 798bbf8a1a1fe..bfb67294560e5 100644
--- a/Mathlib/Data/Int/Bitwise.lean
+++ b/Mathlib/Data/Int/Bitwise.lean
@@ -378,13 +378,13 @@ theorem shiftr_neg (m n : ℤ) : shiftr m (-n) = shiftl m n := by rw [← shiftl
 
 -- Porting note: what's the correct new name?
 @[simp]
-theorem shiftl_coe_nat (m n : ℕ) : shiftl m n = Nat.shiftl m n :=
-  rfl
+theorem shiftl_coe_nat (m n : ℕ) : shiftl m n = m <<< n :=
+  by simp [shiftl]
 #align int.shiftl_coe_nat Int.shiftl_coe_nat
 
 -- Porting note: what's the correct new name?
 @[simp]
-theorem shiftr_coe_nat (m n : ℕ) : shiftr m n = Nat.shiftr m n := by cases n <;> rfl
+theorem shiftr_coe_nat (m n : ℕ) : shiftr m n = m >>> n := by cases n <;> rfl
 #align int.shiftr_coe_nat Int.shiftr_coe_nat
 
 @[simp]
@@ -393,14 +393,14 @@ theorem shiftl_negSucc (m n : ℕ) : shiftl -[m+1] n = -[Nat.shiftl' true m n+1]
 #align int.shiftl_neg_succ Int.shiftl_negSucc
 
 @[simp]
-theorem shiftr_negSucc (m n : ℕ) : shiftr -[m+1] n = -[Nat.shiftr m n+1] := by cases n <;> rfl
+theorem shiftr_negSucc (m n : ℕ) : shiftr -[m+1] n = -[m >>> n+1] := by cases n <;> rfl
 #align int.shiftr_neg_succ Int.shiftr_negSucc
 
 theorem shiftr_add : ∀ (m : ℤ) (n k : ℕ), shiftr m (n + k) = shiftr (shiftr m n) k
   | (m : ℕ), n, k => by
-    rw [shiftr_coe_nat, shiftr_coe_nat, ← Int.ofNat_add, shiftr_coe_nat, Nat.shiftr_add]
+    rw [shiftr_coe_nat, shiftr_coe_nat, ← Int.ofNat_add, shiftr_coe_nat, Nat.shiftRight_add]
   | -[m+1], n, k => by
-    rw [shiftr_negSucc, shiftr_negSucc, ← Int.ofNat_add, shiftr_negSucc, Nat.shiftr_add]
+    rw [shiftr_negSucc, shiftr_negSucc, ← Int.ofNat_add, shiftr_negSucc, Nat.shiftRight_add]
 #align int.shiftr_add Int.shiftr_add
 
 /-! ### bitwise ops -/
@@ -408,22 +408,24 @@ theorem shiftr_add : ∀ (m : ℤ) (n k : ℕ), shiftr m (n + k) = shiftr (shift
 attribute [local simp] Int.zero_div
 
 theorem shiftl_add : ∀ (m : ℤ) (n : ℕ) (k : ℤ), shiftl m (n + k) = shiftl (shiftl m n) k
-  | (m : ℕ), n, (k : ℕ) => congr_arg ofNat (Nat.shiftl_add _ _ _)
+  | (m : ℕ), n, (k : ℕ) =>
+    congr_arg ofNat (by simp [Nat.pow_add, mul_assoc])
   | -[m+1], n, (k : ℕ) => congr_arg negSucc (Nat.shiftl'_add _ _ _ _)
   | (m : ℕ), n, -[k+1] =>
-    subNatNat_elim n k.succ (fun n k i => shiftl (↑m) i = Nat.shiftr (Nat.shiftl m n) k)
+    subNatNat_elim n k.succ (fun n k i => shiftl (↑m) i = (Nat.shiftl' false m n) >>> k)
       (fun (i n : ℕ) =>
-        by dsimp; rw [← Nat.shiftl_sub, add_tsub_cancel_left]; apply Nat.le_add_right)
+        by dsimp; simp [- Nat.shiftLeft_eq, ← Nat.shiftLeft_sub _ , add_tsub_cancel_left])
       fun i n =>
-        by dsimp; rw [add_assoc, Nat.shiftr_add, ← Nat.shiftl_sub, tsub_self] <;> rfl
+        by dsimp; simp [- Nat.shiftLeft_eq, Nat.shiftRight_add, ← Nat.shiftLeft_sub, shiftl]
   | -[m+1], n, -[k+1] =>
     subNatNat_elim n k.succ
-      (fun n k i => shiftl -[m+1] i = -[Nat.shiftr (Nat.shiftl' true m n) k+1])
+      (fun n k i => shiftl -[m+1] i = -[(Nat.shiftl' true m n) >>> k+1])
       (fun i n =>
         congr_arg negSucc <| by
           rw [← Nat.shiftl'_sub, add_tsub_cancel_left]; apply Nat.le_add_right)
       fun i n =>
-      congr_arg negSucc <| by rw [add_assoc, Nat.shiftr_add, ← Nat.shiftl'_sub, tsub_self] <;> rfl
+      congr_arg negSucc <| by rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftl'_sub, tsub_self]
+      <;> rfl
 #align int.shiftl_add Int.shiftl_add
 
 theorem shiftl_sub (m : ℤ) (n : ℕ) (k : ℤ) : shiftl m (n - k) = shiftr (shiftl m n) k :=
@@ -431,25 +433,25 @@ theorem shiftl_sub (m : ℤ) (n : ℕ) (k : ℤ) : shiftl m (n - k) = shiftr (sh
 #align int.shiftl_sub Int.shiftl_sub
 
 theorem shiftl_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), shiftl m n = m * ↑(2 ^ n)
-  | (m : ℕ), _ => congr_arg ((↑) : ℕ → ℤ) (Nat.shiftl_eq_mul_pow _ _)
+  | (m : ℕ), _ => congr_arg ((↑) : ℕ → ℤ) (by simp)
   | -[_+1], _ => @congr_arg ℕ ℤ _ _ (fun i => -i) (Nat.shiftl'_tt_eq_mul_pow _ _)
 #align int.shiftl_eq_mul_pow Int.shiftl_eq_mul_pow
 
 theorem shiftr_eq_div_pow : ∀ (m : ℤ) (n : ℕ), shiftr m n = m / ↑(2 ^ n)
-  | (m : ℕ), n => by rw [shiftr_coe_nat, Nat.shiftr_eq_div_pow _ _]; simp
+  | (m : ℕ), n => by rw [shiftr_coe_nat, Nat.shiftRight_eq_div_pow _ _]; simp
   | -[m+1], n => by
-    rw [shiftr_negSucc, negSucc_ediv, Nat.shiftr_eq_div_pow]; rfl
+    rw [shiftr_negSucc, negSucc_ediv, Nat.shiftRight_eq_div_pow]; rfl
     exact ofNat_lt_ofNat_of_lt (pow_pos (by decide) _)
 #align int.shiftr_eq_div_pow Int.shiftr_eq_div_pow
 
 theorem one_shiftl (n : ℕ) : shiftl 1 n = (2 ^ n : ℕ) :=
-  congr_arg ((↑) : ℕ → ℤ) (Nat.one_shiftl _)
+  congr_arg ((↑) : ℕ → ℤ) (by simp)
 #align int.one_shiftl Int.one_shiftl
 
 @[simp]
 theorem zero_shiftl : ∀ n : ℤ, shiftl 0 n = 0
-  | (n : ℕ) => congr_arg ((↑) : ℕ → ℤ) (Nat.zero_shiftl _)
-  | -[_+1] => congr_arg ((↑) : ℕ → ℤ) (Nat.zero_shiftr _)
+  | (n : ℕ) => congr_arg ((↑) : ℕ → ℤ) (by simp)
+  | -[_+1] => congr_arg ((↑) : ℕ → ℤ) (by simp)
 #align int.zero_shiftl Int.zero_shiftl
 
 @[simp]
diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index 1fe5565681c55..ddd2253150578 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -70,13 +70,14 @@ theorem zero_of_testBit_eq_false {n : ℕ} (h : ∀ i, testBit n i = false) : n
 #align nat.zero_of_test_bit_eq_ff Nat.zero_of_testBit_eq_false
 
 @[simp]
-theorem zero_testBit (i : ℕ) : testBit 0 i = false := by simp only [testBit, shiftr_zero, bodd_zero]
+theorem zero_testBit (i : ℕ) : testBit 0 i = false := by
+  simp only [testBit, zero_shiftRight, bodd_zero]
 #align nat.zero_test_bit Nat.zero_testBit
 
 /-- The ith bit is the ith element of `n.bits`. -/
 theorem testBit_eq_inth (n i : ℕ) : n.testBit i = n.bits.getI i := by
   induction' i with i ih generalizing n
-  · simp [testBit, shiftr, bodd_eq_bits_head, List.getI_zero_eq_headI]
+  · simp [testBit, bodd_eq_bits_head, List.getI_zero_eq_headI]
   conv_lhs => rw [← bit_decomp n]
   rw [testBit_succ, ih n.div2, div2_bits_eq_tail]
   cases n.bits <;> simp
@@ -140,11 +141,11 @@ theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : tes
 
 @[simp]
 theorem testBit_two_pow_self (n : ℕ) : testBit (2 ^ n) n = true := by
-  rw [testBit, shiftr_eq_div_pow, Nat.div_self (pow_pos (α := ℕ) zero_lt_two n), bodd_one]
+  rw [testBit, shiftRight_eq_div_pow, Nat.div_self (pow_pos (α := ℕ) zero_lt_two n), bodd_one]
 #align nat.test_bit_two_pow_self Nat.testBit_two_pow_self
 
 theorem testBit_two_pow_of_ne {n m : ℕ} (hm : n ≠ m) : testBit (2 ^ n) m = false := by
-  rw [testBit, shiftr_eq_div_pow]
+  rw [testBit, shiftRight_eq_div_pow]
   cases' hm.lt_or_lt with hm hm
   · rw [Nat.div_eq_zero, bodd_zero]
     exact Nat.pow_lt_pow_of_lt_right one_lt_two hm
diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index a396c16a759dc..f988a1a327dfa 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -20,15 +20,11 @@ namespace Nat
 section
 set_option linter.deprecated false
 
-theorem shiftl_eq_mul_pow (m) : ∀ n, shiftl m n = m * 2 ^ n
-  | 0 => (Nat.mul_one _).symm
-  | k + 1 => by
-    show bit0 (shiftl m k) = m * (2 ^ k * 2)
-    rw [bit0_val, shiftl_eq_mul_pow m k, mul_comm 2, mul_assoc]
-#align nat.shiftl_eq_mul_pow Nat.shiftl_eq_mul_pow
+theorem shiftLeft_eq_mul_pow (m) : ∀ n, m <<< n = m * 2 ^ n := shiftLeft_eq _
+#align nat.shiftl_eq_mul_pow Nat.shiftLeft_eq_mul_pow
 
 theorem shiftl'_tt_eq_mul_pow (m) : ∀ n, shiftl' true m n + 1 = (m + 1) * 2 ^ n
-  | 0 => by simp [shiftl, shiftl', pow_zero, Nat.one_mul]
+  | 0 => by simp [shiftl', pow_zero, Nat.one_mul]
   | k + 1 => by
     change bit1 (shiftl' true m k) + 1 = (m + 1) * (2 ^ k * 2)
     rw [bit1_val]
@@ -38,26 +34,17 @@ theorem shiftl'_tt_eq_mul_pow (m) : ∀ n, shiftl' true m n + 1 = (m + 1) * 2 ^
 
 end
 
-theorem one_shiftl (n) : shiftl 1 n = 2 ^ n :=
-  (shiftl_eq_mul_pow _ _).trans (Nat.one_mul _)
-#align nat.one_shiftl Nat.one_shiftl
-
 @[simp]
-theorem zero_shiftl (n) : shiftl 0 n = 0 :=
-  (shiftl_eq_mul_pow _ _).trans (Nat.zero_mul _)
+theorem zero_shiftl (n) : 0 <<< n = 0 :=
+  (shiftLeft_eq _ _).trans (Nat.zero_mul _)
 #align nat.zero_shiftl Nat.zero_shiftl
 
-theorem shiftr_eq_div_pow (m) : ∀ n, shiftr m n = m / 2 ^ n
+theorem shiftRight_eq_div_pow (m) : ∀ n, m >>> n = m / 2 ^ n
   | 0 => (Nat.div_one _).symm
-  | k + 1 =>
-    (congr_arg div2 (shiftr_eq_div_pow m k)).trans <| by
-      rw [div2_val, Nat.div_div_eq_div_mul, Nat.pow_succ]
-#align nat.shiftr_eq_div_pow Nat.shiftr_eq_div_pow
-
-@[simp]
-theorem zero_shiftr (n) : shiftr 0 n = 0 :=
-  (shiftr_eq_div_pow _ _).trans (Nat.zero_div _)
-#align nat.zero_shiftr Nat.zero_shiftr
+  | k + 1 => by
+    rw [shiftRight_add, shiftRight_eq_div_pow m k]
+    simp [Nat.div_div_eq_div_mul, ← Nat.pow_succ]
+#align nat.shiftr_eq_div_pow Nat.shiftRight_eq_div_pow
 
 theorem shiftl'_ne_zero_left (b) {m} (h : m ≠ 0) (n) : shiftl' b m n ≠ 0 := by
   induction n <;> simp [bit_ne_zero, shiftl', *]
@@ -123,25 +110,25 @@ theorem size_shiftl' {b m n} (h : shiftl' b m n ≠ 0) : size (shiftl' b m n) =
 #align nat.size_shiftl' Nat.size_shiftl'
 
 @[simp]
-theorem size_shiftl {m} (h : m ≠ 0) (n) : size (shiftl m n) = size m + n :=
-  size_shiftl' (shiftl'_ne_zero_left _ h _)
+theorem size_shiftl {m} (h : m ≠ 0) (n) : size (m  <<< n) = size m + n :=
+  by simp only [size_shiftl' (shiftl'_ne_zero_left _ h _), ← shiftLeft_eq_shiftl'_false]
 #align nat.size_shiftl Nat.size_shiftl
 
 theorem lt_size_self (n : ℕ) : n < 2 ^ size n := by
-  rw [← one_shiftl]
-  have : ∀ {n}, n = 0 → n < shiftl 1 (size n) := by simp
+  rw [← one_shiftLeft]
+  have : ∀ {n}, n = 0 → n < 1 <<< (size n) := by simp
   apply binaryRec _ _ n
   · apply this rfl
   intro b n IH
   by_cases h : bit b n = 0
   · apply this h
-  rw [size_bit h, shiftl_succ]
-  exact bit_lt_bit0 _ IH
+  rw [size_bit h, shiftLeft_succ, shiftLeft_eq, one_mul, ← bit0_val]
+  exact bit_lt_bit0 _ (by simpa [shiftRight_eq_div_pow] using IH)
 #align nat.lt_size_self Nat.lt_size_self
 
 theorem size_le {m n : ℕ} : size m ≤ n ↔ m < 2 ^ n :=
   ⟨fun h => lt_of_lt_of_le (lt_size_self _) (pow_le_pow_of_le_right (by decide) h), by
-    rw [← one_shiftl]; revert n
+    rw [← one_shiftLeft]; revert n
     apply binaryRec _ _ m
     · intro n
       simp
@@ -152,7 +139,9 @@ theorem size_le {m n : ℕ} : size m ≤ n ↔ m < 2 ^ n :=
       cases' n with n
       · exact e.elim (Nat.eq_zero_of_le_zero (le_of_lt_succ h))
       · apply succ_le_succ (IH _)
-        apply lt_imp_lt_of_le_imp_le (fun h' => bit0_le_bit _ h') h⟩
+        apply lt_of_mul_lt_mul_left _ (zero_le 2)
+        simp only [← bit0_val, shiftLeft_succ] at *
+        exact lt_of_le_of_lt (bit0_le_bit b rfl.le) h⟩
 #align nat.size_le Nat.size_le
 
 theorem lt_size {m n : ℕ} : m < size n ↔ 2 ^ m ≤ n := by
diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index 9039db9e248f3..dbd0bf5acbb07 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -955,45 +955,41 @@ theorem lxor'_to_nat : ∀ m n, (lxor m n : ℕ) = Nat.lxor' m n := by
 #align num.lxor_to_nat Num.lxor'_to_nat
 
 @[simp, norm_cast]
-theorem shiftl_to_nat (m n) : (shiftl m n : ℕ) = Nat.shiftl m n := by
+theorem shiftl_to_nat (m n) : (shiftl m n : ℕ) = Nat.shiftLeft m n := by
   cases m <;> dsimp only [shiftl]
   · symm
     apply Nat.zero_shiftl
   simp only [cast_pos]
   induction' n with n IH
   · rfl
-  simp [PosNum.shiftl_succ_eq_bit0_shiftl, Nat.shiftl_succ, IH]
+  simp [PosNum.shiftl_succ_eq_bit0_shiftl, Nat.shiftLeft_succ, IH,
+        Nat.bit0_val, pow_succ, ← mul_assoc, mul_comm]
 #align num.shiftl_to_nat Num.shiftl_to_nat
 
 @[simp, norm_cast]
-theorem shiftr_to_nat (m n) : (shiftr m n : ℕ) = Nat.shiftr m n := by
+theorem shiftr_to_nat (m n) : (shiftr m n : ℕ) = Nat.shiftRight m n := by
   cases' m with m <;> dsimp only [shiftr];
   · symm
-    apply Nat.zero_shiftr
+    apply Nat.zero_shiftRight
   induction' n with n IH generalizing m
   · cases m <;> rfl
   cases' m with m m <;> dsimp only [PosNum.shiftr]
-  · rw [Nat.shiftr_eq_div_pow]
+  · rw [Nat.shiftRight_eq, Nat.shiftRight_eq_div_pow]
     symm
     apply Nat.div_eq_of_lt
-    exact @Nat.pow_lt_pow_of_lt_right 2 (by decide) 0 (n + 1) (Nat.succ_pos _)
+    simp [@Nat.pow_lt_pow_of_lt_right 2 (by decide) 0 (n + 1) (Nat.succ_pos _)]
   · trans
     apply IH
-    change Nat.shiftr m n = Nat.shiftr (_root_.bit1 m) (n + 1)
-    rw [add_comm n 1, Nat.shiftr_add]
-    apply congr_arg fun x => Nat.shiftr x n
-    -- Porting note: `unfold` is not repeated in Lean4.
-    repeat unfold Nat.shiftr
-    change (m : ℕ) = Nat.div2 (Nat.bit true m)
-    rw [Nat.div2_bit]
+    change Nat.shiftRight m n = Nat.shiftRight (_root_.bit1 m) (n + 1)
+    rw [add_comm n 1, @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]
+    apply congr_arg fun x => Nat.shiftRight x n
+    simp [Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val]
   · trans
     apply IH
-    change Nat.shiftr m n = Nat.shiftr (_root_.bit0 m) (n + 1)
-    rw [add_comm n 1, Nat.shiftr_add]
-    apply congr_arg fun x => Nat.shiftr x n
-    repeat unfold Nat.shiftr
-    change (m : ℕ) = Nat.div2 (Nat.bit false m)
-    rw [Nat.div2_bit]
+    change Nat.shiftRight m n = Nat.shiftRight (_root_.bit0 m) (n + 1)
+    rw [add_comm n 1,  @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]
+    apply congr_arg fun x => Nat.shiftRight x n
+    simp [Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val]
 #align num.shiftr_to_nat Num.shiftr_to_nat
 
 @[simp]
@@ -1001,27 +997,25 @@ theorem testBit_to_nat (m n) : testBit m n = Nat.testBit m n := by
   -- Porting note: `unfold` → `dsimp only`
   cases m <;> dsimp only [testBit, Nat.testBit]
   case zero =>
-    change false = Nat.bodd (Nat.shiftr 0 n)
-    rw [Nat.zero_shiftr]
+    change false = Nat.bodd (0 >>> n)
+    rw [Nat.zero_shiftRight]
     rfl
   case pos m =>
     induction' n with n IH generalizing m <;> cases' m with m m <;> dsimp only [PosNum.testBit]
     · rfl
     · exact (Nat.bodd_bit _ _).symm
     · exact (Nat.bodd_bit _ _).symm
-    · change false = Nat.bodd (Nat.shiftr 1 (n + 1))
-      rw [add_comm, Nat.shiftr_add]
-      change false = Nat.bodd (Nat.shiftr 0 n)
-      rw [Nat.zero_shiftr]; rfl
-    · change PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.bit true m) (n + 1))
-      rw [add_comm, Nat.shiftr_add]
-      dsimp only [Nat.shiftr]
-      rw [Nat.div2_bit]
+    · change false = Nat.bodd (1 >>> (n + 1))
+      rw [add_comm, Nat.shiftRight_add]
+      change false = Nat.bodd (0 >>> n)
+      rw [Nat.zero_shiftRight]; rfl
+    · change PosNum.testBit m n = Nat.bodd ((Nat.bit true m) >>> (n + 1))
+      rw [add_comm, Nat.shiftRight_add]
+      simp only [Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, Nat.div2_bit]
       apply IH
-    · change PosNum.testBit m n = Nat.bodd (Nat.shiftr (Nat.bit false m) (n + 1))
-      rw [add_comm, Nat.shiftr_add]
-      dsimp only [Nat.shiftr]
-      rw [Nat.div2_bit]
+    · change PosNum.testBit m n = Nat.bodd ((Nat.bit false m) >>> (n + 1))
+      rw [add_comm, Nat.shiftRight_add]
+      simp only [Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, Nat.div2_bit]
       apply IH
 #align num.test_bit_to_nat Num.testBit_to_nat
 
diff --git a/Mathlib/Init/Data/Int/Bitwise.lean b/Mathlib/Init/Data/Int/Bitwise.lean
index 7a4535d60ed66..407522da1fccd 100644
--- a/Mathlib/Init/Data/Int/Bitwise.lean
+++ b/Mathlib/Init/Data/Int/Bitwise.lean
@@ -108,9 +108,9 @@ def lxor' : ℤ → ℤ → ℤ
   is obtained by left-shifting the binary representation of `m` by `n` places -/
 def shiftl : ℤ → ℤ → ℤ
   | (m : ℕ), (n : ℕ) => Nat.shiftl' false m n
-  | (m : ℕ), -[n +1] => Nat.shiftr m (Nat.succ n)
+  | (m : ℕ), -[n +1] => m >>> (Nat.succ n)
   | -[m +1], (n : ℕ) => -[Nat.shiftl' true m n +1]
-  | -[m +1], -[n +1] => -[Nat.shiftr m (Nat.succ n) +1]
+  | -[m +1], -[n +1] => -[m >>> (Nat.succ n) +1]
 #align int.shiftl Int.shiftl
 
 /-- `shiftr m n` produces an integer whose binary representation
diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index 3598159954558..095c5f9be0e47 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -189,6 +189,7 @@ def shiftl' (b : Bool) (m : ℕ) : ℕ → ℕ
   | n + 1 => bit b (shiftl' b m n)
 #align nat.shiftl' Nat.shiftl'
 
+@[simp]
 theorem shiftLeft_eq_shiftl'_false : ∀ n, shiftl' false m n = m <<< n
   | 0 => rfl
   | n + 1 => by
@@ -205,10 +206,10 @@ lemma bit_1 (b : Bool) : Nat.bit b 1 = 2 + b.toNat:= by
   cases' b <;> simp
 
 @[simp]
-lemma shiftLeft_eq' {m n : Nat} : shiftLeft n m = n <<< m := rfl
+lemma shiftLeft_eq' {m n : Nat} : shiftLeft m n = m <<< n := rfl
 
 @[simp]
-lemma shiftRight_eq {m n : Nat} : shiftRight n m = n >>> m := rfl
+lemma shiftRight_eq {m n : Nat} : shiftRight m n = m >>> n := rfl
 
 @[simp]
 theorem shiftLeft_zero (m) : m <<< 0 = m := rfl
@@ -223,6 +224,7 @@ theorem shiftRight_zero : n >>> 0 = n := rfl
 @[simp]
 theorem shiftRight_succ (m n) : m >>> (n + 1) = (m >>> n) / 2 := rfl
 
+@[simp]
 theorem zero_shiftRight : ∀ n, 0 >>> n = 0 := by
   intro n
   induction' n with n IH

From ea15870255b0f7b91b24a0297d65b0293171e687 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sat, 5 Aug 2023 02:52:39 -0700
Subject: [PATCH 06/17] fixed remaining files

---
 Mathlib/Data/FP/Basic.lean       | 8 ++++----
 Mathlib/Data/Ordmap/Ordnode.lean | 6 +++---
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Data/FP/Basic.lean b/Mathlib/Data/FP/Basic.lean
index de24f581e77ec..fe4ba517ceacb 100644
--- a/Mathlib/Data/FP/Basic.lean
+++ b/Mathlib/Data/FP/Basic.lean
@@ -19,8 +19,8 @@ import Mathlib.Data.Rat.Floor
 
 @[nolint docBlame]
 def Int.shift2 (a b : ℕ) : ℤ → ℕ × ℕ
-  | Int.ofNat e => (a.shiftl e, b)
-  | Int.negSucc e => (a, b.shiftl e.succ)
+  | Int.ofNat e => (a <<< e, b)
+  | Int.negSucc e => (a, b <<< e.succ)
 #align int.shift2 Int.shift2
 
 namespace FP
@@ -141,8 +141,8 @@ protected def Float.neg : Float → Float
 
 @[nolint docBlame]
 def divNatLtTwoPow (n d : ℕ) : ℤ → Bool
-  | Int.ofNat e => n < d.shiftl e
-  | Int.negSucc e => n.shiftl e.succ < d
+  | Int.ofNat e => n < d <<< e
+  | Int.negSucc e => n <<< e.succ < d
 #align fp.div_nat_lt_two_pow FP.divNatLtTwoPowₓ -- Porting note: TC argument `[C : FP.FloatCfg]` no longer present
 
 
diff --git a/Mathlib/Data/Ordmap/Ordnode.lean b/Mathlib/Data/Ordmap/Ordnode.lean
index 7a22c17beb925..394febbbc3464 100644
--- a/Mathlib/Data/Ordmap/Ordnode.lean
+++ b/Mathlib/Data/Ordmap/Ordnode.lean
@@ -879,11 +879,11 @@ def ofAscListAux₁ : ∀ l : List α, ℕ → Ordnode α × { l' : List α // l
   | x :: xs => fun s =>
     if s = 1 then (ι x, ⟨xs, Nat.le_succ _⟩)
     else
-      match ofAscListAux₁ xs (s.shiftl 1) with
+      match ofAscListAux₁ xs (s <<< 1) with
       | (t, ⟨[], _⟩) => (t, ⟨[], Nat.zero_le _⟩)
       | (l, ⟨y :: ys, h⟩) =>
         have := Nat.le_succ_of_le h
-        let (r, ⟨zs, h'⟩) := ofAscListAux₁ ys (s.shiftl 1)
+        let (r, ⟨zs, h'⟩) := ofAscListAux₁ ys (s <<< 1)
         (link l y r, ⟨zs, le_trans h' (le_of_lt this)⟩)
         termination_by ofAscListAux₁ l => l.length
 #align ordnode.of_asc_list_aux₁ Ordnode.ofAscListAux₁
@@ -895,7 +895,7 @@ def ofAscListAux₂ : List α → Ordnode α → ℕ → Ordnode α
     match ofAscListAux₁ xs s with
     | (r, ⟨ys, h⟩) =>
       have := Nat.lt_succ_of_le h
-      ofAscListAux₂ ys (link l x r) (s.shiftl 1)
+      ofAscListAux₂ ys (link l x r) (s <<< 1)
       termination_by ofAscListAux₂ l => l.length
 #align ordnode.of_asc_list_aux₂ Ordnode.ofAscListAux₂
 

From 6ca797143c90cccb7ffa9244601061587bc7aaf6 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sun, 6 Aug 2023 01:01:12 -0700
Subject: [PATCH 07/17] naming

---
 Mathlib/Data/Nat/Size.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index e10497eb65ac0..4bf0d2d6d0f70 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -32,9 +32,8 @@ theorem shiftl'_tt_eq_mul_pow (m) : ∀ n, shiftl' true m n + 1 = (m + 1) * 2 ^
 end
 
 @[simp]
-theorem zero_shiftl (n) : 0 <<< n = 0 :=
-  (shiftLeft_eq _ _).trans (Nat.zero_mul _)
-#align nat.zero_shiftl Nat.zero_shiftl
+theorem zero_shiftLeft (n) : 0 <<< n = 0 := by simp
+#align nat.zero_shiftl Nat.zero_shiftLeft
 
 theorem shiftRight_eq_div_pow (m) : ∀ n, m >>> n = m / 2 ^ n
   | 0 => (Nat.div_one _).symm
@@ -107,9 +106,9 @@ theorem size_shiftl' {b m n} (h : shiftl' b m n ≠ 0) : size (shiftl' b m n) =
 #align nat.size_shiftl' Nat.size_shiftl'
 
 @[simp]
-theorem size_shiftl {m} (h : m ≠ 0) (n) : size (m  <<< n) = size m + n :=
+theorem size_shiftLeft {m} (h : m ≠ 0) (n) : size (m <<< n) = size m + n :=
   by simp only [size_shiftl' (shiftl'_ne_zero_left _ h _), ← shiftLeft_eq_shiftl'_false]
-#align nat.size_shiftl Nat.size_shiftl
+#align nat.size_shiftl Nat.size_shiftLeft
 
 theorem lt_size_self (n : ℕ) : n < 2 ^ size n := by
   rw [← one_shiftLeft]

From 7c4bc985f201071caebca773997e89e7221436a3 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sun, 6 Aug 2023 01:35:06 -0700
Subject: [PATCH 08/17] fixed some simp normal form issues

---
 Mathlib/Data/Nat/Size.lean         | 1 -
 Mathlib/Init/Data/Nat/Bitwise.lean | 2 --
 2 files changed, 3 deletions(-)

diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index 4bf0d2d6d0f70..8dcb1b9ea2be7 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -31,7 +31,6 @@ theorem shiftl'_tt_eq_mul_pow (m) : ∀ n, shiftl' true m n + 1 = (m + 1) * 2 ^
 
 end
 
-@[simp]
 theorem zero_shiftLeft (n) : 0 <<< n = 0 := by simp
 #align nat.zero_shiftl Nat.zero_shiftLeft
 
diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index 63168513b343d..257c838d60250 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -208,10 +208,8 @@ lemma shiftLeft_eq' {m n : Nat} : shiftLeft m n = m <<< n := rfl
 @[simp]
 lemma shiftRight_eq {m n : Nat} : shiftRight m n = m >>> n := rfl
 
-@[simp]
 theorem shiftLeft_zero (m) : m <<< 0 = m := rfl
 
-@[simp]
 theorem shiftLeft_succ (m n) : m <<< (n + 1) = 2 * (m <<< n) := by
   simp only [shiftLeft_eq, Nat.pow_add, Nat.pow_one, ← Nat.mul_assoc, Nat.mul_comm]
 

From c7484d4d78c058b5e75140bb62ecbe90daf8b58a Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sun, 6 Aug 2023 02:13:52 -0700
Subject: [PATCH 09/17] fixed some build errors

---
 Mathlib/Data/Int/Bitwise.lean | 3 ++-
 Mathlib/Data/Num/Lemmas.lean  | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean
index 1ea7459f93539..58d9297e80e82 100644
--- a/Mathlib/Data/Int/Bitwise.lean
+++ b/Mathlib/Data/Int/Bitwise.lean
@@ -413,7 +413,8 @@ theorem shiftl_add : ∀ (m : ℤ) (n : ℕ) (k : ℤ), shiftl m (n + k) = shift
       (fun (i n : ℕ) =>
         by dsimp; simp [- Nat.shiftLeft_eq, ← Nat.shiftLeft_sub _ , add_tsub_cancel_left])
       fun i n =>
-        by dsimp; simp [- Nat.shiftLeft_eq, Nat.shiftRight_add, ← Nat.shiftLeft_sub, shiftl]
+        by dsimp; simp [- Nat.shiftLeft_eq, Nat.shiftLeft_zero, Nat.shiftRight_add,
+                        ← Nat.shiftLeft_sub, shiftl]
   | -[m+1], n, -[k+1] =>
     subNatNat_elim n k.succ
       (fun n k i => shiftl -[m+1] i = -[(Nat.shiftl' true m n) >>> k+1])
diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index b226129093122..5ef3e74e0dd87 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -955,7 +955,7 @@ theorem lxor'_to_nat : ∀ m n, (lxor m n : ℕ) = Nat.lxor' m n := by
 theorem shiftl_to_nat (m n) : (shiftl m n : ℕ) = Nat.shiftLeft m n := by
   cases m <;> dsimp only [shiftl]
   · symm
-    apply Nat.zero_shiftl
+    apply Nat.zero_shiftLeft
   simp only [cast_pos]
   induction' n with n IH
   · rfl

From 16ce204fe2554dc5677a7b25eaea0816977bbd74 Mon Sep 17 00:00:00 2001
From: mhk119 <58151072+mhk119@users.noreply.github.com>
Date: Sun, 6 Aug 2023 03:01:45 -0700
Subject: [PATCH 10/17] Update Mathlib/Init/Data/Nat/Bitwise.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Init/Data/Nat/Bitwise.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index 257c838d60250..b6f02be413524 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -195,7 +195,7 @@ theorem shiftLeft_eq_shiftl'_false : ∀ n, shiftl' false m n = m <<< n
     simp [shiftl', bit_val, shiftLeft_eq_shiftl'_false, this]
 
 @[simp]
-lemma bit_0 (b : Bool) : Nat.bit b 0 = b.toNat := by
+lemma bit_zero (b : Bool) : Nat.bit b 0 = b.toNat := by
   cases' b <;> simp
 
 @[simp]

From e0005a6679a91e82342ad0793b63551db0d31f25 Mon Sep 17 00:00:00 2001
From: mhk119 <58151072+mhk119@users.noreply.github.com>
Date: Sun, 6 Aug 2023 03:52:39 -0700
Subject: [PATCH 11/17] Update Mathlib/Data/Num/Lemmas.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Data/Num/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index 5ef3e74e0dd87..ae547eec29ef2 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -952,7 +952,7 @@ theorem lxor'_to_nat : ∀ m n, (lxor m n : ℕ) = Nat.lxor' m n := by
 #align num.lxor_to_nat Num.lxor'_to_nat
 
 @[simp, norm_cast]
-theorem shiftl_to_nat (m n) : (shiftl m n : ℕ) = Nat.shiftLeft m n := by
+theorem shiftl_to_nat (m n) : (shiftl m n : ℕ) = (m : ℕ) <<< (n : ℕ) := by
   cases m <;> dsimp only [shiftl]
   · symm
     apply Nat.zero_shiftLeft

From 77d2ed4e44578d6281aa2b8435e226c99de10e34 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sun, 6 Aug 2023 15:41:45 -0700
Subject: [PATCH 12/17] changes based on the review

---
 Mathlib/Data/Nat/Size.lean         | 2 ++
 Mathlib/Data/Num/Lemmas.lean       | 6 +++---
 Mathlib/Init/Data/Nat/Bitwise.lean | 8 --------
 3 files changed, 5 insertions(+), 11 deletions(-)

diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index 8dcb1b9ea2be7..522dee645af0f 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -34,6 +34,8 @@ end
 theorem zero_shiftLeft (n) : 0 <<< n = 0 := by simp
 #align nat.zero_shiftl Nat.zero_shiftLeft
 
+#align nat.one_shiftl Nat.one_shiftLeft
+
 theorem shiftRight_eq_div_pow (m) : ∀ n, m >>> n = m / 2 ^ n
   | 0 => (Nat.div_one _).symm
   | k + 1 => by
diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index 5ef3e74e0dd87..a9a0b81ad8a2c 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -952,7 +952,7 @@ theorem lxor'_to_nat : ∀ m n, (lxor m n : ℕ) = Nat.lxor' m n := by
 #align num.lxor_to_nat Num.lxor'_to_nat
 
 @[simp, norm_cast]
-theorem shiftl_to_nat (m n) : (shiftl m n : ℕ) = Nat.shiftLeft m n := by
+theorem shiftl_to_nat (m n) : (shiftl m n : ℕ) = (m : ℕ) <<< (n : ℕ) := by
   cases m <;> dsimp only [shiftl]
   · symm
     apply Nat.zero_shiftLeft
@@ -965,14 +965,14 @@ theorem shiftl_to_nat (m n) : (shiftl m n : ℕ) = Nat.shiftLeft m n := by
 
 @[simp, norm_cast]
 
-theorem shiftr_to_nat (m n) : (shiftr m n : ℕ) = Nat.shiftRight m n := by
+theorem shiftr_to_nat (m n) : (shiftr m n : ℕ) = (m : ℕ) >>> (n : ℕ)  := by
   cases' m with m <;> dsimp only [shiftr];
   · symm
     apply Nat.zero_shiftRight
   induction' n with n IH generalizing m
   · cases m <;> rfl
   cases' m with m m <;> dsimp only [PosNum.shiftr]
-  · rw [Nat.shiftRight_eq, Nat.shiftRight_eq_div_pow]
+  · rw [Nat.shiftRight_eq_div_pow]
     symm
     apply Nat.div_eq_of_lt
     simp [@Nat.pow_lt_pow_of_lt_right 2 (by decide) 0 (n + 1) (Nat.succ_pos _)]
diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index 257c838d60250..5603b46c5b5be 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -194,14 +194,6 @@ theorem shiftLeft_eq_shiftl'_false : ∀ n, shiftl' false m n = m <<< n
       rw [Nat.mul_comm, Nat.mul_assoc, ← pow_succ]; simp
     simp [shiftl', bit_val, shiftLeft_eq_shiftl'_false, this]
 
-@[simp]
-lemma bit_0 (b : Bool) : Nat.bit b 0 = b.toNat := by
-  cases' b <;> simp
-
-@[simp]
-lemma bit_1 (b : Bool) : Nat.bit b 1 = 2 + b.toNat:= by
-  cases' b <;> simp
-
 @[simp]
 lemma shiftLeft_eq' {m n : Nat} : shiftLeft m n = m <<< n := rfl
 

From 490a0ed98171e0aa543a63c9f051fb480aa84777 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sun, 6 Aug 2023 15:49:04 -0700
Subject: [PATCH 13/17] delete bit_0 and bit_1

---
 Mathlib/Init/Data/Nat/Bitwise.lean | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index b6f02be413524..5603b46c5b5be 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -194,14 +194,6 @@ theorem shiftLeft_eq_shiftl'_false : ∀ n, shiftl' false m n = m <<< n
       rw [Nat.mul_comm, Nat.mul_assoc, ← pow_succ]; simp
     simp [shiftl', bit_val, shiftLeft_eq_shiftl'_false, this]
 
-@[simp]
-lemma bit_zero (b : Bool) : Nat.bit b 0 = b.toNat := by
-  cases' b <;> simp
-
-@[simp]
-lemma bit_1 (b : Bool) : Nat.bit b 1 = 2 + b.toNat:= by
-  cases' b <;> simp
-
 @[simp]
 lemma shiftLeft_eq' {m n : Nat} : shiftLeft m n = m <<< n := rfl
 

From 73694a5d016ea060fe0120db6589a2cad2ec5d46 Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sun, 6 Aug 2023 17:57:00 -0700
Subject: [PATCH 14/17] swapped order

---
 Mathlib/Data/Nat/Size.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index 522dee645af0f..a7649a1a9c6c1 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -31,11 +31,11 @@ theorem shiftl'_tt_eq_mul_pow (m) : ∀ n, shiftl' true m n + 1 = (m + 1) * 2 ^
 
 end
 
+#align nat.one_shiftl Nat.one_shiftLeft
+
 theorem zero_shiftLeft (n) : 0 <<< n = 0 := by simp
 #align nat.zero_shiftl Nat.zero_shiftLeft
 
-#align nat.one_shiftl Nat.one_shiftLeft
-
 theorem shiftRight_eq_div_pow (m) : ∀ n, m >>> n = m / 2 ^ n
   | 0 => (Nat.div_one _).symm
   | k + 1 => by

From 955a9a7f093381816d02d5c9e1106d5836003e9d Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 21 Aug 2023 21:42:32 +0000
Subject: [PATCH 15/17] fix lemma name

---
 Mathlib/Data/Nat/Size.lean         | 2 +-
 Mathlib/Init/Data/Nat/Bitwise.lean | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index a7649a1a9c6c1..f71ef1010145c 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -108,7 +108,7 @@ theorem size_shiftl' {b m n} (h : shiftl' b m n ≠ 0) : size (shiftl' b m n) =
 
 @[simp]
 theorem size_shiftLeft {m} (h : m ≠ 0) (n) : size (m <<< n) = size m + n :=
-  by simp only [size_shiftl' (shiftl'_ne_zero_left _ h _), ← shiftLeft_eq_shiftl'_false]
+  by simp only [size_shiftl' (shiftl'_ne_zero_left _ h _), ← shiftl'_false]
 #align nat.size_shiftl Nat.size_shiftLeft
 
 theorem lt_size_self (n : ℕ) : n < 2 ^ size n := by
diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index 5603b46c5b5be..e5fb920d08eac 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -187,12 +187,12 @@ def shiftl' (b : Bool) (m : ℕ) : ℕ → ℕ
 #align nat.shiftl' Nat.shiftl'
 
 @[simp]
-theorem shiftLeft_eq_shiftl'_false : ∀ n, shiftl' false m n = m <<< n
+theorem shiftl'_false : ∀ n, shiftl' false m n = m <<< n
   | 0 => rfl
   | n + 1 => by
     have : 2 * (m * 2^n) = 2^(n+1)*m := by
       rw [Nat.mul_comm, Nat.mul_assoc, ← pow_succ]; simp
-    simp [shiftl', bit_val, shiftLeft_eq_shiftl'_false, this]
+    simp [shiftl', bit_val, shiftl'_false, this]
 
 @[simp]
 lemma shiftLeft_eq' {m n : Nat} : shiftLeft m n = m <<< n := rfl
@@ -321,7 +321,7 @@ theorem shiftl'_add (b m n) : ∀ k, shiftl' b m (n + k) = shiftl' b (shiftl' b
 #align nat.shiftl'_add Nat.shiftl'_add
 
 theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k := by
-  intro k; simp only [← shiftLeft_eq_shiftl'_false, shiftl'_add]
+  intro k; simp only [← shiftl'_false, shiftl'_add]
 
 theorem shiftRight_add (m n : Nat) : ∀ k, m >>> (n + k) = (m >>> n) >>> k
   | 0 => rfl
@@ -336,7 +336,7 @@ theorem shiftl'_sub (b m) : ∀ {n k}, k ≤ n → shiftl' b m (n - k) = (shiftl
 #align nat.shiftl'_sub Nat.shiftl'_sub
 
 theorem shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<< n) >>> k :=
-  fun _ _ _ hk => by simp only [← shiftLeft_eq_shiftl'_false, shiftl'_sub false _ hk]
+  fun _ _ _ hk => by simp only [← shiftl'_false, shiftl'_sub false _ hk]
 
 @[simp]
 theorem testBit_zero (b n) : testBit (bit b n) 0 = b :=

From 04e9677fdaadfe24c36aba54f3edb0f064460c47 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 21 Aug 2023 21:48:01 +0000
Subject: [PATCH 16/17] nolint

---
 Mathlib/Data/Nat/Size.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index f71ef1010145c..17c8483a37746 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -106,7 +106,9 @@ theorem size_shiftl' {b m n} (h : shiftl' b m n ≠ 0) : size (shiftl' b m n) =
   rfl
 #align nat.size_shiftl' Nat.size_shiftl'
 
-@[simp]
+-- TODO: decide whether `Nat.shiftLeft_eq` (which rewrites the LHS into a power) should be a simp
+-- lemma; it was not in mathlib3. Until then, tell the simpNF linter to ignore the issue.
+@[simp, nolint simpNF]
 theorem size_shiftLeft {m} (h : m ≠ 0) (n) : size (m <<< n) = size m + n :=
   by simp only [size_shiftl' (shiftl'_ne_zero_left _ h _), ← shiftl'_false]
 #align nat.size_shiftl Nat.size_shiftLeft

From 4695dd5967133a26b301f1982f28de179a85ace5 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 25 Aug 2023 12:20:06 +0100
Subject: [PATCH 17/17] Add comment explaining prime

---
 Mathlib/Init/Data/Nat/Bitwise.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
index e5fb920d08eac..9319164cb46b8 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -194,11 +194,12 @@ theorem shiftl'_false : ∀ n, shiftl' false m n = m <<< n
       rw [Nat.mul_comm, Nat.mul_assoc, ← pow_succ]; simp
     simp [shiftl', bit_val, shiftl'_false, this]
 
+/-- Std4 takes the unprimed name for `Nat.shiftLeft_eq m n : m <<< n = m * 2 ^ n`. -/
 @[simp]
-lemma shiftLeft_eq' {m n : Nat} : shiftLeft m n = m <<< n := rfl
+lemma shiftLeft_eq' (m n : Nat) : shiftLeft m n = m <<< n := rfl
 
 @[simp]
-lemma shiftRight_eq {m n : Nat} : shiftRight m n = m >>> n := rfl
+lemma shiftRight_eq (m n : Nat) : shiftRight m n = m >>> n := rfl
 
 theorem shiftLeft_zero (m) : m <<< 0 = m := rfl