fix: swap Nat.zero_or and Nat.or_zero (#4094)

Closes #4093
leanprover · May 7, 2024 · ec27b37 · ec27b37
1 parent e5b7dc8
commit ec27b37
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -402,12 +402,12 @@ theorem and_pow_two_identity {x : Nat} (lt : x < 2^n) : x &&& 2^n-1 = x := by
 
 /-! ### lor -/
 
-@[simp] theorem or_zero (x : Nat) : 0 ||| x = x := by
+@[simp] theorem zero_or (x : Nat) : 0 ||| x = x := by
   simp only [HOr.hOr, OrOp.or, lor]
   unfold bitwise
   simp [@eq_comm _ 0]
 
-@[simp] theorem zero_or (x : Nat) : x ||| 0 = x := by
+@[simp] theorem or_zero (x : Nat) : x ||| 0 = x := by
   simp only [HOr.hOr, OrOp.or, lor]
   unfold bitwise
   simp [@eq_comm _ 0]