case succ n =>
  unfold Nat.lsb
  have : 2 * n.succ - 1 = 2 * (n.succ - 1) + 1 := by
    simp only [Nat.mul_succ, Nat.succ_sub_one]
  have : ∀ (k l : Nat), (2*k) &&& (2*l + 1) = 2*k &&& 2*l := by
    intro k l
    have : ∀ m, 2*m &&& 1 = 0 := by intros; rw [Nat.land_one, Nat.mul_mod_right]
    have : 2*l + 1 = 2*l ^^^ 1 := Nat.add_eq_xor (this l)
    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]
  rw [‹2*n.succ - 1 = 2 * (n.succ - 1) + 1›, this]
  conv =>
    rhs; simp only [←Nat.shiftLeft_one]
    simp only [←Nat.land_shiftLeft, ←Nat.xor_shiftLeft]
n : Nat
⊢ 2 * Nat.lsb (succ n) = Nat.lsb (2 * succ n)
no goals