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

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