[proofplan] We prove the inversion formula by substituting the defining expression for $g(G)$ into the proposed formula for $f(F)$. Because the lattice of flats is finite, the resulting double sum may be rearranged without any convergence issue. The coefficient of each $f(H)$ is then an interval sum of the Möbius function, and the needed right-sided Möbius identity follows directly from the defining recursion of the Möbius function. This leaves only the coefficient of $f(F)$ equal to $1$, while every lower flat has coefficient $0$. [/proofplan]

[step:Establish the right-sided Möbius cancellation identity]For flats $H,F \in L(M)$ with $H \leq F$, define the finite interval \begin{align*} [H,F] := \{G \in L(M) : H \leq G \leq F\}. \end{align*} We claim that the interval sum equals $1$ when $H=F$ and equals $0$ when $H<F$. If $H=F$, then $[F,F]=\{F\}$ and $\mu(F,F)=1$, so the identity holds. Suppose $H<F$. By the definition of the Möbius function of a finite poset, we use the right-sided defining recursion on the interval $[H,F]$: the normalization is $\mu(F,F)=1$, and for $H<F$, \begin{align*} \mu(H,F)=-\sum_{G \in [H,F]\setminus\{H\}} \mu(G,F). \end{align*} This recursion gives \begin{align*} \sum_{G \in [H,F]} \mu(G,F)=\mu(H,F)+\sum_{G \in [H,F]\setminus\{H\}} \mu(G,F)=0. \end{align*} Thus the claimed cancellation identity holds for every interval $[H,F]$.[/step]

[guided]Fix flats $H,F \in L(M)$ with $H \leq F$. The interval from $H$ to $F$ is the finite set \begin{align*} [H,F] := \{G \in L(M) : H \leq G \leq F\}. \end{align*} We want to compute the coefficient that will later appear in front of $f(H)$, namely \begin{align*} \sum_{G \in [H,F]} \mu(G,F). \end{align*} There are two cases. If $H=F$, then the interval contains only $F$, and the defining normalization of the Möbius function gives $\mu(F,F)=1$. Therefore \begin{align*} \sum_{G \in [F,F]} \mu(G,F)=\mu(F,F)=1. \end{align*} Now assume $H<F$. By the definition of the Möbius function of a finite poset, we use the right-sided defining recursion on the interval $[H,F]$: \begin{align*} \mu(H,F)=-\sum_{G \in [H,F]\setminus\{H\}} \mu(G,F). \end{align*} This formula is exactly the statement that the Möbius function cancels the constant zeta function on every nontrivial interval. Substituting this expression for $\mu(H,F)$ into the full interval sum gives \begin{align*} \sum_{G \in [H,F]} \mu(G,F)=\mu(H,F)+\sum_{G \in [H,F]\setminus\{H\}} \mu(G,F). \end{align*} Using the recursion, the right-hand side becomes \begin{align*} -\sum_{G \in [H,F]\setminus\{H\}} \mu(G,F)+\sum_{G \in [H,F]\setminus\{H\}} \mu(G,F)=0. \end{align*} Hence the interval sum equals $1$ when $H=F$ and equals $0$ when $H<F$. This is the cancellation identity that will remove every term except $f(F)$ in the final sum.[/guided]

[step:Substitute the summation formula for $g$ and rearrange the finite sums] Fix a flat $F \in L(M)$. For an integer $n \in \mathbb{Z}$ and an element $a \in A$, let $n a \in A$ denote the usual integer multiple in the additive abelian group $A$. Finite distributivity of integer multiplication over addition in $A$ will be used when regrouping the sums. Define \begin{align*} S_F := \sum_{G \leq F} \mu(G,F) g(G) \in A. \end{align*} Using the hypothesis on $g(G)$ for each flat $G \leq F$, we obtain \begin{align*} S_F=\sum_{G \leq F} \mu(G,F)\sum_{H \leq G} f(H). \end{align*} Since $L(M)$ is finite, all sums are finite. Using associativity and commutativity in the abelian group $A$, together with distributivity of integer multiples over finite sums, we may regroup the terms by the flat $H$. The pairs being summed are precisely the pairs $(H,G)$ satisfying $H \leq G \leq F$. Therefore \begin{align*} S_F=\sum_{H \leq F}\left(\sum_{G \in [H,F]} \mu(G,F)\right)f(H). \end{align*} [/step]

[step:Use Möbius cancellation to isolate the term $f(F)$] By the cancellation identity proved above, for each flat $H \leq F$, the coefficient \begin{align*} \sum_{G \in [H,F]} \mu(G,F) \end{align*} equals $1$ when $H=F$ and equals $0$ when $H<F$. Substituting this coefficient computation into the regrouped expression for $S_F$ gives \begin{align*} S_F=1\cdot f(F)+\sum_{H<F}0\cdot f(H)=f(F). \end{align*} Thus \begin{align*} \sum_{G \leq F} \mu(G,F)g(G)=f(F). \end{align*} Since $F \in L(M)$ was arbitrary, the inversion formula holds for every flat $F \in L(M)$. [/step]