-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_append {x : BitVec w} {y : BitVec v} :
    (x ++ y).setWidth k = if h : k ≤ v then y.setWidth k else (x.setWidth (k - v) ++ y).cast (by omega)

Proof state:
case pred.isFalse.isFalse
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
h₁ : ¬i < v
h₂ : ¬k ≤ v
⊢ (decide True && x.getLsbD (i - v)) = (BitVec.cast ⋯ (setWidth (k - v) x ++ y)).getLsbD i

Tactic:
simp [getLsbD_append, h₁]

Result:
case pred.isFalse.isFalse
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
h₁ : ¬i < v
h₂ : ¬k ≤ v
⊢ x.getLsbD (i - v) = true → i - v < k - v

Proof state:
case pred.isTrue.isFalse
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
h₁ : i < v
h₂ : ¬k ≤ v
⊢ (decide True && y.getLsbD i) = (BitVec.cast ⋯ (setWidth (k - v) x ++ y)).getLsbD i

Tactic:
simp [getLsbD_append, h₁]

Result:
no goals

Proof state:
case pred
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
⊢ (setWidth k (x ++ y)).getLsbD i =
    (if h : k ≤ v then setWidth k y else BitVec.cast ⋯ (setWidth (k - v) x ++ y)).getLsbD i

Tactic:
simp only [getLsbD_setWidth, h, getLsbD_append]

Result:
case pred
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
⊢ (decide True && if i < v then y.getLsbD i else x.getLsbD (i - v)) =
    (if h : k ≤ v then setWidth k y else BitVec.cast ⋯ (setWidth (k - v) x ++ y)).getLsbD i

Proof state:
w v k : Nat
x : BitVec w
y : BitVec v
h : ¬k ≤ v
⊢ k - v + v = k

Tactic:
omega

Result:
no goals

Proof state:
case pred
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
⊢ (decide True && if i < v then y.getLsbD i else x.getLsbD (i - v)) =
    (if h : k ≤ v then setWidth k y else BitVec.cast ⋯ (setWidth (k - v) x ++ y)).getLsbD i

Tactic:
split <;> rename_i h₁ <;> split <;> rename_i h₂

Result:
case pred.isTrue.isTrue
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
h₁ : i < v
h₂ : k ≤ v
⊢ (decide True && y.getLsbD i) = (setWidth k y).getLsbD i

case pred.isTrue.isFalse
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
h₁ : i < v
h₂ : ¬k ≤ v
⊢ (decide True && y.getLsbD i) = (BitVec.cast ⋯ (setWidth (k - v) x ++ y)).getLsbD i

case pred.isFalse.isTrue
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
h₁ : ¬i < v
h₂ : k ≤ v
⊢ (decide True && x.getLsbD (i - v)) = (setWidth k y).getLsbD i

case pred.isFalse.isFalse
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
h₁ : ¬i < v
h₂ : ¬k ≤ v
⊢ (decide True && x.getLsbD (i - v)) = (BitVec.cast ⋯ (setWidth (k - v) x ++ y)).getLsbD i

Proof state:
w v k : Nat
x : BitVec w
y : BitVec v
⊢ setWidth k (x ++ y) = if h : k ≤ v then setWidth k y else BitVec.cast ⋯ (setWidth (k - v) x ++ y)

Tactic:
ext i h

Result:
case pred
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
⊢ (setWidth k (x ++ y)).getLsbD i =
    (if h : k ≤ v then setWidth k y else BitVec.cast ⋯ (setWidth (k - v) x ++ y)).getLsbD i

Proof state:
case pred.isFalse.isTrue
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
h₁ : ¬i < v
h₂ : k ≤ v
⊢ (decide True && x.getLsbD (i - v)) = (setWidth k y).getLsbD i

Tactic:
omega

Result:
no goals

Proof state:
case pred.isTrue.isTrue
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
h₁ : i < v
h₂ : k ≤ v
⊢ (decide True && y.getLsbD i) = (setWidth k y).getLsbD i

Tactic:
simp [h]

Result:
no goals

Proof state:
case pred.isFalse.isFalse
w v k : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < k
h₁ : ¬i < v
h₂ : ¬k ≤ v
⊢ x.getLsbD (i - v) = true → i - v < k - v

Tactic:
omega

Result:
no goals