suffices ∀ n, 2*n.lsb = (2*n).lsb by
  intro n k
  induction k generalizing n
  case zero => rfl
  case succ k h_ind =>
    simp only [Nat.succ_eq_add_one, ←Nat.shiftLeft_shiftLeft, h_ind]
    conv => change 2*(n <<< k).lsb = (2* (n <<< k)).lsb
    rw [this]
⊢ ∀ (n k : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
⊢ ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)