fix: do not lift (<- ...) over pure if-then-else

[leodemoura]

Now, only (<- ...)s occurring in the condition of a pure if-then-else are lifted.
That is, if (<- foo) then ... else ... is ok, but if ... then (<- foo) else ... is not. See #3713

closes #3713

This PR also adjusts this repo. Note that some of the (<- ...) were harmless since they were just accessing some
read-only state.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-04-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-04-01 21:36:14)

[alexjbest]

Thank you Leo! I got hit by this again recently so I am very happy to see it fixed

[eric-wieser]

I've filed this as #3827, since it also impacts Qq; am I right in thinking that this is tracked by the following TODO?

lean4/src/Lean/Elab/Do.lean

Lines 81 to 82 in 47f3e6b

	-- TODO: we must track whether we are inside a quotation or not.
	private partial def hasLiftMethod : Syntax → Bool