awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : s < 0
inr :
  Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ // (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧ IsPrincipal (↑I : Ideal (𝓞 K)) ∧ False } *
      torsionOrder K =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
⊢ Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ //
          (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
            IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } *
      torsionOrder K =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
have inr₁ : Nat.card.{u_1}
      { I : ↥(Ideal (𝓞 K))⁰ // (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧ IsPrincipal (↑I : Ideal (𝓞 K)) ∧ False } *
    torsionOrder K =
  Nat.card.{u_1} { a : (↑(idealSet K J) : Type u_1) // False }
Tactic: simp_rw [lt_iff_not_ge.mp (lt_of_lt_of_le hs (Nat.cast_nonneg _)), lt_iff_not_ge.mp
      (lt_of_lt_of_le hs (mixedEmbedding.norm_nonneg _)), and_false, Nat.card_of_isEmpty,
      zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : s < 0
inr :
  Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ // (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧ IsPrincipal (↑I : Ideal (𝓞 K)) ∧ False } *
      torsionOrder K =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
inr₁ :
  Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ // (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧ IsPrincipal (↑I : Ideal (𝓞 K)) ∧ False } *
      torsionOrder K =
    Nat.card.{u_1} { a : (↑(idealSet K J) : Type u_1) // False }
⊢ Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ //
          (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
            IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } *
      torsionOrder K =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
have inr₂ : Nat.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // False } * torsionOrder K =
  Nat.card.{u_1} { a : (↑(idealSet K J) : Type u_1) // False }
Tactic: simp_rw [lt_iff_not_ge.mp (lt_of_lt_of_le hs (Nat.cast_nonneg _)), lt_iff_not_ge.mp
      (lt_of_lt_of_le hs (mixedEmbedding.norm_nonneg _)), and_false, Nat.card_of_isEmpty,
      zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : s < 0
inr :
  Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ // (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧ IsPrincipal (↑I : Ideal (𝓞 K)) ∧ False } *
      torsionOrder K =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
inr₁ :
  Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ // (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧ IsPrincipal (↑I : Ideal (𝓞 K)) ∧ False } *
      torsionOrder K =
    Nat.card.{u_1} { a : (↑(idealSet K J) : Type u_1) // False }
inr₂ :
  Nat.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // False } * torsionOrder K =
    Nat.card.{u_1} { a : (↑(idealSet K J) : Type u_1) // False }
⊢ Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ //
          (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
            IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } *
      torsionOrder K =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
have inr₃ : 0 * torsionOrder K = 0
Tactic: simp_rw [lt_iff_not_ge.mp (lt_of_lt_of_le hs (Nat.cast_nonneg _)), lt_iff_not_ge.mp
      (lt_of_lt_of_le hs (mixedEmbedding.norm_nonneg _)), and_false, Nat.card_of_isEmpty,
      zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
w : InfinitePlace K
⊢ Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces x) : mixedSpace K) :
      ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
have rw : normAtAllPlaces x w = (normAtPlace w : (a : mixedSpace K) → ℝ) x
Tactic: rw [normAtPlace_mixedSpaceOfRealSpace (normAtPlace_nonneg w x)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Set (mixedSpace K)) (normLeOne K) (normAtAllPlaces ⁻¹' normAtAllPlaces '' normLeOne K)
have refine : Subset (α := Set (mixedSpace K)) (normAtAllPlaces ⁻¹' normAtAllPlaces '' normLeOne K) (normLeOne K)
Tactic: refine subset_antisymm (Set.subset_preimage_image _ _) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hy₁ : Membership.mem (γ := Set (mixedSpace K)) (normLeOne K) y
hy₂ : normAtAllPlaces y = normAtAllPlaces x
⊢ Membership.mem (γ := Set (mixedSpace K)) (normLeOne K) x
have rw : ∀
  (hy₁ :
    Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (normLeOne K)
      ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces y) : mixedSpace K))
  (hy₂ : normAtAllPlaces y = normAtAllPlaces x),
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (normLeOne K)
    ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces x) : mixedSpace K)
Tactic: rw [mem_normLeOne, ← normAtAllPlaces_mem_fundamentalCone_iff, ← norm_normAtAllPlaces,
    ← mem_normLeOne] at hy₁ ⊢
Cleared hypotheses: hy₁, hy₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Set (realSpace K)) (normAtAllPlaces '' normLeOne 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 : ℝ)})
have h : ∀ (x : realSpace K),
  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: ext x
-- 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
⊢ 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)) (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₄⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
y : mixedSpace K
h₃ :
  Membership.mem (γ := Set (mixedSpace K))
    {x : mixedSpace K | LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)} y
