chore(ring_theory/ideal/operations): golf and remove @ (#7347)
Instead of passing all these arguments explicitly, it's sufficient to just use `(... : _)` to get the elaborator to do the right thing.
This makes this proof less fragile to argument changes to `pi.ring_hom`, such as the planned generalization to non-associative rings
