case inl heven =>
  rw [
    Nat.lsb_of_even heven,
    Nat.shiftLeft_getBit,
    decide_eq_false (p:=0≥1) (by decide),
    Bool.false_and,
  ]
  conv => rhs; dsimp [getBit]; rw [heven]; reduce
n : Nat
heven : n % 2 = 0
⊢ getBit (Nat.lsb n) 0 = getBit n 0
no goals