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