∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (φ : K →+* ℂ),
  NumberField.ComplexEmbedding.IsConj φ (NumberField.IsCMField.complexConj K)