Looking for an answer drawing from credible and/or official sources.

The "compare and swap" mentioned by torek in the comments and in his other answer is further illustrated by the sources of Git itself.

the latter only pushes to the remote if the remote does not have commits that the local branch doesn't have?

That feature was introduced in this commit (Dec. 2013, Git v1.8.5-rc0)

--force-with-lease will protect all remote refs that are going to be updated by requiring their current value to be the same as some reasonable default, unless otherwise specified;

For now, "some reasonable default" is tentatively defined as "the value of the remote-tracking branch we have for the ref of the remote being updated", and it is an error if we do not have such a remote-tracking branch.

So "lease" means:

"force-with-lease": You assume you took the lease on the ref when you fetched to decide what the rebased history should be, and you can push back only if the lease has not been broken.

"You assume you took the lease on the ref": So "lease" is used to describe a safety mechanism for force pushing changes to a remote repository.

When you fetch from a remote repository, you essentially get the latest state of the repository at that time. Think of this as taking a "snapshot" or a temporary "lease" on the repository's state.
The "lease" implies that you are aware of the repository's state as of the last fetch and are operating under the assumption that this state has not changed since.

When you use git push --force-with-lease, you are telling Git: "I want to force push my changes, but only if the remote repository is in the same state as my last fetch."
In other words, you can push your changes as long as no one else has pushed any updates to the remote repository since your last fetch.
If someone else has introduced changes to the remote repository (thereby "breaking the lease"), the push will be rejected. That helps prevent accidental overwriting of others' work.

The sources still mention "cas" ("compare and swap"):

• This option was originally called "cas" (for "compare and swap"), the name which nobody liked because it was too technical.
• The second attempt called it "lockref" (because it is conceptually like pushing after taking a lock) but the word "lock" was hated because it implied that it may reject push by others, which is not the way this option works.
• This round calls it "force-with-lease".
  You assume you took the lease on the ref when you fetched to decide what the rebased history should be, and you can push back only if the lease has not been broken.

So: "git push --force-with-lease vs. --force"

As I mentioned in "push --force-with-lease by default", Git 2.13 (Q2 2017) confirms that the option --force-with-lease can be ignored if a background process (like the ones you find in an IDE with a Git plugin) runs git fetch origin.
In that case, --force prevails.

As Pavlus adds in the comments:

it is not ignored per se, it is just now you have identical refs for local remote head and remote head, so --force-with-lease will behave correctly -- compare these two, and if in that interval of time between fetch and push, someone updated remote, it won't behave as --force, it will still fail.

Another difference: before Git 2.29 (Q4 2020), pushing a ref whose name contains a non-ASCII character with the "--force-with-lease" option did not work over smart HTTP protocol.
It would work with git push --force.

See commit cd85b44 (21 Jul 2020) by Brian m. Carlson (bk2204).
^{(Merged by Junio C Hamano -- gitster -- in commit c2796ac, 30 Jul 2020)}

remote-curl: make --force-with-lease work with non-ASCII ref names

^{Reported-by: Frej Bjon
Signed-off-by: brian m. carlson}

When we invoke a remote transport helper and pass an option with an argument, we quote the argument as a C-style string if necessary.
This is the case for the cas option, which implements the --force-with-lease command-line flag, when we're passing a non-ASCII refname.

However, the remote curl helper isn't designed to parse such an argument, meaning that if we try to use --force-with-lease with an HTTP push and a non-ASCII refname, we get an error like this:

error: cannot parse expected object name '0000000000000000000000000000000000000000"'  

Note the double quote, which get_oid has reminded us is not valid in an hex object ID.

Even if we had been able to parse it, we would send the wrong data to the server: we'd send an escaped ref, which would not behave as the user wanted and might accidentally result in updating or deleting a ref we hadn't intended.

Since we need to expect a quoted C-style string here, just check if the first argument is a double quote, and if so, unquote it.
Note that if the refname contains a double quote, then we will have double-quoted it already, so there is no ambiguity.

We test for this case only in the smart protocol, since the DAV-based protocol is not capable of handling this capability.
We use UTF-8 because this is nicer in our tests and friendlier to Windows, but the code should work for all non-ASCII refs.

While we're at it, since the name of the option is now well established and isn't going to change, let's inline it instead of using the #define constant.

Git 2.30 (Q1 2021) adds git push --force-if-includes

When a local branch that is based on a remote ref, has been rewound and is to be force pushed on the remote, "--force-if-includes" runs a check that ensures any updates to the remote-tracking ref that may have happened (by push from another repository) in-between the time of the last update to the local branch (via "git pull", for instance) and right before the time of push, have been integrated locally before allowing a forced update.

Does it mean that if I do fetch before pushing, then "force-with-lease" will happily overwrite the remote branch, even with other people's work in it? I wonder how well it plays with automatic fetching many IDEs do.

The --force-with-lease option is designed to protect against overwriting changes in the remote repository that you have not seen. When you use this option, Git checks that the remote branch has not changed since your last fetch. If the remote branch has been updated (e.g., by another collaborator's push), the --force-with-lease push will fail.

Automatic fetching by IDEs can lead to scenarios where you unintentionally overwrite changes made by others without reviewing them. This happens because your local view of the remote branch is kept up-to-date automatically, and --force-with-lease checks against this view.

So I would either deactivate the automatic fetch, or at least review the two branches (the current one, and its remote tracking counterpart) before making any force push (with lease or not).