∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (x x_1 : K),
  (NumberField.IsCMField.complexConj K) (x + x_1) =
    (NumberField.IsCMField.complexConj K) x + (NumberField.IsCMField.complexConj K) x_1