-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ 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
have 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
Tactic: refine ⟨?_, fun ⟨⟨⟨h₁, h₂⟩, h₃⟩, h₄⟩ ↦ ?_⟩