-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_setWidth {m : Nat} {x : BitVec n} {i : Nat} :
    getMsbD (setWidth m x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m))

Proof state:
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
⊢ m - n = 0

Tactic:
omega

Result:
no goals

Proof state:
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
h' : i < m
⊢ i + n - m < n

Tactic:
omega

Result:
no goals

Proof state:
case pos
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
h' : i < m
⊢ x.getLsbD (m - 1 - i) = true → i < m

Tactic:
omega

Result:
no goals

Proof state:
n m : Nat
x : BitVec n
i : Nat
⊢ (setWidth m x).getMsbD i = (decide (m - n ≤ i) && x.getMsbD (i + n - m))

Tactic:
unfold setWidth

Result:
n m : Nat
x : BitVec n
i : Nat
⊢ (if h : n ≤ m then setWidth' h x else BitVec.ofNat m x.toNat).getMsbD i =
    (decide (m - n ≤ i) && x.getMsbD (i + n - m))

Proof state:
case neg
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
h' : ¬i < m
⊢ (decide (i < m) && (if h_1 : False then setWidth' ⋯ x else BitVec.ofNat m x.toNat).getLsbD (m - 1 - i)) =
    (decide (0 ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

Tactic:
simp [h']

Result:
case neg
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
h' : ¬i < m
⊢ i + n - m < n → x.getLsbD (n - 1 - (i + n - m)) = false

Proof state:
case neg
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
⊢ (if h_1 : False then setWidth' ⋯ x else BitVec.ofNat m x.toNat).getMsbD i =
    (decide (m - n ≤ i) && x.getMsbD (i + n - m))

Tactic:
simp only [show m - n = 0 by omega, getMsbD, getLsbD_setWidth]

Result:
case neg
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
⊢ (decide (i < m) && (if h_1 : False then setWidth' ⋯ x else BitVec.ofNat m x.toNat).getLsbD (m - 1 - i)) =
    (decide (0 ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

Proof state:
case neg
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
⊢ (decide (i < m) && (if h_1 : False then setWidth' ⋯ x else BitVec.ofNat m x.toNat).getLsbD (m - 1 - i)) =
    (decide (0 ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

Tactic:
by_cases h' : i < m

Result:
case pos
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
h' : i < m
⊢ (decide (i < m) && (if h_1 : False then setWidth' ⋯ x else BitVec.ofNat m x.toNat).getLsbD (m - 1 - i)) =
    (decide (0 ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case neg
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
h' : ¬i < m
⊢ (decide (i < m) && (if h_1 : False then setWidth' ⋯ x else BitVec.ofNat m x.toNat).getLsbD (m - 1 - i)) =
    (decide (0 ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

Proof state:
n m : Nat
x : BitVec n
i : Nat
⊢ (if h : n ≤ m then setWidth' h x else BitVec.ofNat m x.toNat).getMsbD i =
    (decide (m - n ≤ i) && x.getMsbD (i + n - m))

Tactic:
by_cases h : n ≤ m <;> simp only [h]

Result:
case pos
n m : Nat
x : BitVec n
i : Nat
h : n ≤ m
⊢ (if h_1 : True then setWidth' ⋯ x else BitVec.ofNat m x.toNat).getMsbD i =
    (decide (m - n ≤ i) && x.getMsbD (i + n - m))

case neg
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
⊢ (if h_1 : False then setWidth' ⋯ x else BitVec.ofNat m x.toNat).getMsbD i =
    (decide (m - n ≤ i) && x.getMsbD (i + n - m))

Proof state:
n m : Nat
x : BitVec n
i : Nat
h : n ≤ m
h' : ¬m - n ≤ i
⊢ i - (m - n) = i + n - m

Tactic:
omega

Result:
no goals

Proof state:
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
h' : i < m
⊢ n - 1 - (i + n - m) = m - 1 - i

Tactic:
omega

Result:
no goals

Proof state:
case pos
n m : Nat
x : BitVec n
i : Nat
h : n ≤ m
⊢ (if h_1 : True then setWidth' ⋯ x else BitVec.ofNat m x.toNat).getMsbD i =
    (decide (m - n ≤ i) && x.getMsbD (i + n - m))

Tactic:
by_cases h' : m - n ≤ i
<;> simp [h', show i - (m - n) = i + n - m by omega]

Result:
no goals

Proof state:
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
h' : i < m
⊢ m - 1 - i < m

Tactic:
omega

Result:
no goals

Proof state:
case pos
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
h' : i < m
⊢ (decide (i < m) && (if h_1 : False then setWidth' ⋯ x else BitVec.ofNat m x.toNat).getLsbD (m - 1 - i)) =
    (decide (0 ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

Tactic:
simp [show m - 1 - i < m by omega, show i + n - m < n by omega,
  show n - 1 - (i + n - m) = m - 1 - i by omega]

Result:
case pos
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
h' : i < m
⊢ x.getLsbD (m - 1 - i) = true → i < m

Proof state:
case neg
n m : Nat
x : BitVec n
i : Nat
h : ¬n ≤ m
h' : ¬i < m
⊢ i + n - m < n → x.getLsbD (n - 1 - (i + n - m)) = false

Tactic:
omega

Result:
no goals