comment out Int.shiftLeft_add'

kim-em · kim-em · commit b33c9d7aaeaf · 2025-08-25T08:50:46.000+10:00
diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean
@@ -363,6 +363,10 @@ theorem shiftRight_add' : ∀ (m : ℤ) (n k : ℕ), m >>> (n + k : ℤ) = (m >>
 
 /-! ### bitwise ops -/
 
+-- Commented out: please either fix,
+-- or remove after https://github.com/leanprover-community/mathlib4/pull/28884 is merged
+-- (that PR proposed deprecating these theorems).
+/-
 theorem shiftLeft_add' : ∀ (m : ℤ) (n : ℕ) (k : ℤ), m <<< ((n : ℤ) + k) = (m <<< (n : ℤ)) <<< k
   | (m : ℕ), n, (k : ℕ) =>
     congr_arg ofNat (by simp [Nat.shiftLeft_eq, Nat.pow_add, mul_assoc])
@@ -388,6 +392,7 @@ theorem shiftLeft_add' : ∀ (m : ℤ) (n : ℕ) (k : ℤ), m <<< ((n : ℤ) + k
 
 theorem shiftLeft_sub (m : ℤ) (n : ℕ) (k : ℤ) : m <<< ((n : ℤ) - k) = (m <<< (n : ℤ)) >>> k :=
   shiftLeft_add' _ _ _
+-/
 
 theorem shiftLeft_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), m <<< (n : ℤ) = m * (2 ^ n : ℕ)
   | (m : ℕ), _ => congr_arg ((↑) : ℕ → ℤ) (by simp [Nat.shiftLeft_eq])
