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

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

Tactic:
simp only [RefVec.get, Ref.mk.injEq]

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
hidx : idx < w * curr
h✝ : ¬curr < n
⊢ (⋯ ▸ s).refs[idx] = s.refs[idx]

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
hidx : idx < w * curr
h✝ : ¬curr < n
⊢ (let_fun this := ⋯;
        this ▸ s).get
      idx ⋯ =
    s.get idx hidx

Tactic:
dsimp only

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

Proof state:
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
hidx : idx < w * curr
h✝ : curr < n
⊢ (go n input (curr + 1) ⋯ (s.append input)).get idx ⋯ = s.get idx hidx

Tactic:
rw [go_get_aux]

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
hidx : idx < w * curr
h✝ : curr < n
⊢ (s.append input).get idx ?isTrue.hidx = s.get idx hidx

case isTrue.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
hidx : idx < w * curr
h✝ : curr < n
⊢ idx < w * (curr + 1)

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
hidx : idx < w * curr
h✝ : ¬curr < n
⊢ (⋯ ▸ s).refs[idx] = s.refs[idx]

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
hidx : idx < w * curr
h✝ : ¬curr < n
this : curr = n
⊢ (⋯ ▸ s).refs[idx] = s.refs[idx]

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

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
hidx : idx < w * curr
h✝ : curr < n
⊢ (let s := s.append input;
        go n input (curr + 1) ⋯ s).get
      idx ⋯ =
    s.get idx hidx

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
hidx : idx < w * curr
h✝ : ¬curr < n
⊢ (let_fun this := ⋯;
        this ▸ s).get
      idx ⋯ =
    s.get idx hidx

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

case isTrue.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
hidx : idx < w * curr
h✝ : curr < n
⊢ idx < w * curr + w

Tactic:
simp only [hidx, ↓reduceDIte]

Result:
case isTrue.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
hidx : idx < w * curr
h✝ : curr < n
⊢ idx < w * curr + w

Proof state:
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
hidx : idx < w * curr
h✝ : curr < n
⊢ (let s := s.append input;
        go n input (curr + 1) ⋯ s).get
      idx ⋯ =
    s.get idx hidx

Tactic:
dsimp only

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
hidx : idx < w * curr
h✝ : curr < n
⊢ (go n input (curr + 1) ⋯ (s.append input)).get idx ⋯ = s.get idx hidx

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

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

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
hidx : idx < w * curr
h✝ : ¬curr < n
⊢ curr = n

Tactic:
omega

Result:
no goals

Proof state:
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
hidx : idx < w * curr
h✝ : curr < n
⊢ (s.append input).get idx ?isTrue.hidx = s.get idx hidx

case isTrue.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
hidx : idx < w * curr
h✝ : curr < n
⊢ idx < w * (curr + 1)

Tactic:
rw [AIG.RefVec.get_append]

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

case isTrue.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
hidx : idx < w * curr
h✝ : curr < n
⊢ idx < w * curr + w

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx : idx < w * curr
hcurr : curr ≤ curr
h✝ : ¬curr < curr
⊢ (⋯ ▸ s).refs[idx] = s.refs[idx]

Tactic:
simp

Result:
no goals