split to #18039

Mathlib/Data/Nat/BinaryRec.lean

@@ -128,7 +128,12 @@ 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
 
-theorem binaryRec_eq {motive : Nat → Sort u} {z : motive 0}
+/--
+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}
     {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
@@ -145,6 +150,9 @@ theorem binaryRec_eq {motive : Nat → Sort u} {z : motive 0}
     rw [testBit_bit_zero, bit_shiftRight_one]
     intros; rfl
 
-@[deprecated (since := "2024-10-21")] alias binaryRec_eq' := Nat.binaryRec_eq
+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)
 
 end Nat

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 _ _ (.inl rfl)
+  binaryRec_eq rfl _ _
 
 theorem bitIndices_bit_false (n : ℕ) :
     bitIndices (bit false n) = (bitIndices n).map (· + 1) :=
-  binaryRec_eq _ _ (.inl rfl)
+  binaryRec_eq rfl _ _
 
 @[simp] theorem bitIndices_two_mul_add_one (n : ℕ) :
     bitIndices (2 * n + 1) = 0 :: (bitIndices n).map (· + 1) := by

Mathlib/Data/Nat/Bits.lean

@@ -230,7 +230,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]

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)`

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 _ _ (.inl rfl)
+  Nat.binaryRec_eq rfl _ _
 
 @[simp]
 theorem ofNat'_one : Num.ofNat' 1 = 1 := by erw [ofNat'_bit true 0, cond, ofNat'_zero]; rfl