diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 09e1c0813e..96be0f6235 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -591,10 +591,13 @@ theorem and_or_distrib_left (x y z : Nat) : x &&& (y ||| z) = (x &&& y) ||| (x &
    simp [Bool.and_or_distrib_left]
 
 @[grind =]
-theorem and_distrib_right (x y z : Nat) : (x ||| y) &&& z = (x &&& z) ||| (y &&& z) := by
+theorem and_or_distrib_right (x y z : Nat) : (x ||| y) &&& z = (x &&& z) ||| (y &&& z) := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.and_or_distrib_right]
 
+@[deprecated and_or_distrib_right (since := "2025-10-02")]
+abbrev and_distrib_right := and_or_distrib_right
+
 theorem or_and_distrib_left (x y z : Nat) : x ||| (y &&& z) = (x ||| y) &&& (x ||| z) := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.or_and_distrib_left]