English
The bitwise AND operation equals the standard logical AND on bits: bitwise and = land.
Русский
Побитовое AND равно стандартному логическому AND на битах: bitwise and = land.
LaTeX
$$$$ \operatorname{bitwise} \text{ and } = \operatorname{land}. $$$$
Lean4
theorem bitwise_and : bitwise and = land := by
funext m n
rcases m with m | m <;> rcases n with n | n <;>
try { rfl
} <;>
simp only [bitwise, natBitwise, Bool.not_false, cond_false, cond_true, Bool.and_true, Bool.and_false]
· rw [Nat.bitwise_swap, Function.swap]
congr
funext x y
cases x <;> cases y <;> rfl
· congr
simp
-- Porting note: Was `bitwise_tac` in mathlib
