From 42215cc0728fbee0705acf87995a8720ec8bcc0d Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Mon, 20 May 2024 08:50:28 +0200
Subject: [PATCH] feat: `Nat.shiftLeft_shiftRight` (#4199)

Show that shifting a natural number left and then shifting right by the
same amount is a no-op.

I originally proved this in a different PR, ended up not needing the
fact after all, but it still seemed like a generally useful simp lemma
to have.
---
 src/Init/Data/Nat/Lemmas.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index e59b9680ce..d6c69b4c1c 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -794,6 +794,9 @@ theorem shiftLeft_shiftLeft (m n : Nat) : ∀ k, (m <<< n) <<< k = m <<< (n + k)
   | 0 => rfl
   | k + 1 => by simp [← Nat.add_assoc, shiftLeft_shiftLeft _ _ k, shiftLeft_succ]
 
+@[simp] theorem shiftLeft_shiftRight (x n : Nat) : x <<< n >>> n = x := by
+  rw [Nat.shiftLeft_eq, Nat.shiftRight_eq_div_pow, Nat.mul_div_cancel _ (Nat.two_pow_pos _)]
+
 theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x + y / m := by
   match x with
   | 0 => simp