-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_shiftLeft {x : BitVec m} {n : Nat} (h : i < m) :
    (x <<< n)[i] = (!decide (i < n) && getLsbD x (i - n))

Proof state:
case false.false.false
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = false
h₂ : decide (n ≤ i) = false
h₃ : decide (i < n) = false
⊢ (false && (false && x.toNat.testBit (i - n))) = (!false && x.toNat.testBit (i - n))

case false.false.true
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = false
h₂ : decide (n ≤ i) = false
h₃ : decide (i < n) = true
⊢ (false && (false && x.toNat.testBit (i - n))) = (!true && x.toNat.testBit (i - n))

case false.true.false
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = false
h₂ : decide (n ≤ i) = true
h₃ : decide (i < n) = false
⊢ (false && (true && x.toNat.testBit (i - n))) = (!false && x.toNat.testBit (i - n))

case false.true.true
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = false
h₂ : decide (n ≤ i) = true
h₃ : decide (i < n) = true
⊢ (false && (true && x.toNat.testBit (i - n))) = (!true && x.toNat.testBit (i - n))

case true.false.false
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = true
h₂ : decide (n ≤ i) = false
h₃ : decide (i < n) = false
⊢ (true && (false && x.toNat.testBit (i - n))) = (!false && x.toNat.testBit (i - n))

case true.false.true
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = true
h₂ : decide (n ≤ i) = false
h₃ : decide (i < n) = true
⊢ (true && (false && x.toNat.testBit (i - n))) = (!true && x.toNat.testBit (i - n))

case true.true.false
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = true
h₂ : decide (n ≤ i) = true
h₃ : decide (i < n) = false
⊢ (true && (true && x.toNat.testBit (i - n))) = (!false && x.toNat.testBit (i - n))

case true.true.true
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = true
h₂ : decide (n ≤ i) = true
h₃ : decide (i < n) = true
⊢ (true && (true && x.toNat.testBit (i - n))) = (!true && x.toNat.testBit (i - n))

Tactic:
all_goals { simp_all <;> omega }

Result:
no goals

Proof state:
case true.true.true
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = true
h₂ : decide (n ≤ i) = true
h₃ : decide (i < n) = true
⊢ (true && (true && x.toNat.testBit (i - n))) = (!true && x.toNat.testBit (i - n))

Tactic:
simp_all <;> omega

Result:
no goals

Proof state:
m i : Nat
x : BitVec m
n : Nat
h : i < m
⊢ (decide (i < m) && (decide (n ≤ i) && x.toNat.testBit (i - n))) = (!decide (i < n) && x.toNat.testBit (i - n))

Tactic:
cases h₁ : decide (i < m) <;> cases h₂ : decide (n ≤ i) <;> cases h₃ : decide (i < n)

Result:
case false.false.false
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = false
h₂ : decide (n ≤ i) = false
h₃ : decide (i < n) = false
⊢ (false && (false && x.toNat.testBit (i - n))) = (!false && x.toNat.testBit (i - n))

case false.false.true
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = false
h₂ : decide (n ≤ i) = false
h₃ : decide (i < n) = true
⊢ (false && (false && x.toNat.testBit (i - n))) = (!true && x.toNat.testBit (i - n))

case false.true.false
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = false
h₂ : decide (n ≤ i) = true
h₃ : decide (i < n) = false
⊢ (false && (true && x.toNat.testBit (i - n))) = (!false && x.toNat.testBit (i - n))

case false.true.true
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = false
h₂ : decide (n ≤ i) = true
h₃ : decide (i < n) = true
⊢ (false && (true && x.toNat.testBit (i - n))) = (!true && x.toNat.testBit (i - n))

case true.false.false
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = true
h₂ : decide (n ≤ i) = false
h₃ : decide (i < n) = false
⊢ (true && (false && x.toNat.testBit (i - n))) = (!false && x.toNat.testBit (i - n))

case true.false.true
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = true
h₂ : decide (n ≤ i) = false
h₃ : decide (i < n) = true
⊢ (true && (false && x.toNat.testBit (i - n))) = (!true && x.toNat.testBit (i - n))

case true.true.false
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = true
h₂ : decide (n ≤ i) = true
h₃ : decide (i < n) = false
⊢ (true && (true && x.toNat.testBit (i - n))) = (!false && x.toNat.testBit (i - n))

case true.true.true
m i : Nat
x : BitVec m
n : Nat
h : i < m
h₁ : decide (i < m) = true
h₂ : decide (n ≤ i) = true
h₃ : decide (i < n) = true
⊢ (true && (true && x.toNat.testBit (i - n))) = (!true && x.toNat.testBit (i - n))

Proof state:
m i : Nat
x : BitVec m
n : Nat
h : i < m
⊢ (x <<< n)[i] = (!decide (i < n) && x.getLsbD (i - n))

Tactic:
rw [← testBit_toNat, getElem_eq_testBit_toNat]

Result:
m i : Nat
x : BitVec m
n : Nat
h : i < m
⊢ (x <<< n).toNat.testBit i = (!decide (i < n) && x.toNat.testBit (i - n))

Proof state:
m i : Nat
x : BitVec m
n : Nat
h : i < m
⊢ (x <<< n).toNat.testBit i = (!decide (i < n) && x.toNat.testBit (i - n))

Tactic:
simp only [toNat_shiftLeft, Nat.testBit_mod_two_pow, Nat.testBit_shiftLeft, ge_iff_le]

Result:
m i : Nat
x : BitVec m
n : Nat
h : i < m
⊢ (decide (i < m) && (decide (n ≤ i) && x.toNat.testBit (i - n))) = (!decide (i < n) && x.toNat.testBit (i - n))