. dsimp
  refine Nat.le_trans ?_ (by apply go_le_size)
  apply AIG.LawfulOperator.le_size
case isTrue
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤
    (let res := aig.mkAtomCached (BVBit.mk a ⟨idx, h✝⟩);
          let aig_1 := res.aig;
          let bitRef := res.ref;
          let s := s.cast ⋯;
          let s := s.pushRef bitRef;
          go w aig_1 (idx + 1) s a ⋯).aig.decls.size

case isFalse
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : ¬idx < w
⊢ aig.decls.size ≤
    (let_fun hidx := ⋯;
          { aig := aig, stream := hidx ▸ s }).aig.decls.size
case isFalse
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : ¬idx < w
⊢ aig.decls.size ≤
    (let_fun hidx := ⋯;
          { aig := aig, stream := hidx ▸ s }).aig.decls.size