[proofplan] We fix an arbitrary $\sigma \in \operatorname{Gal}(L/K)$ and lift it to the automorphism $\tau \in \operatorname{Gal}(M/K)$ that maximises $i_{M/K}(\tau)$ among all lifts of $\sigma$. The core of the proof is the pointwise identity $i_{M/K}(\tau g) = \min(i_{M/L}(g),\, i_{M/K}(\tau))$ for all $g \in H$, which we establish using the ultrametric inequality on $\mathcal{O}_M = \mathcal{O}_K[\alpha]$ and the maximality of $\tau$. From this identity, we derive $i_{L/K}(\sigma) - 1 = \eta_{M/L}(i_{M/K}(\tau) - 1)$ by expanding both sides via the averaging formula for $i_{L/K}$ and the integral definition of $\eta_{M/L}$. The theorem then follows from the chain of equivalences: $\sigma \in G_s(M/K)H/H$ iff $i_{M/K}(\tau) - 1 \geq s$ iff $i_{L/K}(\sigma) - 1 \geq \eta_{M/L}(s) = t$ iff $\sigma \in G_t(L/K)$. [/proofplan]

[step:Choose a lift $\tau$ of $\sigma$ that maximises $i_{M/K}(\tau)$] Let $\sigma \in \operatorname{Gal}(L/K)$. The coset of lifts of $\sigma$ to $\operatorname{Gal}(M/K)$ is $\{\tau g : g \in H\}$ for any single lift $\tau$. Since $H = \operatorname{Gal}(M/L)$ is finite, we may choose $\tau$ in this coset so that \begin{align*} i_{M/K}(\tau) = \max_{g \in H} i_{M/K}(\tau g). \end{align*} Fix such a $\tau$ for the remainder of the proof. Let $\alpha \in \mathcal{O}_M$ be a generator of the extension $M/K$, so that $\mathcal{O}_M = \mathcal{O}_K[\alpha]$. [/step]

[step:Establish the pointwise identity $i_{M/K}(\tau g) = \min(i_{M/L}(g),\, i_{M/K}(\tau))$ for all $g \in H$]Recall that for any $\rho \in \operatorname{Gal}(M/K) \setminus \{\operatorname{id}\}$, the index $i_{M/K}(\rho)$ is defined by \begin{align*} i_{M/K}(\rho) = v_M(\rho(\alpha) - \alpha), \end{align*} where $v_M$ is the normalised valuation on $M$ and $\mathcal{O}_M = \mathcal{O}_K[\alpha]$. **Lower bound.** Write $\tau g(\alpha) - \alpha = (\tau g(\alpha) - \tau(\alpha)) + (\tau(\alpha) - \alpha)$. Since $\tau$ is an isometry of $M$ (it preserves $v_M$), we have \begin{align*} v_M(\tau g(\alpha) - \tau(\alpha)) = v_M(g(\alpha) - \alpha) = i_{M/K}(g). \end{align*} Note that for $g \in H = \operatorname{Gal}(M/L)$, the element $g$ fixes $L$ pointwise, and in particular $g$ fixes $\mathcal{O}_L$. Since $\mathcal{O}_L = \mathcal{O}_K[\alpha] \cap L$, we have $i_{M/K}(g) = i_{M/L}(g)$ when $g \neq \operatorname{id}$ (the indices computed via $\alpha$ agree because $\mathcal{O}_M = \mathcal{O}_K[\alpha]$ and the valuation is the same). By the ultrametric inequality on $v_M$: \begin{align*} i_{M/K}(\tau g) = v_M(\tau g(\alpha) - \alpha) \geq \min(v_M(\tau g(\alpha) - \tau(\alpha)),\, v_M(\tau(\alpha) - \alpha)) = \min(i_{M/L}(g),\, i_{M/K}(\tau)). \end{align*} When $g = \operatorname{id}$, we have $\tau g = \tau$ and $i_{M/L}(\operatorname{id}) = +\infty$ by convention, so $\min(+\infty, i_{M/K}(\tau)) = i_{M/K}(\tau) = i_{M/K}(\tau g)$, and the identity holds. **Upper bound and case analysis for $g \neq \operatorname{id}$.** From the maximality of $\tau$: \begin{align*} i_{M/K}(\tau) \geq i_{M/K}(\tau g). \end{align*} *Case 1: $i_{M/L}(g) \geq i_{M/K}(\tau)$.* The lower bound gives $i_{M/K}(\tau g) \geq \min(i_{M/L}(g), i_{M/K}(\tau)) = i_{M/K}(\tau)$. Combined with the upper bound $i_{M/K}(\tau g) \leq i_{M/K}(\tau)$, we get $i_{M/K}(\tau g) = i_{M/K}(\tau) = \min(i_{M/L}(g), i_{M/K}(\tau))$. *Case 2: $i_{M/L}(g) < i_{M/K}(\tau)$.* The two terms in $\tau g(\alpha) - \alpha = (\tau g(\alpha) - \tau(\alpha)) + (\tau(\alpha) - \alpha)$ have valuations $i_{M/L}(g)$ and $i_{M/K}(\tau)$, which are distinct. By the ultrametric equality for terms of different valuation (the [Isosceles Triangle Principle](/theorems/???)), the valuation of the sum equals the minimum: \begin{align*} i_{M/K}(\tau g) = v_M(\tau g(\alpha) - \alpha) = \min(i_{M/L}(g),\, i_{M/K}(\tau)) = i_{M/L}(g). \end{align*} In both cases, $i_{M/K}(\tau g) = \min(i_{M/L}(g),\, i_{M/K}(\tau))$.[/step]

