English
For any motive, and any h with h(b,n) = motive(bit b n), bitCasesOn (bit b n) h = h b n.
Русский
Для любого motive и любого h с h(b,n) = motive(bit b n) выполняется равенство bitCasesOn (bit b n) h = h b n.
LaTeX
$$$\forall {motive : Nat \to Sort u}\, (h : \forall b : Bool, \forall n : \mathbb{N}, motive (bit b n))\, (b : Bool)\, (n : \mathbb{N}),\; bitCasesOn (bit b n) h = h b n$$$
Lean4
@[simp]
theorem bitCasesOn_bit (h : ∀ b n, motive (bit b n)) (b : Bool) (n : Nat) : bitCasesOn (bit b n) h = h b n :=
by
change congrArg motive (bit b n).bit_testBit_zero_shiftRight_one ▸ h _ _ = h b n
generalize congrArg motive (bit b n).bit_testBit_zero_shiftRight_one = e; revert e
rw [testBit_bit_zero, bit_shiftRight_one]
intros; rfl
