∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A : Subfield E) (f : L →+* E) (B : Subfield L),
  Cardinal.lift.{v, w} ((Subfield.comap f A).relrank B) = Cardinal.lift.{w, v} (A.relrank (Subfield.map f B))