Proof of the incompatibility of extenders in comparison lemma of mice I am studying the comparison lemma for mice from the "An Outline of Inner Model Theory" article in the handbook and I'm struggling with the subclaim in the proof. It's on page $1618$.
So let $M$ and $N$ be $k$-sound premice of size $\le \theta$, and suppose $\Sigma$ and $\Gamma$ are $(k, \theta^++1)$-iteration strategies for $M$ and $N$ respectively; then we recursively build iteration trees $T_\alpha$ and $U_\alpha$ played according to $\Sigma$ and $\Gamma$ by "iterating away the least disagreement". So suppose at each step $\alpha$ we choose the top extenders $E_{l_\alpha}^T$ and $E_{r_\alpha}^U$(where at most one of them may be $\emptyset$) to iterate the top elements of $T_\alpha$ and $U_\alpha$. And before the subclaim, the author defines the notion of compatibility for extenders in this context: Let's assume $E$ and $F$ are extenders. We say that $E$ and $F$ are compatible if and only if for some $\eta$, either $E$ is the trivial completion of $F|\eta$ or $F$ is the trivial completion of $E|\eta$. Also at this part of the proof, we assume that the we may iterate $T_\alpha$ and $U_\alpha$ up to $\theta^+$, without encountering two comparable iterates of $M$ and $N$.
Then the subclaim is that: for $\alpha, \beta <\theta^+$, $E_\alpha^T$ is incompatible with $E_\beta^U$. Now for the proof: Let $E = E_\alpha^T$ and $F = E_\beta^U$, and suppose that $E$ is the trivial completion of $F|\eta$, for some $\eta$. Let $\xi$ be such that $E$ is used at the step $T_\xi \rightarrow T_{\xi+1}$ and let $\gamma$ be such that $F$ is used at the step $T_\gamma \rightarrow T_{\gamma+1}$. Since $\text{lh}(E) \le \text{lh}(F)$ $(*)$, then $\xi \le \gamma$. But if $\xi = \gamma$, so $\text{lh}(E) = \text{lh}(F)$ and so $E=F$ $(**)$ which is impossible. Thus $\xi < \gamma$ and $\text{lh}(E) < \text{lh}(F)$. Now let $P$ and $Q$ be the last elements of $T_\gamma$ and $U_\gamma$ respectively. So $\text{lh}(E)$ is a cardinal of $P$ and $P$ agrees with $Q$ below $\text{lh}(F)$ by construction, this means that $\text{lh}(E)$ is a cardinal of $J^Q_{\text{lh}(F)}$. On the other hand the initial segment condition of the definition of a fine extender sequence implies that $E \in J^Q_{\text{lh}(F)}$ $(***)$. Now since $E$ collapses it's length in a computable way, this is a contradiction.
Now my problem is in the parts $(*)$, $(**)$ and $(***)$. What I don't understand is that:

*

*In order to get $\text{lh}(E) \le \text{lh}(F)$ in $(*)$, we either need to assume $\alpha \le \beta$, which would make the proof not symmetric w.r.t the definition of compatibility or we at least need to change the definition of compatibility as I will write below. (I think it matters over which model we want for example $E$ to be the trivial completion of $F|\eta$.)


*Also I don't know how we get $E=F$ in $(**)$. I think here we again need to assume that in the compatibility notion, the trivial completion is taken over the correct model. Also we seem to need that $\eta\ge \nu(F)$, no?


