fix merge

FR-vdash-bot · Jan 20, 2024 · 67605c3 · 67605c3
1 parent 70bbab4
commit 67605c3
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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)) :