∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B : IntermediateField F E)
  {L : Type v} [inst_3 : Field L] [inst_4 : Algebra F L] (f : L →ₐ[F] E),
  B ≤ f.fieldRange → (IntermediateField.comap f A).relrank (IntermediateField.comap f B) = A.relrank B