-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
    (x.replicate n).getLsbD i =
    (decide (i < w * n) && x.getLsbD (i % w))

Proof state:
i n w : Nat
x : BitVec w
⊢ (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))

Tactic:
induction n generalizing x

Result:
case zero
i w : Nat
x : BitVec w
⊢ (replicate 0 x).getLsbD i = (decide (i < w * 0) && x.getLsbD (i % w))

case succ
i w n✝ : Nat
a✝ : ∀ (x : BitVec w), (replicate n✝ x).getLsbD i = (decide (i < w * n✝) && x.getLsbD (i % w))
x : BitVec w
⊢ (replicate (n✝ + 1) x).getLsbD i = (decide (i < w * (n✝ + 1)) && x.getLsbD (i % w))

Proof state:
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : ¬i < w * n + w
⊢ ¬i < w * n

Tactic:
omega

Result:
no goals

Proof state:
i w : Nat
x : BitVec w
⊢ (replicate 0 x).getLsbD i = (decide (i < w * 0) && x.getLsbD (i % w))

Tactic:
simp

Result:
no goals

Proof state:
case neg
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : i < w * (n + 1)
hi' : ¬i < w * n
⊢ x.getLsbD (i - w * n) = x.getLsbD (i % w)

Tactic:
rw [Nat.sub_mul_eq_mod_of_lt_of_le] <;> omega

Result:
no goals

Proof state:
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
⊢ (replicate (n + 1) x).getLsbD i = (decide (i < w * (n + 1)) && x.getLsbD (i % w))

Tactic:
simp only [replicate_succ, getLsbD_cast, getLsbD_append]

Result:
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) =
    (decide (i < w * (n + 1)) && x.getLsbD (i % w))

Proof state:
case pos
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : i < w * (n + 1)
hi' : i < w * n
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) = x.getLsbD (i % w)

Tactic:
simp [hi', ih]

Result:
no goals

Proof state:
case neg
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : ¬i < w * (n + 1)
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) =
    (decide (i < w * (n + 1)) && x.getLsbD (i % w))

Tactic:
rw [Nat.mul_succ] at hi ⊢

Result:
case neg
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : ¬i < w * n + w
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) =
    (decide (i < w * n + w) && x.getLsbD (i % w))

Proof state:
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) =
    (decide (i < w * (n + 1)) && x.getLsbD (i % w))

Tactic:
by_cases hi : i < w * (n + 1)

Result:
case pos
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : i < w * (n + 1)
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) =
    (decide (i < w * (n + 1)) && x.getLsbD (i % w))

case neg
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : ¬i < w * (n + 1)
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) =
    (decide (i < w * (n + 1)) && x.getLsbD (i % w))

Proof state:
case neg
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : i < w * (n + 1)
hi' : ¬i < w * n
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) = x.getLsbD (i % w)

Tactic:
simp [hi', decide_false]

Result:
case neg
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : i < w * (n + 1)
hi' : ¬i < w * n
⊢ x.getLsbD (i - w * n) = x.getLsbD (i % w)

Proof state:
case neg
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : ¬i < w * n + w
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) =
    (decide (i < w * n + w) && x.getLsbD (i % w))

Tactic:
simp only [show ¬i < w * n by omega, decide_false, cond_false, hi, Bool.false_and]

Result:
case neg
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : ¬i < w * n + w
⊢ (if False then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) = false

Proof state:
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : ¬i < w * n + w
⊢ w ≤ i - w * n

Tactic:
omega

Result:
no goals

Proof state:
case pos
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : i < w * (n + 1)
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) = x.getLsbD (i % w)

Tactic:
by_cases hi' : i < w * n

Result:
case pos
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : i < w * (n + 1)
hi' : i < w * n
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) = x.getLsbD (i % w)

case neg
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : i < w * (n + 1)
hi' : ¬i < w * n
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) = x.getLsbD (i % w)

Proof state:
case pos
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : i < w * (n + 1)
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) =
    (decide (i < w * (n + 1)) && x.getLsbD (i % w))

Tactic:
simp only [hi, decide_true, Bool.true_and]

Result:
case pos
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : i < w * (n + 1)
⊢ (if i < w * n then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) = x.getLsbD (i % w)

Proof state:
case zero
i w : Nat
x : BitVec w
⊢ (replicate 0 x).getLsbD i = (decide (i < w * 0) && x.getLsbD (i % w))

case succ
i w n✝ : Nat
a✝ : ∀ (x : BitVec w), (replicate n✝ x).getLsbD i = (decide (i < w * n✝) && x.getLsbD (i % w))
x : BitVec w
⊢ (replicate (n✝ + 1) x).getLsbD i = (decide (i < w * (n✝ + 1)) && x.getLsbD (i % w))

Tactic:
case zero => simp

Result:
case succ
i w n✝ : Nat
a✝ : ∀ (x : BitVec w), (replicate n✝ x).getLsbD i = (decide (i < w * n✝) && x.getLsbD (i % w))
x : BitVec w
⊢ (replicate (n✝ + 1) x).getLsbD i = (decide (i < w * (n✝ + 1)) && x.getLsbD (i % w))

Proof state:
case neg
i w n : Nat
ih : ∀ (x : BitVec w), (replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
x : BitVec w
hi : ¬i < w * n + w
⊢ (if False then (replicate n x).getLsbD i else x.getLsbD (i - w * n)) = false

Tactic:
apply BitVec.getLsbD_ge (x := x) (i := i - w * n) (ge := by omega)

Result:
no goals