∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K)
  (motive :
    x ∈
        ⇑NumberField.mixedEmbedding.mixedSpaceOfRealSpace ⁻¹'
                (NumberField.mixedEmbedding.logMap ⁻¹'
                  ZSpan.fundamentalDomain
                    (Module.Basis.ofZLatticeBasis ℝ (NumberField.Units.unitLattice K)
                      (NumberField.Units.basisUnitLattice K))) ∩
              {x | ∀ (w : NumberField.InfinitePlace K), 0 ≤ x w} ∩
            {x | NumberField.mixedEmbedding.norm (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x) ≠ 0} ∩
          {x | NumberField.mixedEmbedding.norm (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x) ≤ 1} →
      Prop)
  (x_1 :
    x ∈
      ⇑NumberField.mixedEmbedding.mixedSpaceOfRealSpace ⁻¹'
              (NumberField.mixedEmbedding.logMap ⁻¹'
                ZSpan.fundamentalDomain
                  (Module.Basis.ofZLatticeBasis ℝ (NumberField.Units.unitLattice K)
                    (NumberField.Units.basisUnitLattice K))) ∩
            {x | ∀ (w : NumberField.InfinitePlace K), 0 ≤ x w} ∩
          {x | NumberField.mixedEmbedding.norm (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x) ≠ 0} ∩
        {x | NumberField.mixedEmbedding.norm (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x) ≤ 1}),
  (∀
      (h₁ :
        x ∈
          ⇑NumberField.mixedEmbedding.mixedSpaceOfRealSpace ⁻¹'
            (NumberField.mixedEmbedding.logMap ⁻¹'
              ZSpan.fundamentalDomain
                (Module.Basis.ofZLatticeBasis ℝ (NumberField.Units.unitLattice K)
                  (NumberField.Units.basisUnitLattice K))))
      (h₂ : x ∈ {x | ∀ (w : NumberField.InfinitePlace K), 0 ≤ x w})
      (h₃ : x ∈ {x | NumberField.mixedEmbedding.norm (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x) ≠ 0})
      (h₄ : x ∈ {x | NumberField.mixedEmbedding.norm (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x) ≤ 1}),
      motive ⋯) →
    motive x_1