From 67605c3ceb27d8aa2f1631ffeca91ad47869d7de Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Sun, 21 Jan 2024 02:07:47 +0800
Subject: [PATCH] fix merge

---
 Std/Data/Nat/Bitwise.lean | 2 +-
 Std/Data/Nat/Lemmas.lean  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Std/Data/Nat/Bitwise.lean b/Std/Data/Nat/Bitwise.lean
index 253a8b42c0..927e7df137 100644
--- a/Std/Data/Nat/Bitwise.lean
+++ b/Std/Data/Nat/Bitwise.lean
@@ -85,7 +85,7 @@ theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i
 theorem ne_implies_bit_diff {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i ≠ testBit y i := by
   induction y using binaryRec' generalizing x with
   | z =>
-    simp only [zero_testBit, ← Bool.eq_true_iff]
+    simp only [zero_testBit, Bool.ne_false_iff]
     exact ne_zero_implies_bit_true p
   | f yb y h hyp =>
     rw [← x.bit_decomp] at *
diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index 073435d634..60485a6538 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -1470,7 +1470,7 @@ theorem binaryRec_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (b
 theorem binaryRec_of_ne_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) {n}
     (h : n ≠ 0) :
     binaryRec z f n = bit_decomp n ▸ f n.bodd n.div2 (binaryRec z f n.div2) := by
-  rw [binaryRec, dif_neg h, Eq.rec_eq_cast, Eq.rec_eq_cast]
+  rw [binaryRec, dif_neg h, eqRec_eq_cast, eqRec_eq_cast]
 
 theorem binaryRec_eq {C : Nat → Sort u} {z : C 0} {f : ∀ b n, C n → C (bit b n)} (b n)
     (h : f false 0 z = z ∨ (n = 0 → b = true)) :