∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E]
  (L : Type u_2) [inst_4 : CommRing L] [IsReduced L], Function.Injective fun f => f.comp (algebraMap F E)