∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ}
  {σ₁ σ₂ : Gal(K/k)}, NumberField.ComplexEmbedding.IsConj φ σ₁ → NumberField.ComplexEmbedding.IsConj φ σ₂ → σ₁ = σ₂