[guided]The heart of Herbrand's theorem is this pointwise identity. The strategy is to decompose $\tau g(\alpha) - \alpha$ into two pieces — one measuring $g$ and one measuring $\tau$ — and use ultrametric arithmetic to determine the valuation of the sum. Write $\tau g(\alpha) - \alpha = (\tau g(\alpha) - \tau(\alpha)) + (\tau(\alpha) - \alpha)$. Since $\tau$ is an automorphism of $M$ preserving the valuation $v_M$, the first term has valuation \begin{align*} v_M(\tau g(\alpha) - \tau(\alpha)) = v_M(\tau(g(\alpha) - \alpha)) = v_M(g(\alpha) - \alpha) = i_{M/L}(g), \end{align*} and the second term has valuation $v_M(\tau(\alpha) - \alpha) = i_{M/K}(\tau)$. The ultrametric inequality gives the lower bound $i_{M/K}(\tau g) \geq \min(i_{M/L}(g), i_{M/K}(\tau))$. The upper bound $i_{M/K}(\tau g) \leq i_{M/K}(\tau)$ is the maximality hypothesis on $\tau$. Now we split into cases. If $i_{M/L}(g) \geq i_{M/K}(\tau)$, both the lower and upper bounds equal $i_{M/K}(\tau)$, so $i_{M/K}(\tau g) = i_{M/K}(\tau) = \min(i_{M/L}(g), i_{M/K}(\tau))$. If $i_{M/L}(g) < i_{M/K}(\tau)$, the two terms have *distinct* valuations. The Isosceles Triangle Principle in non-archimedean valued fields states: if $|x| \neq |y|$, then $|x + y| = \max(|x|, |y|)$. Equivalently, for valuations, if $v(a) \neq v(b)$, then $v(a + b) = \min(v(a), v(b))$. Applying this with $a = \tau g(\alpha) - \tau(\alpha)$ (valuation $i_{M/L}(g)$) and $b = \tau(\alpha) - \alpha$ (valuation $i_{M/K}(\tau) > i_{M/L}(g)$), the valuation of the sum is $i_{M/L}(g)$, which equals $\min(i_{M/L}(g), i_{M/K}(\tau))$. Why is the maximality hypothesis essential? Without it, we would have no upper bound on $i_{M/K}(\tau g)$ in Case 1. Different lifts of $\sigma$ give different values of $i_{M/K}(\tau g)$, and the identity holds only for the *maximal* lift.[/guided]

[step:Derive the averaging identity $i_{L/K}(\sigma) - 1 = \eta_{M/L}(i_{M/K}(\tau) - 1)$] The index $i_{L/K}(\sigma)$ for $\sigma \in \operatorname{Gal}(L/K)$ can be computed via the averaging formula: \begin{align*} i_{L/K}(\sigma) = \frac{1}{e_{M/L}} \sum_{g \in H} i_{M/K}(\tau g), \end{align*} where $e_{M/L} = |H_0| = |G_0(M/L)|$ is the ramification index of $M/L$, and $\tau$ is any lift of $\sigma$ (the value is independent of the choice of lift). Applying the pointwise identity from the previous step: \begin{align*} i_{L/K}(\sigma) = \frac{1}{e_{M/L}} \sum_{g \in H} \min(i_{M/L}(g),\, i_{M/K}(\tau)). \end{align*} The Herbrand function $\eta_{M/L}$ is defined by \begin{align*} \eta_{M/L}(s) = \frac{1}{e_{M/L}} \sum_{g \in H} \min(i_{M/L}(g),\, s + 1) - 1. \end{align*} Substituting $s = i_{M/K}(\tau) - 1$: \begin{align*} \eta_{M/L}(i_{M/K}(\tau) - 1) &= \frac{1}{e_{M/L}} \sum_{g \in H} \min(i_{M/L}(g),\, i_{M/K}(\tau)) - 1. \end{align*} Comparing with the formula for $i_{L/K}(\sigma)$: \begin{align*} i_{L/K}(\sigma) = \eta_{M/L}(i_{M/K}(\tau) - 1) + 1, \end{align*} which gives the desired identity $i_{L/K}(\sigma) - 1 = \eta_{M/L}(i_{M/K}(\tau) - 1)$. [/step]

