Fix

tobiasgrosser · tobiasgrosser · commit 6e5f8fc08ac0 · 2024-09-07T06:23:26.000+01:00
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
@@ -725,7 +725,8 @@ protected theorem two_pow_pred_lt_two_pow {w : Nat} (h : 0 < w) :
 @[simp]
 protected theorem two_pow_pred_add_two_pow_pred (h : 0 < w) :
     2 ^ (w - 1) + 2 ^ (w - 1) = 2 ^ w := by
-  rw [← Nat.pow_pred_mul h, Nat.mul_comm, Nat.two_mul]
+  rw [← Nat.pow_pred_mul h]
+  omega
 
 @[simp]
 protected theorem two_pow_sub_two_pow_pred (h : 0 < w) :
