chore: rename Nat.shiftl' to Nat.shiftLeft' (#6788)

This makes it match the unprimed `Nat.shiftLeft`.

Follows on from #6356 which removed `Nat.shiftl`.

Author: eric-wieser

Mathlib/Data/Int/Bitwise.lean

@@ -385,7 +385,7 @@ 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]
-theorem shiftl_negSucc (m n : ℕ) : shiftl -[m+1] n = -[Nat.shiftl' true m n+1] :=
+theorem shiftl_negSucc (m n : ℕ) : shiftl -[m+1] n = -[Nat.shiftLeft' true m n+1] :=
   rfl
 #align int.shiftl_neg_succ Int.shiftl_negSucc
 
@@ -407,22 +407,22 @@ 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 (by simp [Nat.pow_add, mul_assoc])
-  | -[m+1], n, (k : ℕ) => congr_arg negSucc (Nat.shiftl'_add _ _ _ _)
+  | -[m+1], n, (k : ℕ) => congr_arg negSucc (Nat.shiftLeft'_add _ _ _ _)
   | (m : ℕ), n, -[k+1] =>
-    subNatNat_elim n k.succ (fun n k i => shiftl (↑m) i = (Nat.shiftl' false m n) >>> k)
+    subNatNat_elim n k.succ (fun n k i => shiftl (↑m) i = (Nat.shiftLeft' false m n) >>> k)
       (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.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])
+      (fun n k i => shiftl -[m+1] i = -[(Nat.shiftLeft' 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)
+          rw [← Nat.shiftLeft'_sub, add_tsub_cancel_left]; apply Nat.le_add_right)
       fun i n =>
-      congr_arg negSucc <| by rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftl'_sub, tsub_self]
+      congr_arg negSucc <| by rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub, tsub_self]
       <;> rfl
 #align int.shiftl_add Int.shiftl_add
 
@@ -432,7 +432,7 @@ theorem shiftl_sub (m : ℤ) (n : ℕ) (k : ℤ) : shiftl m (n - k) = shiftr (sh
 
 theorem shiftl_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), shiftl m n = m * ↑(2 ^ n)
   | (m : ℕ), _ => congr_arg ((↑) : ℕ → ℤ) (by simp)
-  | -[_+1], _ => @congr_arg ℕ ℤ _ _ (fun i => -i) (Nat.shiftl'_tt_eq_mul_pow _ _)
+  | -[_+1], _ => @congr_arg ℕ ℤ _ _ (fun i => -i) (Nat.shiftLeft'_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)

Mathlib/Data/Nat/Bits.lean

@@ -17,7 +17,7 @@ which allows us to more easily work with operations which do depend
 on the number of leading zeros in the binary representation of `n`.
 For example, we can more easily work with `Nat.bits` and `Nat.size`.
 
-See also: `Nat.bitwise`, `Nat.pow` (for various lemmas about `size` and `shiftl`/`shiftr`),
+See also: `Nat.bitwise`, `Nat.pow` (for various lemmas about `size` and `shiftLeft`/`shiftRight`),
 and `Nat.digits`.
 -/
 

Mathlib/Data/Nat/Size.lean

@@ -12,22 +12,22 @@ import Mathlib.Data.Nat.Bits
 
 namespace Nat
 
-/-! ### `shiftl` and `shiftr` -/
+/-! ### `shiftLeft` and `shiftRight` -/
 
 section
 set_option linter.deprecated false
 
 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', pow_zero, Nat.one_mul]
+theorem shiftLeft'_tt_eq_mul_pow (m) : ∀ n, shiftLeft' true m n + 1 = (m + 1) * 2 ^ n
+  | 0 => by simp [shiftLeft', pow_zero, Nat.one_mul]
   | k + 1 => by
-    change bit1 (shiftl' true m k) + 1 = (m + 1) * (2 ^ k * 2)
+    change bit1 (shiftLeft' true m k) + 1 = (m + 1) * (2 ^ k * 2)
     rw [bit1_val]
-    change 2 * (shiftl' true m k + 1) = _
-    rw [shiftl'_tt_eq_mul_pow m k, mul_left_comm, mul_comm 2]
-#align nat.shiftl'_tt_eq_mul_pow Nat.shiftl'_tt_eq_mul_pow
+    change 2 * (shiftLeft' true m k + 1) = _
+    rw [shiftLeft'_tt_eq_mul_pow m k, mul_left_comm, mul_comm 2]
+#align nat.shiftl'_tt_eq_mul_pow Nat.shiftLeft'_tt_eq_mul_pow
 
 end
 
@@ -43,14 +43,14 @@ theorem shiftRight_eq_div_pow (m) : ∀ n, m >>> n = m / 2 ^ n
     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', *]
-#align nat.shiftl'_ne_zero_left Nat.shiftl'_ne_zero_left
+theorem shiftLeft'_ne_zero_left (b) {m} (h : m ≠ 0) (n) : shiftLeft' b m n ≠ 0 := by
+  induction n <;> simp [bit_ne_zero, shiftLeft', *]
+#align nat.shiftl'_ne_zero_left Nat.shiftLeft'_ne_zero_left
 
-theorem shiftl'_tt_ne_zero (m) : ∀ {n}, (n ≠ 0) → shiftl' true m n ≠ 0
+theorem shiftLeft'_tt_ne_zero (m) : ∀ {n}, (n ≠ 0) → shiftLeft' true m n ≠ 0
   | 0, h => absurd rfl h
   | succ _, _ => Nat.bit1_ne_zero _
-#align nat.shiftl'_tt_ne_zero Nat.shiftl'_tt_ne_zero
+#align nat.shiftl'_tt_ne_zero Nat.shiftLeft'_tt_ne_zero
 
 /-! ### `size` -/
 
@@ -90,27 +90,28 @@ theorem size_one : size 1 = 1 :=
 end
 
 @[simp]
-theorem size_shiftl' {b m n} (h : shiftl' b m n ≠ 0) : size (shiftl' b m n) = size m + n := by
-  induction' n with n IH <;> simp [shiftl'] at h ⊢
+theorem size_shiftLeft' {b m n} (h : shiftLeft' b m n ≠ 0) :
+    size (shiftLeft' b m n) = size m + n := by
+  induction' n with n IH <;> simp [shiftLeft'] at h ⊢
   rw [size_bit h, Nat.add_succ]
-  by_cases s0 : shiftl' b m n = 0 <;> [skip; rw [IH s0]]
+  by_cases s0 : shiftLeft' b m n = 0 <;> [skip; rw [IH s0]]
   rw [s0] at h ⊢
   cases b; · exact absurd rfl h
-  have : shiftl' true m n + 1 = 1 := congr_arg (· + 1) s0
-  rw [shiftl'_tt_eq_mul_pow] at this
+  have : shiftLeft' true m n + 1 = 1 := congr_arg (· + 1) s0
+  rw [shiftLeft'_tt_eq_mul_pow] at this
   obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)
   simp only [zero_add, one_mul] at this
   obtain rfl : n = 0 :=
     Nat.eq_zero_of_le_zero
       (le_of_not_gt fun hn => ne_of_gt (pow_lt_pow_of_lt_right (by decide) hn) this)
   rfl
-#align nat.size_shiftl' Nat.size_shiftl'
+#align nat.size_shiftl' Nat.size_shiftLeft'
 
 -- 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]
+  by simp only [size_shiftLeft' (shiftLeft'_ne_zero_left _ h _), ← shiftLeft'_false]
 #align nat.size_shiftl Nat.size_shiftLeft
 
 theorem lt_size_self (n : ℕ) : n < 2 ^ size n := by

Mathlib/Init/Data/Int/Bitwise.lean

@@ -104,9 +104,9 @@ def lxor' : ℤ → ℤ → ℤ
 /-- `shiftl m n` produces an integer whose binary representation
   is obtained by left-shifting the binary representation of `m` by `n` places -/
 def shiftl : ℤ → ℤ → ℤ
-  | (m : ℕ), (n : ℕ) => Nat.shiftl' false m n
+  | (m : ℕ), (n : ℕ) => Nat.shiftLeft' false m n
   | (m : ℕ), -[n +1] => m >>> (Nat.succ n)
-  | -[m +1], (n : ℕ) => -[Nat.shiftl' true m n +1]
+  | -[m +1], (n : ℕ) => -[Nat.shiftLeft' true m n +1]
   | -[m +1], -[n +1] => -[m >>> (Nat.succ n) +1]
 #align int.shiftl Int.shiftl
 

Mathlib/Init/Data/Nat/Bitwise.lean

@@ -180,21 +180,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
+/--`shiftLeft' 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 : ℕ) : ℕ → ℕ
+def shiftLeft' (b : Bool) (m : ℕ) : ℕ → ℕ
   | 0 => m
-  | n + 1 => bit b (shiftl' b m n)
-#align nat.shiftl' Nat.shiftl'
+  | n + 1 => bit b (shiftLeft' b m n)
+#align nat.shiftl' Nat.shiftLeft'
 
 @[simp]
-theorem shiftl'_false : ∀ n, shiftl' false m n = m <<< n
+theorem shiftLeft'_false : ∀ n, shiftLeft' 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]
+    simp [shiftLeft', bit_val, shiftLeft'_false, this]
 
 /-- Std4 takes the unprimed name for `Nat.shiftLeft_eq m n : m <<< n = m * 2 ^ n`. -/
 @[simp]
@@ -318,28 +318,28 @@ 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 (b m n) : ∀ k, shiftLeft' b m (n + k) = shiftLeft' b (shiftLeft' b m n) k
   | 0 => rfl
-  | k + 1 => congr_arg (bit b) (shiftl'_add b m n k)
-#align nat.shiftl'_add Nat.shiftl'_add
+  | k + 1 => congr_arg (bit b) (shiftLeft'_add b m n k)
+#align nat.shiftl'_add Nat.shiftLeft'_add
 
 theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k := by
-  intro k; simp only [← shiftl'_false, shiftl'_add]
+  intro k; simp only [← shiftLeft'_false, shiftLeft'_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 shiftl'_sub (b m) : ∀ {n k}, k ≤ n → shiftl' b m (n - k) = (shiftl' b m n) >>> k
+theorem shiftLeft'_sub (b m) : ∀ {n k}, k ≤ n → shiftLeft' b m (n - k) = (shiftLeft' 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]
+    rw [succ_sub_succ_eq_sub, shiftLeft', Nat.add_comm, shiftRight_add]
+    simp only [shiftLeft'_sub, Nat.le_of_succ_le_succ h, shiftRight_succ, shiftRight_zero]
     simp [← div2_val, div2_bit]
-#align nat.shiftl'_sub Nat.shiftl'_sub
+#align nat.shiftl'_sub Nat.shiftLeft'_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]
+  fun _ _ _ hk => by simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk]
 
 @[simp]
 theorem testBit_zero (b n) : testBit (bit b n) 0 = b :=