-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) :
    (x ++ y).cast h = x ++ y.cast (by omega)

Proof state:
case pred.isTrue.isFalse
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
h✝¹ : i✝ < v
h✝ : ¬i✝ < v'
⊢ y.getLsbD i✝ = x.getLsbD (i✝ - v')

Tactic:
omega

Result:
no goals

Proof state:
case pred.isTrue.isTrue
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
h✝¹ : i✝ < v
h✝ : i✝ < v'
⊢ y.getLsbD i✝ = y.getLsbD i✝

Tactic:
rfl

Result:
no goals

Proof state:
case pred
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
⊢ (if i✝ < v then y.getLsbD i✝ else x.getLsbD (i✝ - v)) = if i✝ < v' then y.getLsbD i✝ else x.getLsbD (i✝ - v')

Tactic:
split <;> split

Result:
case pred.isTrue.isTrue
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
h✝¹ : i✝ < v
h✝ : i✝ < v'
⊢ y.getLsbD i✝ = y.getLsbD i✝

case pred.isTrue.isFalse
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
h✝¹ : i✝ < v
h✝ : ¬i✝ < v'
⊢ y.getLsbD i✝ = x.getLsbD (i✝ - v')

case pred.isFalse.isTrue
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
h✝¹ : ¬i✝ < v
h✝ : i✝ < v'
⊢ x.getLsbD (i✝ - v) = y.getLsbD i✝

case pred.isFalse.isFalse
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
h✝¹ : ¬i✝ < v
h✝ : ¬i✝ < v'
⊢ x.getLsbD (i✝ - v) = x.getLsbD (i✝ - v')

Proof state:
case pred
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
⊢ (BitVec.cast h (x ++ y)).getLsbD i✝ = (x ++ BitVec.cast ⋯ y).getLsbD i✝

Tactic:
simp only [getLsbD_cast, getLsbD_append, cond_eq_if, decide_eq_true_eq]

Result:
case pred
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
⊢ (if i✝ < v then y.getLsbD i✝ else x.getLsbD (i✝ - v)) = if i✝ < v' then y.getLsbD i✝ else x.getLsbD (i✝ - v')

Proof state:
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
⊢ v = v'

Tactic:
omega

Result:
no goals

Proof state:
case pred.isFalse.isFalse
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
h✝¹ : ¬i✝ < v
h✝ : ¬i✝ < v'
⊢ x.getLsbD (i✝ - v) = x.getLsbD (i✝ - v')

Tactic:
congr

Result:
case pred.isFalse.isFalse.e_i.e_a
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
h✝¹ : ¬i✝ < v
h✝ : ¬i✝ < v'
⊢ v = v'

Proof state:
case pred.isFalse.isTrue
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
h✝¹ : ¬i✝ < v
h✝ : i✝ < v'
⊢ x.getLsbD (i✝ - v) = y.getLsbD i✝

Tactic:
omega

Result:
no goals

Proof state:
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
⊢ BitVec.cast h (x ++ y) = x ++ BitVec.cast ⋯ y

Tactic:
ext

Result:
case pred
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
⊢ (BitVec.cast h (x ++ y)).getLsbD i✝ = (x ++ BitVec.cast ⋯ y).getLsbD i✝

Proof state:
case pred.isFalse.isFalse.e_i.e_a
w v v' : Nat
h : w + v = w + v'
x : BitVec w
y : BitVec v
i✝ : Nat
a✝ : i✝ < w + v'
h✝¹ : ¬i✝ < v
h✝ : ¬i✝ < v'
⊢ v = v'

Tactic:
omega

Result:
no goals