awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
inl :
  ∀ (hs : 0 ≤ 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 }
inr :
  ∀ (hs : s < 0),
    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 }
⊢ 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 }

Tactic:
obtain hs | hs := le_or_gt 0 s

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
inl :
  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) //
        intNorm.{u_1} (K := K)
            (↑((idealSetEquiv K J :
                    (a : (↑(idealSet K J) : Type u_1)) →
                      (↑{a : (↑(integerSet K) : Type u_1) |
                            (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                        Type u_1))
                  a) :
              (↑(integerSet K) : Type u_1)) ≤
          ⌊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 }

Tactic:
simp_rw [← intNorm_idealSetEquiv_apply, ← Nat.le_floor_iff hs]

Premises used: Nat.le_floor_iff, NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
inl :
  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⌋₊ } ×
        ↥(Units.torsion K)) =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) //
        intNorm.{u_1} (K := K)
            (↑((idealSetEquiv K J :
                    (a : (↑(idealSet K J) : Type u_1)) →
                      (↑{a : (↑(integerSet K) : Type u_1) |
                            (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                        Type u_1))
                  a) :
              (↑(integerSet K) : Type u_1)) ≤
          ⌊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) //
        intNorm.{u_1} (K := K)
            (↑((idealSetEquiv K J :
                    (a : (↑(idealSet K J) : Type u_1)) →
                      (↑{a : (↑(integerSet K) : Type u_1) |
                            (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                        Type u_1))
                  a) :
              (↑(integerSet K) : Type u_1)) ≤
          ⌊s⌋₊ }

Tactic:
rw [torsionOrder, ← Nat.card_eq_fintype_card, ← Nat.card_prod]

Premises used: NumberField.Units.torsionOrder, Nat.card_prod, Nat.card_eq_fintype_card
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ 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⌋₊ } ×
        ↥(Units.torsion K)) =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) //
        intNorm.{u_1} (K := K)
            (↑((idealSetEquiv K J :
                    (a : (↑(idealSet K J) : Type u_1)) →
                      (↑{a : (↑(integerSet K) : Type u_1) |
                            (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                        Type u_1))
                  a) :
              (↑(integerSet K) : Type u_1)) ≤
          ⌊s⌋₊ }

Tactic:
Nat.card_congr <| @Equiv.ofFiberEquiv _ (γ := Finset.Iic ⌊s⌋₊) _
      (fun I ↦ ⟨absNorm I.1.val.1, Finset.mem_Iic.mpr I.1.prop.2.2⟩)
      (fun a ↦ ⟨intNorm (idealSetEquiv K J a.1).1, Finset.mem_Iic.mpr a.prop⟩) fun ⟨i, hi⟩ ↦ ?_

Premises used: Iff.mpr, _private.0.NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le.match_2, Ideal.absNorm, Equiv.ofFiberEquiv, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv, Finset.mem_Iic, Equiv, Subtype, Prod.fst, Subtype.mk, NumberField.mixedEmbedding.fundamentalCone.intNorm, Nat.card_congr, And.right, Subtype.prop, Subtype.val, Eq, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
x_1 : ↥(Units.torsion K)
x_2 : ↥(Ideal (𝓞 K))⁰
⊢ ((↑J : Ideal (𝓞 K)) ∣ (↑x_2 : Ideal (𝓞 K)) ∧
        IsPrincipal (↑x_2 : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑x_2 : Ideal (𝓞 K)) ≤ ⌊s⌋₊) ∧
      (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑x_2 : Ideal (𝓞 K)) = i ↔
    (↑J : Ideal (𝓞 K)) ∣ (↑x_2 : Ideal (𝓞 K)) ∧
      IsPrincipal (↑x_2 : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑x_2 : Ideal (𝓞 K)) = i

Tactic:
grind
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
simp_rw :
  { a : (↑(idealSet K J) : Type u_1) //
      intNorm.{u_1} (K := K)
          (↑((idealSetEquiv K J :
                  (a : (↑(idealSet K J) : Type u_1)) →
                    (↑{a : (↑(integerSet K) : Type u_1) |
                          (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                      Type u_1))
                a) :
            (↑(integerSet K) : Type u_1)) =
        i } ≃
    { a : (↑(idealSet K J) : Type u_1) //
      intNorm.{u_1} (K := K)
          (↑((idealSetEquiv K J :
                  (a : (↑(idealSet K J) : Type u_1)) →
                    (↑{a : (↑(integerSet K) : Type u_1) |
                          (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                      Type u_1))
                a) :
            (↑(integerSet K) : Type u_1)) =
        i }
⊢ { a : (↑(idealSet K J) : Type u_1) //
      Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑i : ℝ) : ℝ) } ≃
    { a : (↑(idealSet K J) : Type u_1) //
      intNorm.{u_1} (K := K)
          (↑((idealSetEquiv K J :
                  (a : (↑(idealSet K J) : Type u_1)) →
                    (↑{a : (↑(integerSet K) : Type u_1) |
                          (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                      Type u_1))
                a) :
            (↑(integerSet K) : Type u_1)) =
        i }

Tactic:
simp_rw [← intNorm_idealSetEquiv_apply, Nat.cast_inj]

Premises used: Nat.cast_inj, NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a : (↑(idealSet K J) : Type u_1) //
      intNorm.{u_1} (K := K)
          (↑((idealSetEquiv K J :
                  (a : (↑(idealSet K J) : Type u_1)) →
                    (↑{a : (↑(integerSet K) : Type u_1) |
                          (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                      Type u_1))
                a) :
            (↑(integerSet K) : Type u_1)) =
        i } ≃
    { a : (↑(idealSet K J) : Type u_1) //
      intNorm.{u_1} (K := K)
          (↑((idealSetEquiv K J :
                  (a : (↑(idealSet K J) : Type u_1)) →
                    (↑{a : (↑(integerSet K) : Type u_1) |
                          (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                      Type u_1))
                a) :
            (↑(integerSet K) : Type u_1)) =
        i }

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
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 }
inr₃ : 0 * torsionOrder K = 0
⊢ 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 }

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]

Premises used: lt_iff_not_ge, Nat.cast_nonneg, MulZeroClass.zero_mul, Nat.card_of_isEmpty, NumberField.mixedEmbedding.norm_nonneg, Iff.mp, and_false, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
w : InfinitePlace K
rw rw₁ : normAtAllPlaces x w = (normAtPlace w : (a : mixedSpace K) → ℝ) x
⊢ Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces x) : mixedSpace K) :
      ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)

Tactic:
rw [normAtPlace_mixedSpaceOfRealSpace (normAtPlace_nonneg w x)]

Premises used: NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ Membership.mem (γ := Set (mixedSpace K)) (normLeOne K) x ↔
    Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
      LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
Set.mem_sep_iff

Premises used: Set.Mem, setOf, Set.inter, Set.mem_sep_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurableSet (α := mixedSpace K) (normLeOne K)

Tactic:
(measurableSet_fundamentalCone K).inter <|
    measurableSet_le (mixedEmbedding.continuous_norm K).measurable measurable_const

Premises used: measurableSet_le, NumberField.mixedEmbedding.measurableSet_fundamentalCone, NumberField.mixedEmbedding.continuous_norm, Continuous.measurable, measurable_const, MeasurableSet.inter
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Set (mixedSpace K)) (normLeOne K) (normAtAllPlaces ⁻¹' normAtAllPlaces '' normLeOne K)

Tactic:
subset_antisymm (Set.subset_preimage_image _ _) ?_

Premises used: subset_antisymm, Set.subset_preimage_image
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine : Subset (α := Set (mixedSpace K)) (normAtAllPlaces ⁻¹' normAtAllPlaces '' normLeOne K) (normLeOne K)
⊢ Eq (α := Set (mixedSpace K)) (normLeOne K) (normAtAllPlaces ⁻¹' normAtAllPlaces '' normLeOne K)

Tactic:
refine subset_antisymm (Set.subset_preimage_image _ _) ?_

Premises used: subset_antisymm, Set.subset_preimage_image
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
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)
⊢ Membership.mem (γ := Set (mixedSpace K)) (normLeOne K) x

Tactic:
rw [mem_normLeOne, ← normAtAllPlaces_mem_fundamentalCone_iff, ← norm_normAtAllPlaces,
    ← mem_normLeOne] at hy₁ ⊢

Premises used: NumberField.mixedEmbedding.fundamentalCone.mem_normLeOne, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
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
rwa rwa₁ rwa₂ rwa₃ :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (normLeOne K)
    ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces y) : mixedSpace K)
⊢ Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (normLeOne K)
    ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces x) : mixedSpace K)

Tactic:
rwa [← hy₂]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
⊢ 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 : ℝ)})

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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

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

Premises used: Membership.mem, NumberField.mixedEmbedding.normAtAllPlaces, Iff.intro, Set.image, _private.0.NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne.match_1, NumberField.mixedEmbedding.fundamentalCone.normLeOne
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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)

Tactic:
⟨⟨⟨?_, ?_⟩, ?_⟩, ?_⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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)
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)
⊢ 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)

Tactic:
refine ⟨⟨⟨?_, ?_⟩, ?_⟩, ?_⟩