Prove double negation of LEM in intuitionistic logic I understand that in intuitionistic logic, the law of excluded middle $P \lor \lnot P$ and double negation elimination $\lnot \lnot P \to P$ are not true in general (for every proposition $P$). However, I understand that $\lnot \lnot (P \lor \lnot P)$ and $P \to \lnot \lnot P$ are intuitionistically true in general. Is there an "intuitive" intuitionistic proof for these?

In general, see Glivenko's result.
Your statements we can prove by proving theorems in the positive fragment of intuitionistic logic with a propositional variable $C$ and then letting $C=\bot$.

*

*The double negation introduction, $A\to \neg\neg A$, is modus ponens in the form $$A\to ((A\to C)\to C)$$

*Similarly, $\neg\neg(A\lor\neg A)$ is the special case of $$\big[\big(A\lor(A\to C)\big)\to C\big]\to C$$
To see why this holds, note that when assuming $\big(A\lor(A\to C)\big)\to C$, it functions as a valid premise for itself.

It's worth pointing out that this goes through in logics weaker than intuitionistic logic. We do not need the principle of explosion to show it - and indeed we don't even use a conjunction "$\land$".

A more pedestrian proof of the latter can be obtained as follows. First note that the following holds:
$$\Big[\big((A\lor B)\to C\big)\land \big(((A\to C)\land (B\to C))\to D\big)\big]\to D$$
To see why this holds, note that expression $(A\lor B)\to C$ says that both $A$ and $B$ imply $C$, which is exactly what the second expression demands to prove $D$. Now consider the special case $B=A\to\bot$ and $C=D=\bot$, then this reads
$$\neg\big[\neg (A\lor \neg A) \land \neg((\neg A) \land \neg (\neg A)) \big]$$
Here the second term is just the [non-contradiction principle] for $\neg A$ and this holds by modus ponens. We're again left with $\neg\neg (A\lor \neg A)$.
Note: The user in the comments points out a variant of this proof that effectively uses one of the valid De Morgan's laws and also again the noncontradiction principle.
This avoids the fourth propositional variable, $D$. It basically uses $(P\to\bot) = \neg P$ instead of $\neg(P\land \neg\bot) = \neg P$ that I used above.
