-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem reverse_append {x : BitVec w} {y : BitVec v} :
    (x ++ y).reverse = (y.reverse ++ x.reverse).cast (by omega)

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

Tactic:
omega

Result:
no goals

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

Tactic:
by_cases hi : i < v

Result:
case pos
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : i < v
⊢ (x ++ y).getMsbD i = (BitVec.cast ⋯ (y.reverse ++ x.reverse)).getLsbD i

case neg
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : ¬i < v
⊢ (x ++ y).getMsbD i = (BitVec.cast ⋯ (y.reverse ++ x.reverse)).getLsbD i

Proof state:
case neg
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : i < v
hw : ¬w ≤ i
⊢ (x ++ y).getMsbD i = (BitVec.cast ⋯ (y.reverse ++ x.reverse)).getLsbD i

Tactic:
simp [getMsbD_append, getLsbD_cast, getLsbD_append, getLsbD_reverse, hw, show i < w by omega]

Result:
no goals

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

Tactic:
simp only [getLsbD_append, getLsbD_reverse]

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

Proof state:
case pos
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : i < v
hw : w ≤ i
⊢ (x ++ y).getMsbD i = (BitVec.cast ⋯ (y.reverse ++ x.reverse)).getLsbD i

Tactic:
simp [getMsbD_append, getLsbD_cast, getLsbD_append, getLsbD_reverse, hw]

Result:
no goals

Proof state:
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : ¬i < v
hw : ¬w ≤ i
⊢ i < w

Tactic:
omega

Result:
no goals

Proof state:
case neg
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : ¬i < v
⊢ (x ++ y).getMsbD i = (BitVec.cast ⋯ (y.reverse ++ x.reverse)).getLsbD i

Tactic:
by_cases hw : w ≤ i

Result:
case pos
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : ¬i < v
hw : w ≤ i
⊢ (x ++ y).getMsbD i = (BitVec.cast ⋯ (y.reverse ++ x.reverse)).getLsbD i

case neg
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : ¬i < v
hw : ¬w ≤ i
⊢ (x ++ y).getMsbD i = (BitVec.cast ⋯ (y.reverse ++ x.reverse)).getLsbD i

Proof state:
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : ¬i < v
hw : w ≤ i
⊢ ¬i < w

Tactic:
omega

Result:
no goals

Proof state:
case neg
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : ¬i < v
hw : ¬w ≤ i
⊢ (x ++ y).getMsbD i = (BitVec.cast ⋯ (y.reverse ++ x.reverse)).getLsbD i

Tactic:
simp [getMsbD_append, getLsbD_cast, getLsbD_append, hw, show i < w by omega, getLsbD_reverse]

Result:
no goals

Proof state:
case pos
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : i < v
⊢ (x ++ y).getMsbD i = (BitVec.cast ⋯ (y.reverse ++ x.reverse)).getLsbD i

Tactic:
by_cases hw : w ≤ i

Result:
case pos
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : i < v
hw : w ≤ i
⊢ (x ++ y).getMsbD i = (BitVec.cast ⋯ (y.reverse ++ x.reverse)).getLsbD i

case neg
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : i < v
hw : ¬w ≤ i
⊢ (x ++ y).getMsbD i = (BitVec.cast ⋯ (y.reverse ++ x.reverse)).getLsbD i

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

Tactic:
ext i h

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

Proof state:
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : i < v
hw : ¬w ≤ i
⊢ i < w

Tactic:
omega

Result:
no goals

Proof state:
case pos
w v : Nat
x : BitVec w
y : BitVec v
i : Nat
h : i < w + v
hi : ¬i < v
hw : w ≤ i
⊢ (x ++ y).getMsbD i = (BitVec.cast ⋯ (y.reverse ++ x.reverse)).getLsbD i

Tactic:
simp [getMsbD_append, getLsbD_cast, getLsbD_append, hw, show ¬ i < w by omega, getLsbD_reverse]

Result:
no goals