-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} :
    (x >>> n).getMsbD i = (decide (i < w) && (!decide (i < n) && x.getMsbD (i - n)))

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

Tactic:
simp [getLsbD_ge, show w ≤ (n + (w - 1 - i)) by omega]

Result:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < n
⊢ i < w → n ≤ i → i - n < w → x.getLsbD (w - 1 - (i - n)) = false

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

Tactic:
simp only [h, decide_false, Bool.not_false, show i - n < w by omega, decide_true,
  Bool.true_and]

Result:
case pos
w : Nat
x : BitVec w
i n : Nat
h : ¬i < n
h₁ : i < w
⊢ (decide (i < w) && x.getLsbD (n + (w - 1 - i))) = (decide (i < w) && x.getLsbD (w - 1 - (i - n)))

Proof state:
w : Nat
x : BitVec w
i n : Nat
h : ¬i < n
h₁ : i < w
⊢ i - n < w

Tactic:
omega

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < n
⊢ i < w → n ≤ i → i - n < w → x.getLsbD (w - 1 - (i - n)) = false

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i n : Nat
⊢ (x >>> n).getMsbD i = (decide (i < w) && (!decide (i < n) && x.getMsbD (i - n)))

Tactic:
simp only [getMsbD, getLsbD_ushiftRight]

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

Proof state:
w : Nat
x : BitVec w
i n : Nat
h : i < n
⊢ w ≤ n + (w - 1 - i)

Tactic:
omega

Result:
no goals

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

Tactic:
by_cases h : i < n

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

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

Proof state:
case pos
w : Nat
x : BitVec w
i n : Nat
h : ¬i < n
h₁ : i < w
⊢ (decide (i < w) && x.getLsbD (n + (w - 1 - i))) = (decide (i < w) && x.getLsbD (w - 1 - (i - n)))

Tactic:
congr

Result:
case pos.e_y.e_i
w : Nat
x : BitVec w
i n : Nat
h : ¬i < n
h₁ : i < w
⊢ n + (w - 1 - i) = w - 1 - (i - n)

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

Tactic:
by_cases h₁ : i < w

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

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

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

Tactic:
simp [h, h₁]

Result:
no goals

Proof state:
case pos.e_y.e_i
w : Nat
x : BitVec w
i n : Nat
h : ¬i < n
h₁ : i < w
⊢ n + (w - 1 - i) = w - 1 - (i - n)

Tactic:
omega

Result:
no goals