case one =>
  conv => lhs; rw [Nat.lsb_of_odd (n:=1) (by decide)]
  constructor
  show getBit 1 i = true → getBit 1 i = true ∧ ∀ j, j < i → getBit 1 j = false
  . intro h; apply And.intro h
    have : i = 0 := by
      conv at h => lhs; change getBit (2^0) i; rw [Nat.getBit_two_pow]
      exact Eq.symm (of_decide_eq_true h)
    cases this
    intro _ hj; cases hj
  show getBit 1 i = true ∧ (∀ j, j < i → getBit 1 j = false) → getBit 1 i
  . exact And.left
i : Nat
⊢ getBit (Nat.lsb 1) i = true ↔ getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false
no goals