∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (g : ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (a : K),
  (InfiniteGalois.limitToAlgEquiv g).symm a = InfiniteGalois.toAlgEquivAux✝ g⁻¹ a