That's not really true. It is pretty difficult to delete any data from git, especially by accident. You may screw up your history but you can always fix that if you know what you are doing.
Yes. Git push does not remove the previous commit, but changes the HEAD of the branch to be another commit.
The old commit becomes unconnected, but you can still get to it if you know its hash. There's also a way to list all unconnected commits, which is a bit involved.
Unconnected commits will exist and take up space until garbage collection is done.
If you pushed by mistake on a remote branch instead of creating a PR from a new branch, then you revert the commit, you're going to have trouble with the PR not showing all the changes because they match the orphaned commit.
Note that PR is not a fundamental git concept, but something a code forge can decide to implement any way they like. I presume you're talking about GitHub, because in GitLab, you will be able to see all changes when browsing commits constituting the merge request.
Is this a general rule? If so, I'd appreciate a suggested best practice for the following case: say I commit, push, then a while later fix some minor error and don't want it to be a separate commit (otherwise my commit history would get unmanageable). So I gc --amend and then gp --force. What would be the correct way to do this?
For the specific thing you want, force push is the only way AFAIK. However, my argument is that you should let the commits reflect the true history of the code. Fix the minor error and explain it in the message.
The downside of the "true history" approach, besides obvious aesthetic reasons, is that it precludes the use of such tools as `git bisect` and `git blame`.
