. dsimp at hgo
  rw [← hgo]
  intro hfoo
  rw [go_getRef_aux]
  rw [AIG.RefStream.getRef_push_ref_lt]
  . simp only [Ref.cast, Ref.mk.injEq]
    rw [AIG.RefStream.getRef_cast]
    . simp
    . assumption
  . apply go_le_size
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  (let res := aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.pushRef bitRef;
    go w aig_1 (curr + 1) s a ⋯) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo

case isFalse
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : ¬curr < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
case isFalse
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : ¬curr < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo