-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean
theorem go_get (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n)
    (input : AIG.RefVec aig w) (s : AIG.RefVec aig (w * curr)) :
    ∀ (idx : Nat) (hidx1 : idx < w * n),
        w * curr ≤ idx
          →
        (go n input curr hcurr s).get idx hidx1
          =
        input.get (idx % w) (aux2 hidx1)

Proof state:
case isTrue.inl
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx < w * (curr + 1)
⊢ (go n input (curr + 1) ⋯ (s.append input)).get idx hidx1 = input.get (idx % w) ⋯

Tactic:
rw [go_get_aux]

Result:
case isTrue.inl
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx < w * (curr + 1)
⊢ (s.append input).get idx ?isTrue.inl.hidx = input.get (idx % w) ⋯

case isTrue.inl.hidx
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx < w * (curr + 1)
⊢ idx < w * (curr + 1)

Proof state:
case isTrue.inl.hidx
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx < w * (curr + 1)
⊢ idx < w * curr + w

Tactic:
simpa using h

Result:
no goals

Proof state:
case isTrue.inl.e_idx
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx < w * (curr + 1)
this : ¬idx < w * curr
⊢ idx - w * curr < w

Tactic:
apply Nat.sub_lt_left_of_lt_add <;> assumption

Result:
no goals

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * n ≤ idx
h✝ : ¬curr < n
this : curr = n
⊢ (⋯ ▸ s).get idx hidx1 = input.get (idx % w) ⋯

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
⊢ (if h : curr < n then go n input (curr + 1) ⋯ (s.append input) else ⋯ ▸ s).get idx hidx1 = input.get (idx % w) ⋯

Tactic:
split

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
⊢ (go n input (curr + 1) ⋯ (s.append input)).get idx hidx1 = input.get (idx % w) ⋯

case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : ¬curr < n
⊢ (⋯ ▸ s).get idx hidx1 = input.get (idx % w) ⋯

Proof state:
case isTrue.inr.a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx ≥ w * (curr + 1)
⊢ w * (curr + 1) ≤ idx

Tactic:
assumption

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : ¬curr < n
⊢ curr = n

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.inr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx ≥ w * (curr + 1)
⊢ (go n input (curr + 1) ⋯ (s.append input)).get idx hidx1 = input.get (idx % w) ⋯

Tactic:
rw [go_get]

Result:
case isTrue.inr.a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx ≥ w * (curr + 1)
⊢ w * (curr + 1) ≤ idx

Proof state:
case isTrue.inl
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx < w * (curr + 1)
this : ¬idx < w * curr
⊢ input.get (idx - w * curr) ⋯ = input.get (idx % w) ⋯

Tactic:
congr 1

Result:
case isTrue.inl.e_idx
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx < w * (curr + 1)
this : ¬idx < w * curr
⊢ idx - w * curr = idx % w

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : ¬curr < n
this : curr = n
⊢ (⋯ ▸ s).get idx hidx1 = input.get (idx % w) ⋯

Tactic:
rw [this] at hidx2

Result:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * n ≤ idx
h✝ : ¬curr < n
this : curr = n
⊢ (⋯ ▸ s).get idx hidx1 = input.get (idx % w) ⋯

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx < w * (curr + 1)
⊢ ¬idx < w * curr

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.inl.e_idx
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx < w * (curr + 1)
this : ¬idx < w * curr
⊢ idx - w * curr = idx % w

Tactic:
rw [← Nat.sub_mul_mod (k := curr)]

Result:
case isTrue.inl.e_idx
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx < w * (curr + 1)
this : ¬idx < w * curr
⊢ idx - w * curr = (idx - w * curr) % w

case isTrue.inl.e_idx
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx1 : idx < w * n
hidx2 : w * curr ≤ idx
h✝ : curr < n
h : idx < w * (curr + 1)
this : ¬idx < w * curr
⊢ w * curr ≤ idx