I have the following proof of a little lemma and I want to know if it is clear in its structure and if it actually provides the claimed results.
$\mathcal K$ is an abstract simplicial complex.
Let $\tau, \sigma \in \mathcal K$ such that the following two conditions are satisfied:
1) $\tau \subset \sigma$, in particular dim $\tau<$ dim $\sigma$.
2) $\sigma$ is a maximal face of $\mathcal K$ and no other maximal face of $\mathcal K$ contains $\tau$.
Then $\tau$ is called a free face. A simplicial collapse of $\mathcal K$ is the removal of all simplices $\gamma$ such that $\tau \subseteq \gamma \subseteq \sigma$, where $\tau$ is a free face. If additionally we have dim $\tau = $ dim $\sigma-1$, then this is called an elementary collapse. An elementary collapse at $\tau$ is a dim$(\tau)-$collapse.
A simplicial complex $\mathcal K$ collapses to a simplicial complex $\mathcal L$ if there is a sequence of simplicial complexes $\mathcal K = \mathcal K_0 \searrow \mathcal K_1 \searrow \cdots \searrow \mathcal K_q = \mathcal L$ such that $\mathcal K_{i+1}$ is obtained from $\mathcal K_i$ by a collapse at $\tau_i$. In this case, we call $C = (\tau_o, \tau_1,\cdots,\tau_{q-1})$ a $(\mathcal K,\mathcal L)$ collapsing sequence and write $\mathcal K \searrow^C \mathcal L$. A simplicial complex is called collapsible if it collapses to a single vertex.
A collapsing sequence $C$ is monotone if $i < j$ imply $\text{dim}(\sigma_i) \geq \text{dim}(\sigma_j)$. In this case, if $\mathcal K \searrow \mathcal L$, we say that $\mathcal K$ monotonically collapses to $\mathcal L$.
Now I want to prove that: If $\mathcal K$ collapses to $\mathcal L$, then $\mathcal K$ monotonically collapses to $\mathcal L$.
This is my proof: Consider a collapse sequence $C=(\tau_0, \tau_i,\cdots,\tau_n)$. Starting form $C$ we can construct explicitly a monotone collapse sequence $C'$ by specifying at each step how to choose a new simplex $\tau'$. Denote by $d$ the dimension of $\mathcal K$. We describe the construction with respect to dimension $d$, and as $d$ decreases we cover the entire sequence. Let $\tau \in C$ and $\sigma$ the unique maximal face containing it. Only the following cases are possible:
1) $\text{dim}(\tau) = d-1, \text{dim}(\sigma)=d \Rightarrow \tau'=\tau$;
2) $\text{dim}(\tau) < d-1, \text{dim}(\sigma)=d \Rightarrow \tau'=\gamma$ with $\gamma$ such that $\gamma \supset \sigma$, $\text{dim}(\gamma)=d-1$. $\gamma$ is free since $\gamma \supset \tau$ and $\tau$ is free. For a simplex there exists a monotonically collapse sequence. Collapse all simplicies $\delta \supset \sigma$ of dimension $\text{dim}(\delta)$ at the beginning of step $d = \text{dim}(\delta)$, following the order in which we have found at this step.
3) $\text{dim}(\tau) < d$. Collapse $\tau$ at the beginning of step $d = \text{dim}(\tau)$, following the order in which we have found at this step.
At step $d$, all the simplicies $\tau'$ have dimension $d$. In addition, in 2) we have removed a maximal face of dimension $d$ and in 3) such a face is not present at all; at step $d$ only of the faces of dimension $d$ can prevent us to continue with collapses, thus we can actually swap 3) and remove only $\gamma$ in 2). At the beginning of every successive step we first collapse the simplicies from point 2) and 3). Finally, if $\text{dim}(\tau)=d'<d$ at step $d$, then at step $d'$, $\tau$, satisfy condition 1) of above.
Please comment for suggestions or improvements in the explanation
As written, your proof seems unclear to me. Perhaps there is some kind of induction going on, but I am not clear on that point, because I do not see a clearly formulated induction proof, in particular I do not see a clearly stated induction hypothesis.
If you were doing an induction, I would have expected that you are using it to construct a collapsing sequence $C' = (\tau'_0,\tau'_1,...,\tau'_n)$ from $\mathcal K$ to $\mathcal L$, and I would have expected an induction hypothesis describing the properties of an initial subsequence $(\tau'_0,\tau'_1,...,\tau'_{j-1})$ and of the corresponding sequence $\mathcal K = \mathcal K'_0 \searrow \mathcal K'_1 \searrow \cdots \searrow \mathcal K'_j$; presumably "monotonicity" would be part of the induction hypothesis.
In carrying out the induction step, you would then be required to prove the existence of a free face $\tau'_j$ of $\mathcal K'_j$ such that the maximal simplex $\sigma'_j$ of $\mathcal K'_j$ that contains $\tau'_j$ has dimension equal to the dimension of $\mathcal K'_j$.
In particular, at the point where you say "Let $\tau \in C$ and $\sigma$ the unique maximal face containing $\tau$", I cannot tell at all where in the induction you are and what role $\tau$ will play in the induction step. What if $\tau$ has already been removed by the time you get to $\mathcal K'_i$? What if $\tau$ has not been removed yet and is not a free face of $\mathcal K'_i$?
My question in the comments was aimed at these issues. If, as you say in your comment, $\tau=\tau_i$ for some $i$, and if $\sigma_i$ is the unique maximal face of $\mathcal K_i$ that contains $\tau_i$, and if $\tau_i = \tau'_j$ is also the free face of some $\mathcal K'_j$ that you intend to collapse in the induction step, then it is not at all clear that the maximal simplex of $\mathcal K'_j$ that contains $\tau_i$ is equal to the maximal simplex of $\mathcal K_i$ that contains $\tau_i$, nor that it even has the same dimension.