From 7a0fe6f54c1bcecfca0be87aacb032ac45c6b984 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Tue, 2 Jul 2024 03:55:12 +0200
Subject: [PATCH] feat: Nat.and_le_(left|right) (#4597)

Split from #4583
---
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index d46132bee9..5350f40e34 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -504,3 +504,27 @@ theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^
 
 @[simp] theorem testBit_shiftRight (x : Nat) : testBit (x >>> i) j = testBit x (i+j) := by
   simp [testBit, ←shiftRight_add]
+
+/-! ### le -/
+
+theorem le_of_testBit {n m : Nat} (h : ∀ i, n.testBit i = true → m.testBit i = true) : n ≤ m := by
+  induction n using div2Induction generalizing m
+  next n ih =>
+  have : n / 2 ≤ m / 2 := by
+    rcases n with (_|n)
+    · simp
+    · exact ih (Nat.succ_pos _) fun i => by simpa using h (i + 1)
+  rw [← div_add_mod n 2, ← div_add_mod m 2]
+  cases hn : n.testBit 0
+  · have hn2 : n % 2 = 0 := by simp at hn; omega
+    rw [hn2]
+    omega
+  · have hn2 : n % 2 = 1 := by simpa using hn
+    have hm2 : m % 2 = 1 := by simpa using h _ hn
+    omega
+
+theorem and_le_left {n m : Nat} : n &&& m ≤ n :=
+  le_of_testBit (by simpa using fun i x _ => x)
+
+theorem and_le_right {n m : Nat} : n &&& m ≤ m :=
+  le_of_testBit (by simp)