∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (x : NumberField.RingOfIntegers K),
  (NumberField.IsCMField.complexConj K) ↑x = ↑x ↔
    ∃ y, (algebraMap (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)) K) y = ↑x