From ad03c355bf24f19ce9fc2f2ea5997bc307dabe07 Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Tue, 22 Oct 2024 16:38:36 +0800
Subject: [PATCH 1/2] chore: deprecate `Nat.binaryRec_eq`, rename
 `Nat.binaryRec_eq'` => `Nat.binaryRec_eq`

---
 Mathlib/Data/Nat/BinaryRec.lean  | 13 +++----------
 Mathlib/Data/Nat/BitIndices.lean |  4 ++--
 Mathlib/Data/Nat/Bits.lean       |  2 +-
 Mathlib/Data/Nat/Bitwise.lean    |  2 +-
 Mathlib/Data/Nat/EvenOddRec.lean |  4 ++--
 Mathlib/Data/Num/Lemmas.lean     |  2 +-
 6 files changed, 10 insertions(+), 17 deletions(-)

diff --git a/Mathlib/Data/Nat/BinaryRec.lean b/Mathlib/Data/Nat/BinaryRec.lean
index 0edc733fa68b0..a3d3e6f8e1fc1 100644
--- a/Mathlib/Data/Nat/BinaryRec.lean
+++ b/Mathlib/Data/Nat/BinaryRec.lean
@@ -3,6 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Praneeth Kolichala, Yuyang Zhao
 -/
+import Batteries.Tactic.Alias
 
 /-!
 # Binary recursion on `Nat`
