∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K),
  NumberField.InfinitePlace.unramifiedPlacesOver L v =
    {w | (↑w).LiesOver ↑v ∧ NumberField.InfinitePlace.IsUnramified K w}