-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem replicate_append_self {x : BitVec w} :
    x ++ x.replicate n = (x.replicate n ++ x).cast (by omega)

Proof state:
case succ
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ x ++ replicate (n + 1) x = BitVec.cast ⋯ (replicate (n + 1) x ++ x)

Tactic:
rw [replicate_succ]

Result:
case succ
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ x ++ BitVec.cast ⋯ (x ++ replicate n x) = BitVec.cast ⋯ (BitVec.cast ⋯ (x ++ replicate n x) ++ x)

Proof state:
case succ
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ x ++ BitVec.cast ⋯ (x ++ replicate n x) = BitVec.cast ⋯ (BitVec.cast ⋯ (x ++ replicate n x) ++ x)

Tactic:
conv => lhs; rw [ih]

Result:
case succ
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ x ++ BitVec.cast ⋯ (BitVec.cast ⋯ (replicate n x ++ x)) = BitVec.cast ⋯ (BitVec.cast ⋯ (x ++ replicate n x) ++ x)

Proof state:
w n : Nat
x : BitVec w
⊢ w * n + w = w + w * n

Tactic:
omega

Result:
no goals

Proof state:
case succ
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ x ++ (replicate n x ++ x) = BitVec.cast ⋯ (BitVec.cast ?succ.h (BitVec.cast ⋯ (x ++ (replicate n x ++ x))))

Tactic:
congr

Result:
no goals

Proof state:
case succ
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ x ++ (replicate n x ++ x) = BitVec.cast ⋯ (BitVec.cast ⋯ (x ++ replicate n x) ++ x)

Tactic:
rw [← cast_append_left]

Result:
case succ
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ x ++ (replicate n x ++ x) = BitVec.cast ⋯ (BitVec.cast ?succ.h (x ++ replicate n x ++ x))

case succ.h
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ w + w * n + w = w * (n + 1) + w

Proof state:
case succ.h
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ w + w * n + w = w * (n + 1) + w

Tactic:
rw [Nat.add_comm, Nat.mul_add, Nat.mul_one]

Result:
case succ.h
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ w + (w + w * n) = w * n + w + w

Proof state:
case zero
w : Nat
x : BitVec w
⊢ x ++ replicate 0 x = BitVec.cast ⋯ (replicate 0 x ++ x)

Tactic:
simp

Result:
no goals

Proof state:
case succ
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ x ++ (replicate n x ++ x) = BitVec.cast ⋯ (BitVec.cast ?succ.h (x ++ replicate n x ++ x))

Tactic:
rw [append_assoc]

Result:
case succ
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ x ++ (replicate n x ++ x) = BitVec.cast ⋯ (BitVec.cast ?succ.h (BitVec.cast ⋯ (x ++ (replicate n x ++ x))))

Proof state:
case succ.h
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ w + (w + w * n) = w * n + w + w

Tactic:
omega

Result:
no goals

Proof state:
case succ
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ x ++ BitVec.cast ⋯ (BitVec.cast ⋯ (replicate n x ++ x)) = BitVec.cast ⋯ (BitVec.cast ⋯ (x ++ replicate n x) ++ x)

Tactic:
simp only [cast_cast, cast_eq]

Result:
case succ
w : Nat
x : BitVec w
n : Nat
ih : x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
⊢ x ++ (replicate n x ++ x) = BitVec.cast ⋯ (BitVec.cast ⋯ (x ++ replicate n x) ++ x)