cases this with | intro i hi =>
suffices ∀ j, UInt.getBit (UInt.lsb a) j = decide (i = j) from ⟨i, this⟩
intro j
if hij : i = j
then exact Eq.trans (hij ▸ hi) (decide_eq_true hij).symm
else
  suffices UInt.getBit (UInt.lsb a) j ≠ true
    by rw [decide_eq_false hij]; exact eq_false_of_ne_true this
  intro hcontra
  cases Nat.lt_or_ge i j
  . have : i < j := ‹_›
    have : UInt.getBit a i = false :=
      ((UInt.getBit_lsb_iff a).mp hcontra).right i this
    have : UInt.getBit a i = true :=
      ((UInt.getBit_lsb_iff a).mp hi).left
    cases Eq.trans ‹UInt.getBit a i = false›.symm ‹UInt.getBit a i = true›
  . have : i > j := Nat.lt_of_le_of_ne ‹i ≥ j› (hij ∘ Eq.symm)
    have : UInt.getBit a j = false :=
      And.right ((UInt.getBit_lsb_iff a).mp hi) j this
    have : UInt.getBit a j = true :=
      ((UInt.getBit_lsb_iff a).mp hcontra).left
    cases Eq.trans ‹UInt.getBit a j = false›.symm ‹UInt.getBit a j = true›
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
ha : a ≠ 0
this : ∃ i, UInt.getBit (UInt.lsb a) i = true
⊢ ∃ i, ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i = j)
no goals