∀ {K : Type u_1} [inst : Field K] {A : Set (NumberField.mixedEmbedding.mixedSpace K)}
  (x : NumberField.mixedEmbedding.realSpace K)
  (motive :
    (x ∈
        ⇑NumberField.mixedEmbedding.mixedSpaceOfRealSpace ⁻¹' A ∩
          Set.univ.pi fun w => if w.IsReal then Set.univ else Set.Ici 0) →
      Prop)
  (x_1 :
    x ∈
      ⇑NumberField.mixedEmbedding.mixedSpaceOfRealSpace ⁻¹' A ∩
        Set.univ.pi fun w => if w.IsReal then Set.univ else Set.Ici 0),
  (∀ (hx₁ : x ∈ ⇑NumberField.mixedEmbedding.mixedSpaceOfRealSpace ⁻¹' A)
      (hx₂ : x ∈ Set.univ.pi fun w => if w.IsReal then Set.univ else Set.Ici 0), motive ⋯) →
    motive x_1