. simp [Ref.hgate]
case hstart
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
assign : α → Bool
idx : Nat
hidx1 : idx < newWidth
hidx2 : curr ≤ idx
res : RefStreamEntry α newWidth
h✝ : curr < newWidth
heq : curr = idx
hsplit : ¬idx < w
hgo :
  go (aig.mkConstCached false).aig w (input.cast ⋯) newWidth (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
⊢ ((aig.mkConstCached false).ref.cast ⋯).gate < (aig.mkConstCached false).aig.decls.size
no goals