h₁ :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    y
h₂ : y ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
⊢ 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 : ℝ)})
    (normAtAllPlaces y)
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)))))
  (normAtAllPlaces y)
Tactic: refine ⟨⟨⟨?_, ?_⟩, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
y : mixedSpace K
h₃ :
  Membership.mem (γ := Set (mixedSpace K))
    {x : mixedSpace K | LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)} y
h₁ :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    y
h₂ : y ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
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)))))
    (normAtAllPlaces y)
⊢ 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 : ℝ)})
    (normAtAllPlaces y)
have h₄ : Membership.mem (γ := Set (realSpace K)) {x : realSpace K | ∀ (w : InfinitePlace K), 0 ≤ x w} (normAtAllPlaces y)
Tactic: refine ⟨⟨⟨?_, ?_⟩, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
y : mixedSpace K
h₃ :
  Membership.mem (γ := Set (mixedSpace K))
    {x : mixedSpace K | LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)} y
h₁ :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    y
h₂ : y ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
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)))))
    (normAtAllPlaces y)
h₄ : Membership.mem (γ := Set (realSpace K)) {x : realSpace K | ∀ (w : InfinitePlace K), 0 ≤ x w} (normAtAllPlaces y)
⊢ 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 : ℝ)})
    (normAtAllPlaces y)
have 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 : ℝ)}
  (normAtAllPlaces y)
Tactic: refine ⟨⟨⟨?_, ?_⟩, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
y : mixedSpace K
h₃ :
  Membership.mem (γ := Set (mixedSpace K))
    {x : mixedSpace K | LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)} y
h₁ :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    y
h₂ : y ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
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)))))
    (normAtAllPlaces y)
h₄ : Membership.mem (γ := Set (realSpace K)) {x : realSpace K | ∀ (w : InfinitePlace K), 0 ≤ x w} (normAtAllPlaces y)
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 : ℝ)}
    (normAtAllPlaces y)
⊢ 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 : ℝ)})
    (normAtAllPlaces y)
have 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 : ℝ)}
  (normAtAllPlaces y)
Tactic: refine ⟨⟨⟨?_, ?_⟩, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
y : mixedSpace K
h₃ :
  Membership.mem (γ := Set (mixedSpace K))
    {x : mixedSpace K | LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)} y
h₁ :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    y
h₂ : y ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
⊢ 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)))))
    (normAtAllPlaces y)
have h : ∀
  (h₁ :
    Membership.mem (γ := Set (logSpace K))
      (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
      (logMap y))
  (h₂ : y ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}),
  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)))))
    (normAtAllPlaces y)
Tactic: rwa [Set.mem_preimage, ← logMap_normAtAllPlaces] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
y : mixedSpace K
h₃ :
  Membership.mem (γ := Set (mixedSpace K))
    {x : mixedSpace K | LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)} y
h₁ :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    y
h₂ : y ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
h :
  ∀
    (h₁ :
      Membership.mem (γ := Set (logSpace K))
        (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
        (logMap y))
    (h₂ : y ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}),
    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)))))
      (normAtAllPlaces y)
⊢ 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)))))
    (normAtAllPlaces y)
have h₄ : ∀
  (h₁ :
    Membership.mem (γ := Set (logSpace K))
      (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
      (logMap ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces y))))
  (h₂ : y ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}),
  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)))))
    (normAtAllPlaces y)
Tactic: rwa [Set.mem_preimage, ← logMap_normAtAllPlaces] at h₁
Cleared hypotheses: h₁, h₂