diff --git a/Mathlib/Data/FP/Basic.lean b/Mathlib/Data/FP/Basic.lean
index 72e9e4b4ef2b5..d1d2bb060cc8a 100644
--- a/Mathlib/Data/FP/Basic.lean
+++ b/Mathlib/Data/FP/Basic.lean
@@ -16,8 +16,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
@@ -138,8 +138,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/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean
index 915627f7736d9..58d9297e80e82 100644
--- a/Mathlib/Data/Int/Bitwise.lean
+++ b/Mathlib/Data/Int/Bitwise.lean
@@ -375,13 +375,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]
@@ -390,14 +390,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 -/
@@ -405,22 +405,25 @@ 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.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.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 :=
@@ -428,25 +431,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 c3a12b456462f..4883bdbf3c6ad 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -67,13 +67,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
@@ -137,11 +138,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 de327a3280566..17c8483a37746 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -17,15 +17,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]
@@ -35,26 +31,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
+#align nat.one_shiftl Nat.one_shiftLeft
 
-@[simp]
-theorem zero_shiftl (n) : shiftl 0 n = 0 :=
-  (shiftl_eq_mul_pow _ _).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 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', *]
@@ -119,26 +106,28 @@ 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]
-theorem size_shiftl {m} (h : m ≠ 0) (n) : size (shiftl m n) = size m + n :=
-  size_shiftl' (shiftl'_ne_zero_left _ h _)
-#align nat.size_shiftl Nat.size_shiftl
+-- 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
 
 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
@@ -149,7 +138,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 0bca3ad093020..a9a0b81ad8a2c 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -952,45 +952,42 @@ 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 : ℕ) = (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
-  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
-  cases' m with m <;> dsimp only [shiftr]
+
+theorem shiftr_to_nat (m n) : (shiftr m n : ℕ) = (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_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]
@@ -998,27 +995,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/Data/Ordmap/Ordnode.lean b/Mathlib/Data/Ordmap/Ordnode.lean
index 8f1de80579e88..21c311db520a3 100644
--- a/Mathlib/Data/Ordmap/Ordnode.lean
+++ b/Mathlib/Data/Ordmap/Ordnode.lean
@@ -874,11 +874,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₁
@@ -890,7 +890,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₂
 
diff --git a/Mathlib/Init/Data/Int/Bitwise.lean b/Mathlib/Init/Data/Int/Bitwise.lean
index 41106dfbf6760..cb1d2b4c1d698 100644
--- a/Mathlib/Init/Data/Int/Bitwise.lean
+++ b/Mathlib/Init/Data/Int/Bitwise.lean
@@ -105,9 +105,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 2074019c1b7aa..9319164cb46b8 100644
--- a/Mathlib/Init/Data/Nat/Bitwise.lean
+++ b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -186,41 +186,44 @@ def shiftl' (b : Bool) (m : ℕ) : ℕ → ℕ
   | n + 1 => bit b (shiftl' b m n)
 #align nat.shiftl' Nat.shiftl'
 
-/-- `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]
+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, shiftl'_false, this]
 
+/-- Std4 takes the unprimed name for `Nat.shiftLeft_eq m n : m <<< n = m * 2 ^ n`. -/
 @[simp]
-theorem shiftl_zero (m) : shiftl m 0 = m :=
-  rfl
-#align nat.shiftl_zero Nat.shiftl_zero
+lemma shiftLeft_eq' (m n : Nat) : shiftLeft m n = m <<< n := rfl
 
 @[simp]
-theorem shiftl_succ (m n) : shiftl m (n + 1) = bit0 (shiftl m n) :=
-  rfl
-#align nat.shiftl_succ Nat.shiftl_succ
+lemma shiftRight_eq (m n : Nat) : shiftRight m n = m >>> n := rfl
+
+theorem shiftLeft_zero (m) : m <<< 0 = m := rfl
 
-/--`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 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]
 
-theorem shiftr_zero : ∀ n, shiftr 0 n = 0 := by
+@[simp]
+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
   case zero =>
-    rw [shiftr]
+    simp [shiftRight]
   case succ =>
-    rw [shiftr, div2, 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 (shiftr m n)
+  bodd (m >>> n)
 #align nat.test_bit Nat.testBit
 
 
@@ -318,27 +321,23 @@ theorem shiftl'_add (b m n) : ∀ k, shiftl' b m (n + k) = shiftl' b (shiftl' b
   | 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
+theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k := by
+  intro k; simp only [← shiftl'_false, shiftl'_add]
 
-theorem shiftr_add (m n) : ∀ k, shiftr m (n + k) = shiftr (shiftr m n) k
+theorem shiftRight_add (m n : Nat) : ∀ k, m >>> (n + k) = (m >>> n) >>> k
   | 0 => rfl
-  | k + 1 => congr_arg div2 (shiftr_add m n k)
-#align nat.shiftr_add Nat.shiftr_add
+  | k + 1 => by simp [add_succ, shiftRight_add]
 
-theorem shiftl'_sub (b m) : ∀ {n k}, k ≤ n → shiftl' b m (n - k) = shiftr (shiftl' b m n) k
+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
-    simp [shiftl']
-    rw [Nat.add_comm, shiftr_add]
-    simp [shiftr, div2_bit]
-    simp [shiftl'_sub, (Nat.le_of_succ_le_succ h)]
+    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 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
+theorem shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<< n) >>> k :=
+  fun _ _ _ hk => by simp only [← shiftl'_false, shiftl'_sub false _ hk]
 
 @[simp]
 theorem testBit_zero (b n) : testBit (bit b n) 0 = b :=
@@ -346,10 +345,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 (((bit b n) >>> 1) >>> m) = bodd (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