have : (i ≥ k ∧ i ≤ k) ↔ i = k :=
  ⟨λ h => Nat.le_antisymm h.right h.left, λ h => by cases h; exact ⟨Nat.le.refl, Nat.le.refl⟩⟩
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝³ : k < 2 ^ length α
this✝² : 2 ^ toNat n < 2 ^ length α
this✝¹ : 1 < 2 ^ length α
this✝ : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
this : 0 = i - k ↔ i ≤ k
⊢ (decide (i ≥ k) && (Nat.getBit k (0 + toNat n) && decide (0 = i - k))) = ?m.39484
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝⁴ : k < 2 ^ length α
this✝³ : 2 ^ toNat n < 2 ^ length α
this✝² : 1 < 2 ^ length α
this✝¹ : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
this✝ : 0 = i - k ↔ i ≤ k
this : i ≥ k ∧ i ≤ k ↔ i = k
⊢ (decide (i ≥ k) && (Nat.getBit k (0 + toNat n) && decide (0 = i - k))) = ?m.39484