English
For motive, bit, n, and h, binaryRec' zero equals bit b n h (binaryRec' zero bit n).
Русский
Для motive, bit, n и h выполняется равенство binaryRec'(zero) bit (Nat.bit b n) = bit b n h (binaryRec' zero bit n).
LaTeX
$$$ binaryRec'\ (zero)\ (bit)\ (Nat.bit\ b\ n) = bit\ b\ n\ h\ (binaryRec'\ zero\ bit\ n) $$$
Lean4
theorem binaryRec_eq {zero : motive 0} {bit : ∀ b n, motive n → motive (bit b n)} (b n)
(h : bit false 0 zero = zero ∨ (n = 0 → b = true)) :
binaryRec zero bit (n.bit b) = bit b n (binaryRec zero bit n) :=
by
by_cases h' : n.bit b = 0
case pos =>
obtain ⟨rfl, rfl⟩ := bit_eq_zero_iff.mp h'
simp only [Bool.false_eq_true, imp_false, not_true_eq_false, or_false] at h
unfold binaryRec
exact h.symm
case neg =>
rw [binaryRec, dif_neg h']
change congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one ▸ bit _ _ _ = _
generalize congrArg motive (n.bit b).bit_testBit_zero_shiftRight_one = e; revert e
rw [testBit_bit_zero, bit_shiftRight_one]
intros; rfl
