From 76e2b9e36bc93474f7119461378c6e482a196a5a Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sun, 20 Oct 2024 22:59:50 +0200
Subject: [PATCH] Update Bitwise.lean

---
 Mathlib/Data/Nat/Bitwise.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index 268c51f5ebc80..3c394416fac8e 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -366,8 +366,7 @@ theorem xor_mod_two_eq {m n : ℕ} : (m ^^^ n) % 2 = (m + n) % 2 := by
 @[simp]
 theorem even_xor {m n : ℕ} : Even (m ^^^ n) ↔ (Even m ↔ Even n) := by
   simp only [even_iff, xor_mod_two_eq]
-  simp only [← even_iff]
-  exact even_add
+  omega
 
 @[simp] theorem bit_lt_two_pow_succ_iff {b x n} : bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n := by
   cases b <;> simp <;> omega