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