∀ {F : Type u_1} {E : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {M : Type u_5} {N : Type u_6}
  [inst_3 : Field N] [inst_4 : Field M] [inst_5 : Algebra M N] [Algebra.IsAlgebraic F E] [h : IsGalois F E]
  {f : F ≃+* M} {g : E ≃+* N}, (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E) → IsGalois M N