∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E →ₐ[F] K), IntermediateField.comap i (perfectClosure F K) = perfectClosure F E