∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : IntermediateField F E}
  {S : Set E} (h : K ≤ IntermediateField.adjoin F S),
  IntermediateField.extendScalars h = IntermediateField.adjoin (↥K) S