Theorem: Nat.or_and_distrib_right (Extra/Nat/Bitwise.lean)

State before:
x y z : Nat
⊢ x &&& y ||| z = (x ||| z) &&& (y ||| z)
Tactic:
induction z using Nat.recBit generalizing x y <;>
  cases y using Nat.casesBitOn <;> cases x using Nat.casesBitOn <;> simp [*]
State after:
no goals