I worked on the Galois theory needed in the formalization of the Odd Order Theorem. I wanted to check to see if I had this lemma. It's been over a decade but I think I found it: https://github.com/math-comp/math-comp/blob/84cb21e7bb853041...

    Lemma gal_conjg K E x : 'Gal(E / K) :^ x = 'Gal(E / x @: K).

This says for intermediate fields K and E (within some ambient separable (finite dimensional) field extension L / F), 'Gal(E / K), the group of automorphisms of E that fix K†, conjugated by (written as :^ ) x‡ is equal to 'Gal(E / x @: K),the group of automorphisms of E that fix x @: K which denotes x(K).

The fields E K and F in this proof correspond to the fields L M and K from the article; 'Gal(E / X) corresponds to X* from the article; and of course x corresponds to τ from the article.

†) technically that fix E ∩ K since our notation doesn't technically assume that K ≤ E.

‡) I believe by type inference x must be something we can conjugate the group by, and thus is must be a generic automorphism of E, i.e. an F-automorphism of E.