∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E]
  (R : Type u_1) (L : Type u_2) [inst_4 : CommSemiring R] [inst_5 : Algebra R F] [inst_6 : Algebra R E]
  [inst_7 : Field L] [PerfectField L] [inst_9 : Algebra R L] [inst_10 : IsScalarTower R F E],
  Function.Bijective (AlgHom.restrictDomain F)