∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) (v : NumberField.InfinitePlace K) [(↑w).LiesOver ↑v],
  w.embedding.comp (algebraMap K L) = v.embedding ∨
    (NumberField.ComplexEmbedding.conjugate w.embedding).comp (algebraMap K L) = v.embedding