case true =>
  rw [UInt.when_true_eq, UInt.getBit_shiftLeft]
  have : UInt.getBit (1 : α) (k - toNat (OfNat.ofNat (α:=α) n) % length α) = false := by
    rw [UInt.toNat_ofNat]
    have := calc
      n % 2^length α % length α
        ≤ n % 2^length α := Nat.mod_le ..
      _ ≤ n := Nat.mod_le ..
      _ < n.succ := n.lt_succ_self
      _ ≤ k := hnk
    have : k - n % 2^length α % length α > 0 :=
      Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ this)
    rw [UInt.getBit_one, decide_eq_false (Nat.ne_of_gt this), Bool.and_false]
  simp only [this, Bool.and_false]
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) k = false
no goals