-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem append_assoc {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w₃} :
    (x₁ ++ x₂) ++ x₃ = (x₁ ++ (x₂ ++ x₃)).cast (by omega)

Proof state:
case pred
w₂ w₃ n : Nat
x₁ : BitVec (n + 1)
x₂ : BitVec w₂
x₃ : BitVec w₃
ih : ∀ {x₂ : BitVec w₂} {x₃ : BitVec w₃}, setWidth n x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (setWidth n x₁ ++ (x₂ ++ x₃))
j : Nat
h : j < n + 1 + w₂ + w₃
⊢ (BitVec.cast ⋯ (cons x₁.msb (BitVec.cast ⋯ (setWidth n x₁ ++ (x₂ ++ x₃))))).getLsbD j =
    (BitVec.cast ⋯ (BitVec.cast ⋯ (cons x₁.msb (setWidth n x₁ ++ (x₂ ++ x₃))))).getLsbD j

Tactic:
simp [getLsbD_cons, show n + w₂ + w₃ = n + (w₂ + w₃) by omega]

Result:
no goals

Proof state:
w₂ w₃ n : Nat
x₁ : BitVec (n + 1)
x₂ : BitVec w₂
x₃ : BitVec w₃
ih : ∀ {x₂ : BitVec w₂} {x₃ : BitVec w₃}, setWidth n x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (setWidth n x₁ ++ (x₂ ++ x₃))
j : Nat
h : j < n + 1 + w₂ + w₃
⊢ n + w₂ + w₃ = n + (w₂ + w₃)

Tactic:
omega

Result:
no goals

Proof state:
w₂ w₃ n : Nat
x₁ : BitVec (n + 1)
x₂ : BitVec w₂
x₃ : BitVec w₃
ih : ∀ {x₂ : BitVec w₂} {x₃ : BitVec w₃}, setWidth n x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (setWidth n x₁ ++ (x₂ ++ x₃))
⊢ BitVec.cast ⋯ (cons x₁.msb (BitVec.cast ⋯ (setWidth n x₁ ++ (x₂ ++ x₃)))) =
    BitVec.cast ⋯ (BitVec.cast ⋯ (cons x₁.msb (setWidth n x₁ ++ (x₂ ++ x₃))))

Tactic:
ext j h

Result:
case pred
w₂ w₃ n : Nat
x₁ : BitVec (n + 1)
x₂ : BitVec w₂
x₃ : BitVec w₃
ih : ∀ {x₂ : BitVec w₂} {x₃ : BitVec w₃}, setWidth n x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (setWidth n x₁ ++ (x₂ ++ x₃))
j : Nat
h : j < n + 1 + w₂ + w₃
⊢ (BitVec.cast ⋯ (cons x₁.msb (BitVec.cast ⋯ (setWidth n x₁ ++ (x₂ ++ x₃))))).getLsbD j =
    (BitVec.cast ⋯ (BitVec.cast ⋯ (cons x₁.msb (setWidth n x₁ ++ (x₂ ++ x₃))))).getLsbD j

Proof state:
w₂ w₃ n : Nat
x₁ : BitVec (n + 1)
x₂ : BitVec w₂
x₃ : BitVec w₃
ih : ∀ {x₂ : BitVec w₂} {x₃ : BitVec w₃}, setWidth n x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (setWidth n x₁ ++ (x₂ ++ x₃))
⊢ x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))

Tactic:
rw [← cons_msb_setWidth x₁, cons_append_append, ih, cons_append]

Result:
w₂ w₃ n : Nat
x₁ : BitVec (n + 1)
x₂ : BitVec w₂
x₃ : BitVec w₃
ih : ∀ {x₂ : BitVec w₂} {x₃ : BitVec w₃}, setWidth n x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (setWidth n x₁ ++ (x₂ ++ x₃))
⊢ BitVec.cast ⋯ (cons x₁.msb (BitVec.cast ⋯ (setWidth n x₁ ++ (x₂ ++ x₃)))) =
    BitVec.cast ⋯ (BitVec.cast ⋯ (cons x₁.msb (setWidth n x₁ ++ (x₂ ++ x₃))))

Proof state:
w₁ w₂ w₃ : Nat
x₁ : BitVec w₁
x₂ : BitVec w₂
x₃ : BitVec w₃
⊢ x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))

Tactic:
induction w₁ generalizing x₂ x₃

Result:
case zero
w₂ w₃ : Nat
x₁ : BitVec 0
x₂ : BitVec w₂
x₃ : BitVec w₃
⊢ x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))

case succ
w₂ w₃ n✝ : Nat
a✝ : ∀ {x₁ : BitVec n✝} {x₂ : BitVec w₂} {x₃ : BitVec w₃}, x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))
x₁ : BitVec (n✝ + 1)
x₂ : BitVec w₂
x₃ : BitVec w₃
⊢ x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))

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

case succ
w₂ w₃ n✝ : Nat
a✝ : ∀ {x₁ : BitVec n✝} {x₂ : BitVec w₂} {x₃ : BitVec w₃}, x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))
x₁ : BitVec (n✝ + 1)
x₂ : BitVec w₂
x₃ : BitVec w₃
⊢ x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))

Tactic:
case zero => simp

Result:
case succ
w₂ w₃ n✝ : Nat
a✝ : ∀ {x₁ : BitVec n✝} {x₂ : BitVec w₂} {x₃ : BitVec w₃}, x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))
x₁ : BitVec (n✝ + 1)
x₂ : BitVec w₂
x₃ : BitVec w₃
⊢ x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))

Proof state:
w₁ w₂ w₃ : Nat
x₁ : BitVec w₁
x₂ : BitVec w₂
x₃ : BitVec w₃
⊢ w₁ + (w₂ + w₃) = w₁ + w₂ + w₃

Tactic:
omega

Result:
no goals

Proof state:
case succ
w₂ w₃ n✝ : Nat
a✝ : ∀ {x₁ : BitVec n✝} {x₂ : BitVec w₂} {x₃ : BitVec w₃}, x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))
x₁ : BitVec (n✝ + 1)
x₂ : BitVec w₂
x₃ : BitVec w₃
⊢ x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))

Tactic:
case succ n ih =>
  specialize @ih (setWidth n x₁)
  rw [← cons_msb_setWidth x₁, cons_append_append, ih, cons_append]
  ext j h
  simp [getLsbD_cons, show n + w₂ + w₃ = n + (w₂ + w₃) by omega]

Result:
no goals

Proof state:
w₂ w₃ n : Nat
ih : ∀ {x₁ : BitVec n} {x₂ : BitVec w₂} {x₃ : BitVec w₃}, x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))
x₁ : BitVec (n + 1)
x₂ : BitVec w₂
x₃ : BitVec w₃
⊢ x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))

Tactic:
specialize @ih (setWidth n x₁)

Result:
w₂ w₃ n : Nat
x₁ : BitVec (n + 1)
x₂ : BitVec w₂
x₃ : BitVec w₃
ih : ∀ {x₂ : BitVec w₂} {x₃ : BitVec w₃}, setWidth n x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (setWidth n x₁ ++ (x₂ ++ x₃))
⊢ x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))

Proof state:
w₂ w₃ : Nat
x₁ : BitVec 0
x₂ : BitVec w₂
x₃ : BitVec w₃
⊢ x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))

Tactic:
simp

Result:
no goals