-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_shiftLeft (x : BitVec w) (i) :
    (x <<< i).getMsbD k = x.getMsbD (k + i)

Proof state:
case pos
w k : Nat
x : BitVec w
i : Nat
h : w = 0
⊢ (decide (k < w) && (decide (w - 1 - k < w) && !decide (w - 1 - k < i) && x.getLsbD (w - 1 - k - i))) =
    (decide (k + i < w) && x.getLsbD (w - 1 - (k + i)))

Tactic:
subst h

Result:
case pos
k i : Nat
x : BitVec 0
⊢ (decide (k < 0) && (decide (0 - 1 - k < 0) && !decide (0 - 1 - k < i) && x.getLsbD (0 - 1 - k - i))) =
    (decide (k + i < 0) && x.getLsbD (0 - 1 - (k + i)))

Proof state:
case pos
w k : Nat
x : BitVec w
i : Nat
h : ¬w = 0
t : w - 1 - k < w
h₁ : ¬k < w
h₂ : ¬w - (1 + k) < i
h₃ : k + i < w
⊢ x.getLsbD (w - (1 + (k + i))) = false

Tactic:
apply getLsbD_ge

Result:
case pos.ge
w k : Nat
x : BitVec w
i : Nat
h : ¬w = 0
t : w - 1 - k < w
h₁ : ¬k < w
h₂ : ¬w - (1 + k) < i
h₃ : k + i < w
⊢ w ≤ w - (1 + (k + i))

Proof state:
case neg
w k : Nat
x : BitVec w
i : Nat
h : ¬w = 0
⊢ (decide (k < w) && (decide (w - 1 - k < w) && !decide (w - 1 - k < i) && x.getLsbD (w - 1 - k - i))) =
    (decide (k + i < w) && x.getLsbD (w - 1 - (k + i)))

Tactic:
have t : w - 1 - k < w := by omega

Result:
case neg
w k : Nat
x : BitVec w
i : Nat
h : ¬w = 0
t : w - 1 - k < w
⊢ (decide (k < w) && (decide (w - 1 - k < w) && !decide (w - 1 - k < i) && x.getLsbD (w - 1 - k - i))) =
    (decide (k + i < w) && x.getLsbD (w - 1 - (k + i)))

Proof state:
w k : Nat
x : BitVec w
i : Nat
h : ¬w = 0
⊢ w - 1 - k < w

Tactic:
omega

Result:
no goals

Proof state:
case neg
w k : Nat
x : BitVec w
i : Nat
h : ¬w = 0
t : w - 1 - k < w
⊢ (decide (k < w) && (decide (w - 1 - k < w) && !decide (w - 1 - k < i) && x.getLsbD (w - 1 - k - i))) =
    (decide (k + i < w) && x.getLsbD (w - 1 - (k + i)))

Tactic:
simp only [t]

Result:
case neg
w k : Nat
x : BitVec w
i : Nat
h : ¬w = 0
t : w - 1 - k < w
⊢ (decide (k < w) && (decide True && !decide (w - 1 - k < i) && x.getLsbD (w - 1 - k - i))) =
    (decide (k + i < w) && x.getLsbD (w - 1 - (k + i)))

Proof state:
w k : Nat
x : BitVec w
i : Nat
⊢ (decide (k < w) && (decide (w - 1 - k < w) && !decide (w - 1 - k < i) && x.getLsbD (w - 1 - k - i))) =
    (decide (k + i < w) && x.getLsbD (w - 1 - (k + i)))

Tactic:
by_cases h : w = 0

Result:
case pos
w k : Nat
x : BitVec w
i : Nat
h : w = 0
⊢ (decide (k < w) && (decide (w - 1 - k < w) && !decide (w - 1 - k < i) && x.getLsbD (w - 1 - k - i))) =
    (decide (k + i < w) && x.getLsbD (w - 1 - (k + i)))

case neg
w k : Nat
x : BitVec w
i : Nat
h : ¬w = 0
⊢ (decide (k < w) && (decide (w - 1 - k < w) && !decide (w - 1 - k < i) && x.getLsbD (w - 1 - k - i))) =
    (decide (k + i < w) && x.getLsbD (w - 1 - (k + i)))

Proof state:
case neg
w k : Nat
x : BitVec w
i : Nat
h : ¬w = 0
t : w - 1 - k < w
⊢ (decide (k < w) && (!decide (w - (1 + k) < i) && x.getLsbD (w - (1 + (k + i))))) =
    (decide (k + i < w) && x.getLsbD (w - (1 + (k + i))))

Tactic:
by_cases h₁ : k < w <;> by_cases h₂ : w - (1 + k) < i <;> by_cases h₃ : k + i < w
  <;> simp only [h₁, h₂, h₃, decide_false, h₂, decide_true, Bool.not_true, Bool.false_and, Bool.and_self,
    Bool.true_and, Bool.false_eq, Bool.false_and, Bool.not_false]
  <;> (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge)
  <;> omega

Result:
no goals

Proof state:
w k : Nat
x : BitVec w
i : Nat
⊢ (x <<< i).getMsbD k = x.getMsbD (k + i)

Tactic:
simp only [getMsbD, getLsbD_shiftLeft]

Result:
w k : Nat
x : BitVec w
i : Nat
⊢ (decide (k < w) && (decide (w - 1 - k < w) && !decide (w - 1 - k < i) && x.getLsbD (w - 1 - k - i))) =
    (decide (k + i < w) && x.getLsbD (w - 1 - (k + i)))

Proof state:
case pos
w k : Nat
x : BitVec w
i : Nat
h : ¬w = 0
t : w - 1 - k < w
h₁ : ¬k < w
h₂ : ¬w - (1 + k) < i
h₃ : k + i < w
⊢ x.getLsbD (w - (1 + (k + i))) = false

Tactic:
first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge

Result:
case pos.ge
w k : Nat
x : BitVec w
i : Nat
h : ¬w = 0
t : w - 1 - k < w
h₁ : ¬k < w
h₂ : ¬w - (1 + k) < i
h₃ : k + i < w
⊢ w ≤ w - (1 + (k + i))

Proof state:
case neg
w k : Nat
x : BitVec w
i : Nat
h : ¬w = 0
t : w - 1 - k < w
⊢ (decide (k < w) && (decide True && !decide (w - 1 - k < i) && x.getLsbD (w - 1 - k - i))) =
    (decide (k + i < w) && x.getLsbD (w - 1 - (k + i)))

Tactic:
simp only [decide_true, Nat.sub_sub, Bool.true_and, Nat.add_assoc]

Result:
case neg
w k : Nat
x : BitVec w
i : Nat
h : ¬w = 0
t : w - 1 - k < w
⊢ (decide (k < w) && (!decide (w - (1 + k) < i) && x.getLsbD (w - (1 + (k + i))))) =
    (decide (k + i < w) && x.getLsbD (w - (1 + (k + i))))

Proof state:
case pos
k i : Nat
x : BitVec 0
⊢ (decide (k < 0) && (decide (0 - 1 - k < 0) && !decide (0 - 1 - k < i) && x.getLsbD (0 - 1 - k - i))) =
    (decide (k + i < 0) && x.getLsbD (0 - 1 - (k + i)))

Tactic:
simp

Result:
no goals