-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
h :
  Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x →
    Membership.mem (γ := Set (realSpace K))
      (Set.preimage (β := mixedSpace K) (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
              (Set.preimage (β := logSpace K) logMap
                (ZSpan.fundamentalDomain (ι := Fin (rank K))
                  (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))) ∩
            {x : realSpace K | ∀ (w : InfinitePlace K), 0 ≤ x w} ∩
          {x : realSpace K |
            Ne (α := ℝ)
              ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
                  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) :
                ℝ)
              (0 : ℝ)} ∩
        {x : realSpace K |
          LE.le (α := ℝ)
            ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
                ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) :
              ℝ)
            (1 : ℝ)})
      x
h₁ :
  Membership.mem (γ := Set (realSpace K))
      (Set.preimage (β := mixedSpace K) (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
              (Set.preimage (β := logSpace K) logMap
                (ZSpan.fundamentalDomain (ι := Fin (rank K))
                  (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))) ∩
            {x : realSpace K | ∀ (w : InfinitePlace K), 0 ≤ x w} ∩
          {x : realSpace K |
            Ne (α := ℝ)
              ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
                  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) :
                ℝ)
              (0 : ℝ)} ∩
        {x : realSpace K |
          LE.le (α := ℝ)
            ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
                ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) :
              ℝ)
            (1 : ℝ)})
      x →
    ∀
      (h₁ :
        Membership.mem (γ := Set (realSpace K))
          (Set.preimage (β := mixedSpace K) (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
            (Set.preimage (β := logSpace K) logMap
              (ZSpan.fundamentalDomain (ι := Fin (rank K))
                (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))))
          x)
      (h₂ : Membership.mem (γ := Set (realSpace K)) {x : realSpace K | ∀ (w : InfinitePlace K), 0 ≤ x w} x)
      (h₃ :
        Membership.mem (γ := Set (realSpace K))
          {x : realSpace K |
            Ne (α := ℝ)
              ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
                  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) :
                ℝ)
              (0 : ℝ)}
          x)
      (h₄ :
        Membership.mem (γ := Set (realSpace K))
          {x : realSpace K |
            LE.le (α := ℝ)
              ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
                  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) :
                ℝ)
              (1 : ℝ)}
          x),
      Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x
⊢ Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x ↔
    Membership.mem (γ := Set (realSpace K))
      (Set.preimage (β := mixedSpace K) (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
              (Set.preimage (β := logSpace K) logMap
                (ZSpan.fundamentalDomain (ι := Fin (rank K))
                  (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))) ∩
            {x : realSpace K | ∀ (w : InfinitePlace K), 0 ≤ x w} ∩
          {x : realSpace K |
            Ne (α := ℝ)
              ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
                  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) :
                ℝ)
              (0 : ℝ)} ∩
        {x : realSpace K |
          LE.le (α := ℝ)
            ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
                ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) :
              ℝ)
            (1 : ℝ)})
      x

Tactic:
refine ⟨?_, fun ⟨⟨⟨h₁, h₂⟩, h₃⟩, h₄⟩ ↦ ?_⟩