-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem cons_append_append (x : BitVec w₁) (y : BitVec w₂) (z : BitVec w₃) (a : Bool) :
    (cons a x) ++ y ++ z = (cons a (x ++ y ++ z)).cast (by omega)

Proof state:
case pred
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
⊢ (if i < w₃ then z.getLsbD i
    else
      if i - w₃ < w₂ then y.getLsbD (i - w₃)
      else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i < w₁ + w₂ + w₃ then
      if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)
    else decide (i - (w₁ + w₂ + w₃) = 0) && a

Tactic:
by_cases h₀ : i < w₁ + w₂ + w₃

Result:
case pos
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
⊢ (if i < w₃ then z.getLsbD i
    else
      if i - w₃ < w₂ then y.getLsbD (i - w₃)
      else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i < w₁ + w₂ + w₃ then
      if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)
    else decide (i - (w₁ + w₂ + w₃) = 0) && a

case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
⊢ (if i < w₃ then z.getLsbD i
    else
      if i - w₃ < w₂ then y.getLsbD (i - w₃)
      else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i < w₁ + w₂ + w₃ then
      if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)
    else decide (i - (w₁ + w₂ + w₃) = 0) && a

Proof state:
case pos
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
⊢ (if i < w₃ then z.getLsbD i
    else
      if i - w₃ < w₂ then y.getLsbD (i - w₃)
      else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i < w₁ + w₂ + w₃ then
      if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)
    else decide (i - (w₁ + w₂ + w₃) = 0) && a

Tactic:
simp only [h₀, ↓reduceIte]

Result:
case pos
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
⊢ (if i < w₃ then z.getLsbD i
    else
      if i - w₃ < w₂ then y.getLsbD (i - w₃)
      else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)

Proof state:
case pos
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
h₂ : i < w₃
⊢ z.getLsbD i = a

Tactic:
omega

Result:
no goals

Proof state:
case pos
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
h₂ : i < w₃
⊢ (if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else a) = a

Tactic:
simp [h₂]

Result:
case pos
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
h₂ : i < w₃
⊢ z.getLsbD i = a

Proof state:
case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
h₁ : ¬i < w₃
⊢ (if i - w₃ < w₂ then y.getLsbD (i - w₃)
    else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)

Tactic:
by_cases h₂ : i - w₃ < w₂

Result:
case pos
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
h₁ : ¬i < w₃
h₂ : i - w₃ < w₂
⊢ (if i - w₃ < w₂ then y.getLsbD (i - w₃)
    else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)

case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : i < w₁ + w₂ + w₃
h₁ : ¬i < w₃
h₂ : ¬i - w₃ < w₂
⊢ (if i - w₃ < w₂ then y.getLsbD (i - w₃)
    else if i - w₃ - w₂ < w₁ then x.getLsbD (i - w₃ - w₂) else decide (i - w₃ - w₂ - w₁ = 0) && a) =
    if i - w₃ < w₂ then y.getLsbD (i - w₃) else x.getLsbD (i - w₃ - w₂)

Proof state:
case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
h₂ : ¬i < w₃
⊢ (if i < w₃ then z.getLsbD i else if i - w₃ < w₂ then y.getLsbD (i - w₃) else a) = a

Tactic:
simp [h₂]

Result:
case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
h₂ : ¬i < w₃
⊢ i - w₃ < w₂ → y.getLsbD (i - w₃) = a

Proof state:
case neg
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
h₂ : ¬i < w₃
⊢ i - w₃ < w₂ → y.getLsbD (i - w₃) = a

Tactic:
omega

Result:
no goals

Proof state:
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
a : Bool
i : Nat
h : i < w₁ + 1 + w₂ + w₃
h₀ : ¬i < w₁ + w₂ + w₃
⊢ i - (w₁ + w₂ + w₃) = 0

Tactic:
omega

Result:
no goals