chore(*): don't use tactic internal lemmas in proofs (#11641)
Some lemmas that are intended as internals to a tactic get picked up by library search and end up in proofs.
We replace a few of these tactic lemma uses with actual library lemmas which should be more maintainable, de-coupling tactic internals from the actual library.
