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
ha : ¬a = 0
this : ∃ i₀, ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
no goals