I'm a bit confused by the use of /\ and \/ weakening, I've the following exercise.

Show that $\displaystyle (P \implies Q) \implies \lnot P \models \lnot P \lor \lnot Q$

Now I can go about the lefthand part as follows:

$\displaystyle (P \implies Q) \implies \lnot P \;=\;\{\; by\; implication,\; twice\; \} \\ \lnot(\lnot P \lor Q) \lor \lnot P \;=\;\{\; by\; demorgan\; \} \\ (\lnot\lnot P \land \lnot Q) \lor \lnot P \;=\;\{\; by\; double \;negation,\; \} \\ (P \land \lnot Q) \lor \lnot P \;=\;\{\; by\; distribution,\; \}\\ (\lnot P \lor \lnot Q) \land (\lnot P \lor P) \;=\;\{\; by\; excluded \;middle\; \} \\ (\lnot P \lor \lnot Q) \land True \;=\;\{\; by\; true/false\;elimination,\; \} \\ \lnot P \lor \lnot Q \;\ \models \lnot P \lor \lnot Q$

Seems fair enough, but where I distributed the $\displaystyle \lnot P$ over $\displaystyle P$ and $\displaystyle \lnot Q$, I could've applied $\displaystyle \land$-weakening, which would've given a totally different outcome:

$\displaystyle (P \land \lnot Q) \lor \lnot P \;=\;\{\; by\; \land weakening,\; \} \\ (P \lor \lnot P) \;=\;\{\; by\; excluded \;middle,\; \} \\ True \models \lnot P \land \lnot Q$

which is a false statement.

This all seems a bit ambiguous to me, and I was under the impression we used a formal language in the hopes of getting rid of just that

Any tips on the subject? Are there more rules I should adhere to? Do I have to prioritize distribution over $\displaystyle \land$ weakening for example?

When is using weakening more appropriate? Some (links to) good examples would be excellent