∀ (K : Type u_1) [inst : Field K] [NumberField K],
  Function.Bijective fun c =>
    Sum.casesOn (motive := fun t => c = t → K →+* ℂ) c (fun w h => (↑w).embedding)
      (fun wj h =>
        Prod.casesOn wj fun w j =>
          if j = 0 then (↑w).embedding else NumberField.ComplexEmbedding.conjugate (↑w).embedding)
      ⋯