Theorem: LeanColls.BitVec.get_set (LeanColls/Data/BitVec.lean)

State before:
n : ℕ
bv : BitVec n
i : Fin n
x : Bool
j : Fin n
⊢ (bv.set i x).get j = if i = j then x else bv.get j
Tactic:
simp [get, set]
State after:
n : ℕ
bv : BitVec n
i : Fin n
x : Bool
j : Fin n
⊢ ((Seq.get
            (if x = true then { data := sorryAx ByteArray true, hsize := ⋯ }
              else { data := sorryAx ByteArray true, hsize := ⋯ }).data
            ⟨↑j / 8, ⋯⟩).land
        (UInt8.shiftLeft 1 (↑j % 8).toUInt8) !=
      0) =
    if i = j then x else (Seq.get bv.data ⟨↑j / 8, ⋯⟩).land (UInt8.shiftLeft 1 (↑j % 8).toUInt8) != 0