-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
    getLsbD (cons b x) i = if i = n then b else getLsbD x i

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

Tactic:
omega

Result:
no goals

Proof state:
case inl
b : Bool
n : Nat
x : BitVec n
i : Nat
i_lt_n : i < n
p1 : ¬n ≤ i
p2 : i ≠ n
⊢ (decide (n ≤ i) && 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 inr.inr
b : Bool
n : Nat
x : BitVec n
i : Nat
n_lt_i : n < i
p1 : i ≠ n
⊢ (decide (n ≤ i) && 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
n_lt_i : n < i
p1 : i ≠ n
p2 : i - n ≠ 0
⊢ (decide (n ≤ i) && 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
n_lt_i : n < i
p1 : i ≠ n
⊢ i - n ≠ 0

Tactic:
omega

Result:
no goals

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

Tactic:
omega

Result:
no goals

Proof state:
b : Bool
n : Nat
x : BitVec n
i : Nat
⊢ (cons b x).getLsbD i = if i = n then b else x.getLsbD i

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

Result:
b : Bool
n : Nat
x : BitVec n
i : Nat
⊢ (decide (n ≤ i) && 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
i_lt_n : i < n
⊢ ¬n ≤ i

Tactic:
omega

Result:
no goals

Proof state:
case inl
b : Bool
n : Nat
x : BitVec n
i : Nat
i_lt_n : i < n
⊢ (decide (n ≤ i) && 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
i_lt_n : i < n
p1 : ¬n ≤ i
⊢ (decide (n ≤ i) && 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
⊢ (decide (n ≤ i) && 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
i_lt_n : i < n
⊢ (decide (n ≤ i) && 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
i_eq_n : i = n
⊢ (decide (n ≤ i) && 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
n_lt_i : n < i
⊢ (decide (n ≤ i) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

Proof state:
case inl
b : Bool
n : Nat
x : BitVec n
i : Nat
i_lt_n : i < n
p1 : ¬n ≤ i
⊢ (decide (n ≤ i) && 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
i_lt_n : i < n
p1 : ¬n ≤ i
p2 : i ≠ n
⊢ (decide (n ≤ i) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i

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

Tactic:
cases b <;> trivial

Result:
no goals

Proof state:
case inr.inr
b : Bool
n : Nat
x : BitVec n
i : Nat
n_lt_i : n < i
p1 : i ≠ n
p2 : i - n ≠ 0
⊢ (decide (n ≤ i) && 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 inr.inl
b : Bool
n : Nat
x : BitVec n
i : Nat
i_eq_n : i = n
⊢ (decide (n ≤ i) && 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
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
n_lt_i : n < i
⊢ (decide (n ≤ i) && 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
n_lt_i : n < i
p1 : i ≠ n
⊢ (decide (n ≤ i) && b.toNat.testBit (i - n) || x.toNat.testBit i) = if i = n then b else x.toNat.testBit i