@@ -127,12 +128,7 @@ theorem binaryRec_one {motive : Nat → Sort u} (z : motive 0) (f : ∀ b n, mot
   simp only [add_one_ne_zero, ↓reduceDIte, Nat.reduceShiftRight, binaryRec_zero]
   rfl
 
-/--
-The same as `binaryRec_eq`,
-but that one unfortunately requires `f` to be the identity when appending `false` to `0`.
-Here, we allow you to explicitly say that that case is not happening,
-i.e. supplying `n = 0 → b = true`. -/
-theorem binaryRec_eq' {motive : Nat → Sort u} {z : motive 0}
+theorem binaryRec_eq {motive : Nat → Sort u} {z : motive 0}
     {f : ∀ b n, motive n → motive (bit b n)} (b n)
     (h : f false 0 z = z ∨ (n = 0 → b = true)) :
     binaryRec z f (bit b n) = f b n (binaryRec z f n) := by
@@ -149,9 +145,6 @@ theorem binaryRec_eq' {motive : Nat → Sort u} {z : motive 0}
     rw [testBit_bit_zero, bit_shiftRight_one]
     intros; rfl
 
-theorem binaryRec_eq {motive : Nat → Sort u} {z : motive 0} {f : ∀ b n, motive n → motive (bit b n)}
-    (h : f false 0 z = z) (b n) :
-    binaryRec z f (bit b n) = f b n (binaryRec z f n) :=
-  binaryRec_eq' b n (.inl h)
+@[deprecated (since := "2024-10-21")] alias binaryRec_eq' := binaryRec_eq
 
 end Nat
diff --git a/Mathlib/Data/Nat/BitIndices.lean b/Mathlib/Data/Nat/BitIndices.lean
index bd77462f10032..9d9c7c094edad 100644
--- a/Mathlib/Data/Nat/BitIndices.lean
+++ b/Mathlib/Data/Nat/BitIndices.lean
@@ -41,11 +41,11 @@ def bitIndices (n : ℕ) : List ℕ :=
 
 theorem bitIndices_bit_true (n : ℕ) :
     bitIndices (bit true n) = 0 :: ((bitIndices n).map (· + 1)) :=
-  binaryRec_eq rfl _ _
+  binaryRec_eq _ _ (.inl rfl)
 
 theorem bitIndices_bit_false (n : ℕ) :
     bitIndices (bit false n) = (bitIndices n).map (· + 1) :=
-  binaryRec_eq rfl _ _
+  binaryRec_eq _ _ (.inl rfl)
 
 @[simp] theorem bitIndices_two_mul_add_one (n : ℕ) :
     bitIndices (2 * n + 1) = 0 :: (bitIndices n).map (· + 1) := by
diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index bdcc8d87a6a7c..7079602da88d9 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -264,7 +264,7 @@ theorem zero_bits : bits 0 = [] := by simp [Nat.bits]
 @[simp]
 theorem bits_append_bit (n : ℕ) (b : Bool) (hn : n = 0 → b = true) :
     (bit b n).bits = b :: n.bits := by
-  rw [Nat.bits, Nat.bits, binaryRec_eq']
+  rw [Nat.bits, Nat.bits, binaryRec_eq]
   simpa
 
 @[simp]
diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index 3c394416fac8e..70965de4413df 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -71,7 +71,7 @@ theorem binaryRec_of_ne_zero {C : Nat → Sort*} (z : C 0) (f : ∀ b n, C n →
     binaryRec z f n = bit_decomp n ▸ f (bodd n) (div2 n) (binaryRec z f (div2 n)) := by
   cases n using bitCasesOn with
   | h b n =>
-    rw [binaryRec_eq' _ _ (by right; simpa [bit_eq_zero_iff] using h)]
+    rw [binaryRec_eq _ _ (by right; simpa [bit_eq_zero_iff] using h)]
     generalize_proofs h; revert h
     rw [bodd_bit, div2_bit]
     simp
diff --git a/Mathlib/Data/Nat/EvenOddRec.lean b/Mathlib/Data/Nat/EvenOddRec.lean
index ce6c89abcd14f..679a7ff57f097 100644
--- a/Mathlib/Data/Nat/EvenOddRec.lean
+++ b/Mathlib/Data/Nat/EvenOddRec.lean
@@ -30,14 +30,14 @@ theorem evenOddRec_zero {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i →
 theorem evenOddRec_even {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
     (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) (n : ℕ) :
     (2 * n).evenOddRec h0 h_even h_odd = h_even n (evenOddRec h0 h_even h_odd n) := by
-  apply binaryRec_eq' false n
+  apply binaryRec_eq false n
   simp [H]
 
 @[simp]
 theorem evenOddRec_odd {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
     (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) (n : ℕ) :
     (2 * n + 1).evenOddRec h0 h_even h_odd = h_odd n (evenOddRec h0 h_even h_odd n) := by
-  apply binaryRec_eq' true n
+  apply binaryRec_eq true n
   simp [H]
 
 /-- Strong recursion principle on even and odd numbers: if for all `i : ℕ` we can prove `P (2 * i)`
diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index 2808a6ef83358..97c085e5068b4 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -201,7 +201,7 @@ theorem bit1_of_bit1 : ∀ n : Num, (n + n) + 1 = n.bit1
 theorem ofNat'_zero : Num.ofNat' 0 = 0 := by simp [Num.ofNat']
 
 theorem ofNat'_bit (b n) : ofNat' (Nat.bit b n) = cond b Num.bit1 Num.bit0 (ofNat' n) :=
-  Nat.binaryRec_eq rfl _ _
+  Nat.binaryRec_eq _ _ (.inl rfl)
 
 @[simp]
 theorem ofNat'_one : Num.ofNat' 1 = 1 := by erw [ofNat'_bit true 0, cond, ofNat'_zero]; rfl

From 9c1c52514f5deaefd666251e96211c62fbf2f406 Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Tue, 22 Oct 2024 17:19:44 +0800
Subject: [PATCH 2/2] fix

---
 Mathlib/Data/Num/Lemmas.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean
index 97c085e5068b4..1ee383be417b7 100644
--- a/Mathlib/Data/Num/Lemmas.lean
+++ b/Mathlib/Data/Num/Lemmas.lean
@@ -661,12 +661,11 @@ theorem natSize_to_nat (n) : natSize n = Nat.size n := by rw [← size_eq_natSiz
 theorem ofNat'_eq : ∀ n, Num.ofNat' n = n :=
   Nat.binaryRec (by simp) fun b n IH => by
     rw [ofNat'] at IH ⊢
-    rw [Nat.binaryRec_eq, IH]
+    rw [Nat.binaryRec_eq _ _ (.inl rfl), IH]
     -- Porting note: `Nat.cast_bit0` & `Nat.cast_bit1` are not `simp` theorems anymore.
-    · cases b <;> simp only [cond_false, cond_true, Nat.bit, two_mul, Nat.cast_add, Nat.cast_one]
-      · rw [bit0_of_bit0]
-      · rw [bit1_of_bit1]
-    · rfl
+    cases b <;> simp only [cond_false, cond_true, Nat.bit, two_mul, Nat.cast_add, Nat.cast_one]
+    · rw [bit0_of_bit0]
+    · rw [bit1_of_bit1]
 
 theorem zneg_toZNum (n : Num) : -n.toZNum = n.toZNumNeg := by cases n <;> rfl