Theorem: Nat.bitdivide (Algdata/Data/Nat/Bits.lean)

State before:
n k : Nat
⊢ n = (n ^^^ n &&& k) + (n &&& k)
Tactic:
have : (n ^^^ (n &&& k)) &&& (n &&& k) = 0 := by
  simp [←Nat.land_assoc n n k]
State after:
n k : Nat
this : (n ^^^ n &&& k) &&& (n &&& k) = 0
⊢ n = (n ^^^ n &&& k) + (n &&& k)

State before:
n k : Nat
this : (n ^^^ n &&& k) &&& (n &&& k) = 0
⊢ n = (n ^^^ n &&& k) + (n &&& k)
Tactic:
conv =>
  rhs; simp [add_eq_xor this, Nat.xor_assoc]
State after:
no goals

State before:
n k : Nat
⊢ (n ^^^ n &&& k) &&& (n &&& k) = 0
Tactic:
simp [←Nat.land_assoc n n k]
State after:
no goals