-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if i = n then b else getLsbD x i

Proof state:
case inr.inl
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
i_eq_n : i = n
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Tactic:
simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
Bool.true_and, testBit_toNat, getLsbD_ge, Bool.or_false, ↓reduceIte]

Result:
case inr.inl
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
i_eq_n : i = n
⊢ decide (b.toNat % 2 = 1) = b

Proof state:
case inr.inr
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
n_lt_i : n < i
p1 : i ≠ n
p2 : i - n ≠ 0
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Tactic:
simp [p1, p2, Nat.testBit_bool_to_nat]

Result:
no goals

Proof state:
case inl
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
i_lt_n : i < n
p1 : ¬n ≤ i
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Tactic:
have p2 : i ≠ n := by omega

Result:
case inl
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
i_lt_n : i < n
p1 : ¬n ≤ i
p2 : i ≠ n
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Proof state:
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
⊢ (cons b x)[i] = if i = n then b else x.getLsbD i

Tactic:
simp only [getElem_eq_testBit_toNat, toNat_cons, Nat.testBit_or, getLsbD]

Result:
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
⊢ ((b.toNat <<< n).testBit i || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Proof state:
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
n_lt_i : n < i
p1 : i ≠ n
⊢ i - n ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
case inl
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
i_lt_n : i < n
p1 : ¬n ≤ i
p2 : i ≠ n
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Tactic:
simp [p1, p2]

Result:
no goals

Proof state:
case inl
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
i_lt_n : i < n
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Tactic:
have p1 : ¬(n ≤ i) := by omega

Result:
case inl
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
i_lt_n : i < n
p1 : ¬n ≤ i
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Proof state:
case inr.inr
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
n_lt_i : n < i
p1 : i ≠ n
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Tactic:
have p2 : i - n ≠ 0 := by omega

Result:
case inr.inr
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
n_lt_i : n < i
p1 : i ≠ n
p2 : i - n ≠ 0
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Proof state:
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Tactic:
rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i

Result:
case inl
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
i_lt_n : i < n
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

case inr.inl
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
i_eq_n : i = n
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

case inr.inr
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
n_lt_i : n < i
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Proof state:
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
i_lt_n : i < n
p1 : ¬n ≤ i
⊢ i ≠ n

Tactic:
omega

Result:
no goals

Proof state:
case inr.inl
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
i_eq_n : i = n
⊢ decide (b.toNat % 2 = 1) = b

Tactic:
cases b <;> trivial

Result:
no goals

Proof state:
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
n_lt_i : n < i
⊢ i ≠ n

Tactic:
omega

Result:
no goals

Proof state:
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
i_lt_n : i < n
⊢ ¬n ≤ i

Tactic:
omega

Result:
no goals

Proof state:
case inr.inr
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
n_lt_i : n < i
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Tactic:
have p1 : i ≠ n := by omega

Result:
case inr.inr
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
n_lt_i : n < i
p1 : i ≠ n
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Proof state:
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
⊢ ((b.toNat <<< n).testBit i || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Tactic:
rw [Nat.testBit_shiftLeft]

Result:
b : Bool
n : Nat
x : BitVec n
i : Nat
h : i < n + 1
⊢ (decide (i ≥ n) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i