The implication
$$
[((P\rightarrow Q)\rightarrow P)\rightarrow P ] \rightarrow P\lor\neg P \quad\quad\quad\quad (1)
$$
is in fact not a theorem of intuitionistic propositional logic. You can check this semantically, with a Kripke frame with two worlds $w_1\le w_2$, with $P, Q$ both satisfied in $w_2$ and none of them satisfied in $w_1$. See here for background.
Or you could try to prove (1) in a sequent calculus and discover that you get stuck.
What is true is that if you make Peirce's law an additional axiom, then $P\lor\neg P$ becomes a theorem. In symbols:
$$
\{((A\rightarrow B)\rightarrow A )\rightarrow A\} \vdash P\lor\neg P
$$
Here the curly brackets are supposed to refer to the collection of all substitution instances.
This is discussed in the answer you linked. (So Peirce's law and LEM are equivalent in the sense that adding either of them will give you classical logic.)
By the deduction theorem, you then also obtain an implication similar to (1) as a theorem, but if you check what (substitution) instance of Peirce's was actually used, you'll find that $A=P\lor\neg P$, $B=\bot$. So
$$
\vdash [((P\lor\neg P\rightarrow \bot)\rightarrow P\lor\neg P )\rightarrow P\lor\neg P] \rightarrow P\lor\neg P ,
$$
which of course is not the same as (1).
As for your last question, taken in an abstract sense, it is definitely possible to have "$\vdash A$ implies $\vdash B$" satisfied, but $A\rightarrow B$ is not a formal theorem: the hypothesis holds whenever $\not\vdash A$, and there is of course no reason why this would make $A\rightarrow B$ a theorem.
If you discharge an assumption labelled $z$ you should remember to actually label the assumption.
Also, ex falso quodlibet is not a rule of discharging; the rule to discharge $y$ is negation introduction, which needs to be followed by double negation elimination (though some do combine it into Reduction Ad Absurdum (RAA)).
$$
\dfrac{
\dfrac{
\dfrac{
\dfrac{
\lower{1.5ex}{[\neg (P \to Q)]^z} \quad
\dfrac{
\dfrac{
\dfrac{[\lnot P]^y\quad[P]^x}{\bot}{\lnot E}
}{Q}{\rm efq}
}{P\to Q}{\to I^x}
}{\bot}{\rm efq}
}{\lnot\lnot P}{\lnot I^y}
}{P}{\lnot\lnot E}
}{\neg (P \to Q) \to P}{\to I^z}
$$
This was an example in Jean Gallier's Discrete Mathematics book. I feel like I got the mechanical parts understood. Still, my head hurts when thinking about how I assumed both $P$ and $¬P$ to prove something. How do you guys understand this? How can we assume both $P$ and $¬P$, isn't that absurd?
Yes, that is how Reduction to Absurdity proofs operate: "If this assumption was true it, then what follows would be absurd, so therefore it cannot be true."
In this proof: When given $\lnot (P\to Q)$ should we also assume $\lnot P$, then we could prove $P\to Q$ (through the ex falso quodlibet subproof), which is absurd, so therefore $\lnot (P\to Q)$ entails $P$, and so we deduce $\lnot(P\to Q)\to P$.
Here's the fitch style representation which may be easier to follow.
$$\def\fitch#1#2{\quad\begin{array}{|l}#1 \\\hline #2\end{array}}\fitch{}{\fitch{~1.~\lnot(P\to Q)}{\fitch{2.~\lnot P}{\fitch{~3.~P}{~4.~\bot\hspace{14ex}\lnot e, 2,3\\~5.~Q\hspace{14ex}\text{efq},4}\\~6.~P\to Q\hspace{12ex}{\to}i,3-5\\~7.~\bot\hspace{17ex}\lnot e,1,6}\\~8.~\lnot\lnot P\hspace{18ex}\lnot i,2-7\\~9.~P\hspace{21ex}\lnot\lnot e,8}\\10.~\lnot(P\to Q)\to P\hspace{10ex}{\to}i,1-9}$$
In this notation we keep track of the order in which assumptions are raised and discharged by indentation. Here we see that a contradiction can be derived on raising the third assumption, and so we may validly derive $Q$ within that context (because whatever $Q$ may be, it is at least as true as an absurdity).
Ex falso Quodlibet: If we can say "false is true", then we may say anything is true.
Best Answer
It is called ex falso axiom.
The logic obtained from removing it is called minimal logic and is well studied. In this logic, $\bot$ act just like another atomic formula with no particular property.
In real theories we can often replace $\bot$ with an explicit formula that would play its role, e.g. in Heyting arithmetic, we can derive arbitrary formulas from $0=1$ without any need for $\bot$ or the ex falso axiom.
Troelstra and van Dalen's "Constructivism in Mathematics" has a through discussion of the logic (IIRC).