The first two statements are about the relation the algorithm works on; the third is about the graph, in Mathlib's terms: for a graph on $Fin V$ split at $n$, the relation between $Fin n$ and $Fin (V - n)$ is adjacency across the split, and a matching of the graph is the same thing as an injective assignment of left neighbours to right vertices, edge for edge.

The proof does not use Berge's lemma. A search from $l₀$ fails only when every right vertex reachable from $l₀$ by alternating exploration is already matched, and the left vertices so reached then outnumber the right vertices so reached by exactly one. This state is stable: a later augmentation from another free vertex keeps the reached left vertices matched, hence into the same set of right neighbours, which it therefore saturates again, so that $l₀$ reaches nothing new and stays failed. At the end the failed left vertices $F$ and the set $S$ of all left vertices reachable from them have $|N(S)| = |S| - |F|$, and any matching matches at most $|N(S)|$ vertices of $S$, so it has at most $|L| - |F|$ edges — which is the size of the matching returned, since every left vertex outside $F$ is matched.