if ha : a = 0
then intros; rw [ha, UInt.getBit_zero]
else
  have : ∃ i₀, ∀ j, UInt.getBit (UInt.lsb a) j = decide (i₀=j) := UInt.lsb_singleton a ha
  cases this with | intro i₀ hi₀ =>
  have : UInt.getBit (UInt.lsb a) i₀ = true := decide_eq_true (Eq.refl i₀) ▸ (hi₀ i₀)
  have ⟨_, (halow: ∀ j, j < i₀ → UInt.getBit a j = false)⟩ :=
    (UInt.getBit_lsb_iff a).mp this
  suffices UInt.toNat (UInt.ctz a) = i₀ by
    rw [this]; intro hi; exact halow _ hi
  have : decide (i₀ = toNat (UInt.ctz a)) = true :=
    hi₀ _ ▸ UInt.getBit_lsb_ctz a ha
  apply Eq.symm; exact of_decide_eq_true this
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
no goals