feat(ring_theory/ideal): generalize from integral_closure to `is_in…

…tegral_closure` (#8944)

This PR restates a couple of lemmas about ideals the integral closure to use an instance of `is_integral_closure` instead. The originals are still available, but their proofs are now oneliners shelling out to `is_integral_closure`.