*And in $(***)$ I don't understand how we infer that fact, because I think $F|\eta$ may after all be type $Z$. Because I don't see why if $E$ isn't type $Z$, then $F|\eta$ shouldn't be as well. Because after all $F|\eta$ may compute $((\nu(F|\eta)-1)^+)^{\text{Ult}(M_2, F|\eta)}$ to be equal to $((\nu(F|\eta)-1)^+)^{\text{Ult}(M_2, F|(\nu(F|\eta)-1))}$, but $((\nu(E)-1)^+)^{\text{Ult}(M_1, E)}\neq((\nu(E)-1)^+)^{\text{Ult}(M_1, E|(\nu(E)-1))}$, where $E$ is over $M_1$ and $F$ is over $M_2$.
All in all I think by changing the definition of compatibility to: "assume $E$ and $F$ are extenders over $M_1$ and $M_2$. We say that $E$ and $F$ are compatible if and only if for some $\eta$, either $E$ is the trivial completion of $F|\eta$ over $M_2$ or $F$ is the trivial completion of $E|\eta$ over $M_1$", solves my first confusion. But how do we guarantee that we don't have type $Z$ extenders in situation $(***)$? And also don't we need $\eta\ge \nu(F)$ in case $(**)$?
I have edited my question for part $(**)$.
 A: ($*$): The fact that $\mathrm{lh}(E)\leq\mathrm{lh}(F)$ follows from $E$ being the trivial completion of $F\upharpoonright\eta$. That is, considering the definition of trivial completion I take it as implicit here that $\mathrm{OR}^M=(\kappa^+)^M\leq\eta\leq\mathrm{lh}(F)$ where $\kappa=\mathrm{crit}(E)=\mathrm{crit}(F)$ and $E,F$ are $M$-extenders and $M$ has largest cardinal $\kappa$. Let $\nu=\nu(E)=\nu(F\upharpoonright\eta)\leq\eta$. Since $\nu=\max((\kappa^+)^M,\xi)$ where $\xi$ is the strict sup of generators of $F\upharpoonright\eta$, and since $(\kappa^+)^M<\mathrm{lh}(F)$ and $F$'s generators are bounded in $\mathrm{lh}(F)$, it follows that $\eta<\mathrm{lh}(F)$. If $\eta\geq\nu(F)$ then note that $E=F$, so suppose $\eta<\nu(F)$, and let $\gamma$ be the least $F$-generator such that $\gamma\geq\nu=\nu(E)$, so $\gamma<\nu(F)$. Letting $\pi:\mathrm{Ult}(M,E)\to\mathrm{Ult}(M,F)$ be the natural factor map, we have $\mathrm{crit}(\pi)=\gamma$ is a cardinal in $\mathrm{Ult}(M,E)$. If $\gamma>\nu$ then it follows that $(\nu^+)^{\mathrm{Ult}(M,E)}\leq\gamma$ (actually one can show we have equality), so $$\mathrm{lh}(E)=(\nu^+)^{\mathrm{Ult}(M,E)}\leq(\nu(F)^+)^{\mathrm{Ult}(M,F)}=\mathrm{lh}(F)$$
(actually one can show $\mathrm{lh}(E)<\mathrm{lh}(F)$, using the ISC for $F$).
If instead $\gamma=\nu$ then note that  $$\mathcal{P}(\nu)^{\mathrm{Ult}(M,E)}\subseteq\mathcal{P}(\nu)^{\mathrm{Ult}(M,F)},$$
and therefore
$$\mathrm{lh}(E)=(\nu^+)^{\mathrm{Ult}(M,E)}\leq(\nu^+)^{\mathrm{Ult}(M,F)}\leq(\nu(F)^+)^{\mathrm{Ult}(M,F)}=\mathrm{lh}(F)$$
(again, one can actually show $\mathrm{lh}(E)<\mathrm{lh}(F)$ here).
($**$): Suppose $E\neq F$. Since $E$ is the trivial completion of $F\upharpoonright\eta$ for some $\eta$ (where as above, we have $(\kappa^+)^M\leq\eta<\mathrm{lh}(F)$), we may assume $\eta<\nu(F)$. But then since $E$ is the active extender of some premouse (because it was used in the comparison), it is not type Z, so the initial segment condition applies to it, but this gives
$E\in N|\mathrm{lh}(F)$ where $N$ is the model of $\mathcal{U}$ from which $F$ was selected in the comparison, which implies $\mathrm{lh}(E)<\mathrm{lh}(F)$, a contradiction.
($***$): $E$ is equivalent to $F\upharpoonright\eta$, since $E$ is its trivial completion. This implies they have the same generators and ultrapowers etc
(in particular, $\nu(E)=\nu(F\upharpoonright\eta)$), and since $E$ is not type Z, it follows that $F\upharpoonright\eta$ is not type Z.
