refine Nat.le_trans ?_ (by apply fold.go_le_size)
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ aig : AIG α
target : FoldTarget aig
⊢ aig.decls.size ≤
    (fold.go (aig.mkConstCached true).aig (aig.mkConstCached true).ref 0 target.len (target.stream.cast ⋯)
            target.func).aig.decls.size
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ aig : AIG α
target : FoldTarget aig
⊢ aig.decls.size ≤ (aig.mkConstCached true).aig.decls.size