-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_shiftLeft (x : BitVec m) (n) :
    getLsbD (x <<< n) i = (decide (i < m) && !decide (i < n) && getLsbD x (i - n))

Proof state:
m i : Nat
x : BitVec m
n : Nat
⊢ (decide (i < m) && (decide (n ≤ i) && x.toNat.testBit (i - n))) =
    (decide (i < m) && !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₁ : decide (i < m) = false
h₂ : decide (n ≤ i) = false
h₃ : decide (i < n) = false
⊢ (false && (false && x.toNat.testBit (i - n))) = (false && !false && x.toNat.testBit (i - n))

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

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

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

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

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

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

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

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

Tactic:
rw [← testBit_toNat, getLsbD]

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

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

Tactic:
simp_all <;> omega

Result:
no goals

Proof state:
m i : Nat
x : BitVec m
n : Nat
⊢ (x <<< n).toNat.testBit i = (decide (i < m) && !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
⊢ (decide (i < m) && (decide (n ≤ i) && x.toNat.testBit (i - n))) =
    (decide (i < m) && !decide (i < n) && x.toNat.testBit (i - n))

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

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

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

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

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

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

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

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

Tactic:
all_goals { simp_all <;> omega }

Result:
no goals