[step:Conclude the theorem via a chain of equivalences]Set $t = \eta_{M/L}(s)$. For $\sigma \in \operatorname{Gal}(L/K)$ with maximal lift $\tau$, the following equivalences hold: \begin{align*} \sigma \in \frac{G_s(M/K) \cdot H}{H} &\iff \text{some lift of } \sigma \text{ lies in } G_s(M/K) \\ &\iff i_{M/K}(\tau) - 1 \geq s \quad \text{(since } \tau \text{ is the lift maximising } i_{M/K}\text{)} \\ &\iff \eta_{M/L}(i_{M/K}(\tau) - 1) \geq \eta_{M/L}(s) \quad \text{(since } \eta_{M/L} \text{ is non-decreasing)} \\ &\iff i_{L/K}(\sigma) - 1 \geq t \\ &\iff \sigma \in G_t(L/K). \end{align*} The second equivalence uses the maximality of $\tau$: $\sigma$ has *some* lift in $G_s(M/K)$ if and only if the lift with the largest $i_{M/K}$-value lies in $G_s(M/K)$. The third equivalence uses that $\eta_{M/L}$ is a non-decreasing piecewise-linear function (it is a non-negative linear combination of $\min$ terms). The fourth equivalence is the identity from the previous step. Since this holds for every $\sigma \in \operatorname{Gal}(L/K)$, we conclude \begin{align*} \frac{G_s(M/K) \cdot H}{H} = G_t(L/K), \end{align*} where $t = \eta_{M/L}(s)$. The isomorphism form follows from the second isomorphism theorem: $G_s(M/K) \cdot H / H \cong G_s(M/K) / (G_s(M/K) \cap H) = G_s(M/K) / G_s(M/L)$, since $G_s(M/K) \cap H = G_s(M/L)$ by definition of the lower numbering ramification groups.[/step]

[guided]The chain of equivalences translates the condition "$\sigma$ belongs to the image of $G_s(M/K)$ in $\operatorname{Gal}(L/K)$" into the condition "$\sigma \in G_t(L/K)$" via the Herbrand function. Let us verify each step carefully. **First equivalence.** By definition, $G_s(M/K) \cdot H / H$ consists of cosets $\tau' H$ where $\tau' \in G_s(M/K)$. An element $\sigma \in \operatorname{Gal}(L/K)$ lies in this quotient if and only if it has at least one lift $\tau'$ with $i_{M/K}(\tau') - 1 \geq s$. **Second equivalence.** Among all lifts of $\sigma$, the one maximising $i_{M/K}$ is $\tau$ (by construction). If $\tau \in G_s(M/K)$, then $\sigma$ has a lift in $G_s(M/K)$. Conversely, if some lift $\tau g \in G_s(M/K)$, then $i_{M/K}(\tau g) - 1 \geq s$, and by maximality $i_{M/K}(\tau) \geq i_{M/K}(\tau g)$, so $i_{M/K}(\tau) - 1 \geq s$ as well. **Third equivalence.** The function $\eta_{M/L}$ is non-decreasing because it is defined as $\eta_{M/L}(s) = \frac{1}{e_{M/L}} \sum_{g \in H} \min(i_{M/L}(g), s + 1) - 1$, and $\min(i_{M/L}(g), s + 1)$ is non-decreasing in $s$ for each $g$. Therefore $i_{M/K}(\tau) - 1 \geq s$ implies $\eta_{M/L}(i_{M/K}(\tau) - 1) \geq \eta_{M/L}(s)$. For the converse, if $i_{M/K}(\tau) - 1 < s$, then $\eta_{M/L}(i_{M/K}(\tau) - 1) < \eta_{M/L}(s)$ because $\eta_{M/L}$ is strictly increasing on any interval where at least one ramification break is not yet reached (in fact $\eta_{M/L}$ is piecewise linear with positive slopes on $[-1, \infty)$). **Fourth equivalence.** This is exactly the identity $i_{L/K}(\sigma) - 1 = \eta_{M/L}(i_{M/K}(\tau) - 1)$ proved in the previous step. The isomorphism form $G_t(L/K) \cong G_s(M/K) / G_s(M/L)$ follows from the second isomorphism theorem for groups: $G_s(M/K) \cdot H / H \cong G_s(M/K) / (G_s(M/K) \cap H)$. Since $H = \operatorname{Gal}(M/L)$ and the lower numbering is defined intrinsically on $\operatorname{Gal}(M/K)$, an element $g \in H$ lies in $G_s(M/K)$ if and only if $i_{M/K}(g) - 1 \geq s$, which for $g \in H$ is equivalent to $i_{M/L}(g) - 1 \geq s$, i.e., $g \in G_s(M/L)$. Therefore $G_s(M/K) \cap H = G_s(M/L)$.[/guided]