∀ {F : Type u_4} [inst : Field F] {E : Type u_5} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_6}
  [inst_3 : Field K] [inst_4 : Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K),
  (f.comp L.val).fieldRange = IntermediateField.map f L