[proofplan]
We prove two facts about a formal group law $F(X, Y)$ over a ring $R$. First, we show $F(X, 0) = X$ by exploiting the associativity and unit axioms to deduce that the coefficient of each monomial $X^i$ for $i \geq 2$ in $F(X, 0) - X$ must vanish. Second, we construct the formal inverse $i(X)$ by recursively solving for its coefficients using $F(X, i(X)) = 0$, and we prove uniqueness by the same recursive structure.
[/proofplan]
[step:Show that $F(X, 0) = X$]
By the formal group axioms, $F(X, Y) \equiv X + Y \pmod{(X, Y)^2}$, so
\begin{align*}
F(X, 0) \equiv X \pmod{X^2}.
\end{align*}
Write $F(X, Y) = X + Y + \sum_{i+j \geq 2} c_{ij} X^i Y^j$. Then $F(X, 0) = X + \sum_{i \geq 2} c_{i0} X^i$. We must show $c_{i0} = 0$ for all $i \geq 2$.
The associativity axiom $F(F(X, Y), Z) = F(X, F(Y, Z))$ holds in $R[[X, Y, Z]]$. Setting $Y = Z = 0$:
\begin{align*}
F(F(X, 0), 0) = F(X, F(0, 0)) = F(X, 0),
\end{align*}
where $F(0, 0) = 0$ by the unit axiom ($F(X, Y) \equiv X + Y \pmod{(X,Y)^2}$ forces $F(0, 0) = 0$). Write $g(X) = F(X, 0)$. The equation above gives $g(g(X)) = g(X)$, i.e., $g$ is idempotent under composition. Since $g(X) \equiv X \pmod{X^2}$, the map $g$ is a formal automorphism of $R[[X]]$. An idempotent formal automorphism with $g(X) \equiv X \pmod{X^2}$ must be the identity: if $g(X) = X + a_k X^k + \cdots$ with $a_k \neq 0$ and $k \geq 2$, then $g(g(X)) = X + 2a_k X^k + \cdots$, so $g(g(X)) = g(X)$ forces $2a_k = a_k$, hence $a_k = 0$, a contradiction. Therefore $g(X) = X$, i.e., $F(X, 0) = X$.
[guided]
We know $F(X, Y) \equiv X + Y \pmod{(X, Y)^2}$, so plugging in $Y = 0$ gives $F(X, 0) = X + (\text{higher-order terms in } X)$. The question is whether any higher-order terms survive.
Write $g(X) = F(X, 0)$. By associativity of $F$, we have $F(F(X, Y), Z) = F(X, F(Y, Z))$ in $R[[X, Y, Z]]$. Setting $Y = Z = 0$ and using $F(0, 0) = 0$ (which follows from substituting $X = Y = 0$ into $F(X, Y) \equiv X + Y \pmod{(X,Y)^2}$):
\begin{align*}
g(g(X)) = F(F(X, 0), 0) = F(X, F(0, 0)) = F(X, 0) = g(X).
\end{align*}
So $g$ is idempotent under composition: $g \circ g = g$. Moreover, $g(X) \equiv X \pmod{X^2}$, so $g$ has leading coefficient $1$ and is invertible under composition (a formal power series $X + \sum_{k \geq 2} a_k X^k$ is always invertible as a composition in $R[[X]]$).
Now suppose for contradiction that $g(X) \neq X$. Let $k \geq 2$ be the smallest index with $c_{k0} \neq 0$, so $g(X) = X + c_{k0} X^k + O(X^{k+1})$. Then
\begin{align*}
g(g(X)) &= g(X) + c_{k0} (g(X))^k + O(X^{k+1}) \\
&= (X + c_{k0} X^k + \cdots) + c_{k0} (X + \cdots)^k + O(X^{k+1}) \\
&= X + 2c_{k0} X^k + O(X^{k+1}).
\end{align*}
The equation $g(g(X)) = g(X)$ then gives $2c_{k0} = c_{k0}$ at degree $k$, hence $c_{k0} = 0$, contradicting our assumption. Therefore $g(X) = X$, i.e., $F(X, 0) = X$.
By symmetry (using the commutativity axiom $F(X, Y) = F(Y, X)$), we also have $F(0, Y) = Y$.
[/guided]
[/step]
[step:Construct the formal inverse $i(X) \in X \cdot R[[X]]$ satisfying $F(X, i(X)) = 0$]
We seek $i(X) = \sum_{n \geq 1} b_n X^n \in X \cdot R[[X]]$ such that $F(X, i(X)) = 0$. Since $F(X, Y) = X + Y + \sum_{i+j \geq 2} c_{ij} X^i Y^j$ and $F(X, 0) = X$, the equation $F(X, i(X)) = 0$ becomes
\begin{align*}
X + i(X) + \sum_{i+j \geq 2} c_{ij} X^i \, i(X)^j = 0.
\end{align*}
At degree $1$: $X + b_1 X = 0$, so $b_1 = -1$.
At degree $n \geq 2$: the coefficient of $X^n$ in $X + i(X) + \sum_{i+j \geq 2} c_{ij} X^i \, i(X)^j$ takes the form
\begin{align*}
b_n + P_n(b_1, \ldots, b_{n-1}, c_{ij}) = 0,
\end{align*}
where $P_n$ is a polynomial in $b_1, \ldots, b_{n-1}$ and the constants $c_{ij}$ (the terms from $\sum c_{ij} X^i i(X)^j$ at degree $n$ involve only $b_1, \ldots, b_{n-1}$ when $j \geq 1$, since $i(X)^j$ contributes at least degree $j$, and the term $b_n$ appears only from the linear part $i(X)$). This uniquely determines $b_n = -P_n(b_1, \ldots, b_{n-1}, c_{ij})$ for each $n \geq 2$.
By induction on $n$, the coefficients $b_n$ are uniquely determined, yielding a unique power series $i(X) \in X \cdot R[[X]]$ with $F(X, i(X)) = 0$.
[guided]
We need to find $i(X) = -X + b_2 X^2 + b_3 X^3 + \cdots \in X \cdot R[[X]]$ satisfying $F(X, i(X)) = 0$. The key observation is that the equation can be solved degree by degree, and at each degree the unknown coefficient $b_n$ appears linearly with coefficient $1$.
Write $F(X, Y) = X + Y + H(X, Y)$, where $H(X, Y) = \sum_{i+j \geq 2} c_{ij} X^i Y^j$ collects all higher-order terms. The equation $F(X, i(X)) = 0$ becomes
\begin{align*}
X + i(X) + H(X, i(X)) = 0.
\end{align*}
At degree $1$: the only contributions come from $X$ and $b_1 X$ (since $H$ has no linear terms). This gives $1 + b_1 = 0$, so $b_1 = -1$.
At degree $n \geq 2$: the coefficient of $X^n$ in $i(X)$ is $b_n$. The coefficient of $X^n$ in $H(X, i(X))$ depends on $b_1, \ldots, b_{n-1}$ only, because $H$ starts at degree $2$ and any occurrence of $Y = i(X)$ at degree $n$ within a term $c_{ij} X^i Y^j$ with $i + j \geq 2$ either uses $X^i$ with $i \geq 1$ (reducing the degree available for $Y$) or uses $Y^j$ with $j \geq 2$ (which means the contribution from the highest coefficient of $Y$ is at most $b_{\lfloor n/2 \rfloor}$). More precisely, the degree-$n$ coefficient of $X^i \cdot i(X)^j$ depends only on $b_1, \ldots, b_{n-i}$ when $j = 1$, and on $b_1, \ldots, b_{n-i-j+1}$ when $j \geq 2$, so in all cases only on $b_1, \ldots, b_{n-1}$.
Therefore the equation at degree $n$ has the form $b_n = -P_n(b_1, \ldots, b_{n-1})$ for an explicit polynomial $P_n$, and each $b_n$ is uniquely determined. This recursive construction produces a unique $i(X) \in X \cdot R[[X]]$ with $F(X, i(X)) = 0$.
[/guided]
[/step]
