-- 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)
⊢ (if h : idx < w * curr then s.get idx h else input.get (idx - w * curr) ⋯) = input.get (idx % w) ⋯

Tactic:
have : ¬ (idx < w * curr) := by omega

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)
this : ¬idx < w * curr
⊢ (if h : idx < w * curr then s.get idx h else input.get (idx - w * curr) ⋯) = input.get (idx % w) ⋯

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
⊢ w * curr ≤ 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
⊢ (if h : curr < n then
          let s := s.append input;
          go n input (curr + 1) ⋯ s
        else
          let_fun this := ⋯;
          this ▸ s).get
      idx hidx1 =
    input.get (idx % w) ⋯

Tactic:
dsimp only

Result:
α : 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) ⋯

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), w * curr ≤ idx → (go n input curr hcurr s).get idx hidx1 = input.get (idx % w) ⋯

Tactic:
intro idx hidx1 hidx2

Result:
α : 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
⊢ (go n input curr hcurr s).get idx hidx1 = input.get (idx % w) ⋯

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 * curr) % w

Tactic:
rw [Nat.mod_eq_of_lt]

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 < 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
⊢ (go n input curr hcurr s).get idx hidx1 = input.get (idx % w) ⋯

Tactic:
unfold go

Result:
α : 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
          let s := s.append input;
          go n input (curr + 1) ⋯ s
        else
          let_fun this := ⋯;
          this ▸ s).get
      idx hidx1 =
    input.get (idx % w) ⋯

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
⊢ (if h : idx < w * curr then s.get idx h else input.get (idx - w * curr) ⋯) = input.get (idx % w) ⋯

Tactic:
simp only [this, ↓reduceDIte]

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)
this : ¬idx < w * curr
⊢ input.get (idx - w * curr) ⋯ = input.get (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
⊢ (⋯ ▸ s).get idx hidx1 = input.get (idx % w) ⋯

Tactic:
have : curr = n := by omega

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 * curr ≤ idx
h✝ : ¬curr < n
this : curr = n
⊢ (⋯ ▸ s).get idx hidx1 = input.get (idx % w) ⋯

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)
⊢ (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)

Tactic:
rw [AIG.RefVec.get_append]

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)
⊢ (if h : idx < w * curr then s.get idx h else input.get (idx - w * curr) ⋯) = 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 + w