∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {F E E' : IntermediateField K L} (h : F ≤ E) (h' : F ≤ E'),
  IntermediateField.extendScalars h ≤ IntermediateField.extendScalars h' ↔ E ≤ E'