∀ {K : Type u_1} [inst : Field K] {A : Set (NumberField.mixedEmbedding.mixedSpace K)}
  (x : NumberField.mixedEmbedding.mixedSpace K)
  (motive :
    x ∈
        NumberField.mixedEmbedding.normAtComplexPlaces ⁻¹'
          (NumberField.mixedEmbedding.normAtComplexPlaces '' NumberField.mixedEmbedding.plusPart A) →
      Prop)
  (x_1 :
    x ∈
      NumberField.mixedEmbedding.normAtComplexPlaces ⁻¹'
        (NumberField.mixedEmbedding.normAtComplexPlaces '' NumberField.mixedEmbedding.plusPart A)),
  (∀ (a : NumberField.mixedEmbedding.mixedSpace K) (ha₁ : a ∈ NumberField.mixedEmbedding.plusPart A)
      (ha₂ : NumberField.mixedEmbedding.normAtComplexPlaces a = NumberField.mixedEmbedding.normAtComplexPlaces x),
      motive ⋯) →
    motive x_1