English
The bitwise XOR operation coincides with the integer XOR: bitwise xor = Int.xor.
Русский
Побитовая операция XOR совпадает с целочисленным XOR: bitwise xor = Int.xor.
LaTeX
$$$$ \operatorname{bitwise} \text{ xor } = \operatorname{Int}.xor. $$$$
Lean4
theorem bitwise_xor : bitwise xor = Int.xor := by
funext m n
rcases m with m | m <;> rcases n with n | n <;>
try { rfl
} <;>
simp only [bitwise, natBitwise, Bool.not_false, Bool.bne_eq_xor, cond_false, cond_true, negSucc.injEq,
Bool.false_xor, Bool.true_xor, Bool.not_true, Int.xor, HXor.hXor, XorOp.xor, Nat.xor] <;>
simp