conv =>
  lhs; simp only [UInt.getBit_xor, bitmask.aux]; rw [h_ind (Nat.le_of_succ_le hk)]
  unfold UInt.getBit
  simp only [toNat_shiftLeft, toNat_land, toNat_shiftRight, toNat_ofNat k, toNat_ofNat 1]
  rw [Nat.mod_eq_of_lt hn, Nat.mod_eq_of_lt ‹k < 2^length α›, Nat.mod_eq_of_lt hk, Nat.mod_eq_of_lt ‹1<2^length α›]
  tactic =>
    have : (k >>> toNat n &&& 1) <<< k < 2^length α :=
      calc (k >>> toNat n &&& 1) <<< k
        _ = (k >>> toNat n &&& 1) * 2^k := Nat.shiftLeft_eq _ k
        _ ≤ 1*2^k := Nat.mul_le_mul_right _ $ by rw [Nat.land_one]; exact Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ 1))
        _ = 2^k := Nat.one_mul _
        _ < 2^length α := Nat.pow_lt_pow_right Nat.le.refl hk
  rw [Nat.mod_eq_of_lt this]
  rhs; rw [Nat.shiftLeft_getBit, Nat.land_getBit, Nat.shiftRight_getBit]
  change decide (i ≥ k) && (k.getBit (i-k+toNat n) && Nat.getBit (2^0) (i-k))
  rw [Nat.getBit_two_pow, ←and_decideEq (λ x => Nat.getBit k (x + toNat n))]
  tactic =>
    have : 0 = i-k ↔ i ≤ k :=
      ⟨Nat.le_of_sub_eq_zero ∘ Eq.symm, Eq.symm ∘ Nat.sub_eq_zero_of_le⟩
    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⟩⟩
  rw [decide_eq_decide.mpr ‹0=i-k ↔ i≤k›, Bool.and_comm _ (decide _), ←Bool.and_assoc]
  rw [decide_and_decide, decide_eq_decide.mpr ‹(i≥k ∧ i≤k) ↔ i=k›]
  rw [Nat.zero_add, ←decideEq_and (f:=λ x => Nat.getBit x (toNat n))]
α : 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 α
⊢ UInt.getBit (bitmask.aux n (Nat.succ k)) i = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
α : 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 α
⊢ ((decide (i < k) && Nat.getBit i (toNat n)) != (decide (i = k) && Nat.getBit i (toNat n))) =
    (decide (i < Nat.succ k) && Nat.getBit i (toNat n))