calc
  2*k &&& (2*l + 1)
    = 2*k &&& (2*l ^^^ 1) := by rw [‹2*l + 1 = 2*l ^^^ 1›]
  _ = (2*k &&& 2*l) ^^^ (2*k &&& 1) := Nat.and_xor ..
  _ = (2*k &&& 2*l) ^^^ 0 := by rw [‹∀ m, 2*m &&& 1 = 0›]
  _ = 2*k &&& 2 * l:= by rw [Nat.xor_zero]
n : Nat
this✝¹ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this✝ : ∀ (m : Nat), 2 * m &&& 1 = 0
this : 2 * l + 1 = 2 * l ^^^ 1
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
no goals