awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀
    (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)
h₄ h₅ h₆ 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)
⊢ 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₁

Premises used: Set.mem_preimage, NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces
-- 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)) {x : realSpace K | ∀ (w : InfinitePlace K), 0 ≤ x w} (normAtAllPlaces y)

Tactic:
fun w ↦ normAtPlace_nonneg w y

Premises used: Set.Mem, setOf, NumberField.mixedEmbedding.normAtPlace_nonneg
-- 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)) {x : realSpace K | ∀ (w : InfinitePlace K), 0 ≤ x w} (normAtAllPlaces y)

Tactic:
exact fun w ↦ normAtPlace_nonneg w y

Premises used: NumberField.mixedEmbedding.normAtPlace_nonneg
-- 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 :
  ∀ (h₂ : ¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)),
    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₄ h₅ h₆ h₇ :
  ∀
    (h₂ :
      ¬Eq (α := ℝ)
          ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces y) : mixedSpace K) :
            ℝ)
          (0 : ℝ)),
    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))
    {x : realSpace K |
      Ne (α := ℝ)
        ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
            ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) :
          ℝ)
        (0 : ℝ)}
    (normAtAllPlaces y)

Tactic:
rwa [Set.mem_setOf_eq, ← norm_normAtAllPlaces] at h₂

Premises used: Set.mem_setOf_eq, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces
-- 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 :
  ∀ (h₃ : LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y : ℝ) (1 : ℝ))
    (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))
      {x : realSpace K |
        LE.le (α := ℝ)
          ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) :
            ℝ)
          (1 : ℝ)}
      (normAtAllPlaces y)
h₄ h₅ h₆ h₇ :
  ∀
    (h₃ :
      LE.le (α := ℝ)
        ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
            ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces y) : mixedSpace K) :
          ℝ)
        (1 : ℝ))
    (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))
      {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))
    {x : realSpace K |
      LE.le (α := ℝ)
        ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
            ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) :
          ℝ)
        (1 : ℝ)}
    (normAtAllPlaces y)

Tactic:
rwa [Set.mem_setOf_eq, ← norm_normAtAllPlaces] at h₃

Premises used: Set.mem_setOf_eq, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces
-- 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))
    (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:
⟨mixedSpaceOfRealSpace x, ⟨⟨h₁, h₃⟩, h₄⟩, normAtAllPlaces_mixedSpaceOfRealSpace h₂⟩

Premises used: Set.Mem, setOf, NumberField.mixedEmbedding.mixedSpaceOfRealSpace, And.intro, Exists.intro, Set.image, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, DFunLike.coe
-- 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))
    (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:
exact ⟨mixedSpaceOfRealSpace x, ⟨⟨h₁, h₃⟩, h₄⟩, normAtAllPlaces_mixedSpaceOfRealSpace h₂⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : ℝ
h : Membership.mem (γ := Set ℝ) Set.univ x
⊢ (↑w.mult : ℝ) * Real.log (Real.exp ((↑w.mult : ℝ)⁻¹ * x)) = x

Tactic:
simp only [Real.log_exp, mul_inv_cancel_left₀ mult_coe_ne_zero]

Premises used: mul_inv_cancel_left₀, Real.log_exp, NumberField.InfinitePlace.mult_coe_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : ℝ
h : Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
⊢ Real.exp ((↑w.mult : ℝ)⁻¹ * ((↑w.mult : ℝ) * Real.log x)) = x

Tactic:
simp only [inv_mul_cancel_left₀ mult_coe_ne_zero, Real.exp_log h]

Premises used: inv_mul_cancel_left₀, Real.exp_log, NumberField.InfinitePlace.mult_coe_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ Subset (α := Set ℝ) (Set.Ioi 0) {0}ᶜ

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : ℝ
⊢ HasDerivAt (↑(expMap_single w) : ℝ → ℝ) (deriv_expMap_single w x) x

Tactic:
simpa [expMap_single, mul_comm] using
    (HasDerivAt.comp x (Real.hasDerivAt_exp _) (hasDerivAt_mul_const (w.mult : ℝ)⁻¹))

Premises used: NumberField.InfinitePlace.mult, HasDerivAt.comp, NumberField.mixedEmbedding.fundamentalCone.expMap_single, Nat.cast, Inv.inv, mul_comm, Real.hasDerivAt_exp, hasDerivAt_mul_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
simp_rw :
  Eq.{u_1 + 1} (α := Set (realSpace K))
    (PartialEquiv.source (β := realSpace K)
      (OpenPartialHomeomorph.toPartialEquiv
        (OpenPartialHomeomorph.pi (X := fun (a : InfinitePlace K) ↦ ℝ) (Y := fun (a : InfinitePlace K) ↦ ℝ)
          fun (w : InfinitePlace K) ↦ expMap_single w)))
    Set.univ
simp_rw₁ :
  Eq.{u_1 + 1} (α := Set (realSpace K))
    (PartialEquiv.source (β := realSpace K)
      (PartialEquiv.pi (αi := fun (a : InfinitePlace K) ↦ ℝ) (βi := fun (a : InfinitePlace K) ↦ ℝ)
        fun (i : InfinitePlace K) ↦ (expMap_single i).toPartialEquiv))
    Set.univ
simp_rw₂ :
  Eq.{u_1 + 1} (α := Set (realSpace K))
    (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (i : InfinitePlace K) ↦ (expMap_single i).source) Set.univ
simp_rw₃ :
  Eq.{u_1 + 1} (α := Set (realSpace K))
    (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (i : InfinitePlace K) ↦ Set.univ) Set.univ
⊢ Eq.{u_1 + 1} (α := Set (realSpace K)) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv expMap)) Set.univ

Tactic:
simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_source, expMap_single,
    Set.pi_univ Set.univ]

Premises used: Set.univ, NumberField.mixedEmbedding.fundamentalCone.expMap_single, OpenPartialHomeomorph.pi_toPartialEquiv, NumberField.mixedEmbedding.fundamentalCone.expMap, PartialEquiv.pi_source, Set.pi_univ
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
simp_rw :
  Eq.{u_1 + 1} (α := Set (realSpace K))
    (PartialEquiv.target (α := realSpace K)
      (OpenPartialHomeomorph.toPartialEquiv
        (OpenPartialHomeomorph.pi (X := fun (a : InfinitePlace K) ↦ ℝ) (Y := fun (a : InfinitePlace K) ↦ ℝ)
          fun (w : InfinitePlace K) ↦ expMap_single w)))
    (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (x : InfinitePlace K) ↦ Set.Ioi 0)
simp_rw₁ :
  Eq.{u_1 + 1} (α := Set (realSpace K))
    (PartialEquiv.target (α := realSpace K)
      (PartialEquiv.pi (αi := fun (a : InfinitePlace K) ↦ ℝ) (βi := fun (a : InfinitePlace K) ↦ ℝ)
        fun (i : InfinitePlace K) ↦ (expMap_single i).toPartialEquiv))
    (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (x : InfinitePlace K) ↦ Set.Ioi 0)
simp_rw₂ :
  Eq.{u_1 + 1} (α := Set (realSpace K))
    (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (i : InfinitePlace K) ↦ (expMap_single i).target)
    (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (x : InfinitePlace K) ↦ Set.Ioi 0)
⊢ Eq.{u_1 + 1} (α := Set (realSpace K)) (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv expMap))
    (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (x : InfinitePlace K) ↦ Set.Ioi 0)

Tactic:
simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_target, expMap_single]

Premises used: PartialEquiv.pi_target, NumberField.mixedEmbedding.fundamentalCone.expMap_single, OpenPartialHomeomorph.pi_toPartialEquiv, NumberField.mixedEmbedding.fundamentalCone.expMap
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := realSpace K) (↑expMap : realSpace K → realSpace K)

Tactic:
Set.injOn_univ.1 (expMap_source K ▸ expMap.injOn)

Premises used: Eq.rec, NumberField.mixedEmbedding.fundamentalCone.expMap, OpenPartialHomeomorph.injOn, NumberField.mixedEmbedding.fundamentalCone.expMap_source, Iff.mp, Set.injOn_univ
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Continuous.{u_1, u_1} (X := realSpace K) (↑expMap : realSpace K → realSpace K)

Tactic:
continuousOn_univ.mp <| (expMap_source K) ▸ expMap.continuousOn

Premises used: Eq.rec, NumberField.mixedEmbedding.fundamentalCone.expMap, OpenPartialHomeomorph.continuousOn, NumberField.mixedEmbedding.fundamentalCone.expMap_source, Iff.mp, continuousOn_univ
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
w : InfinitePlace K
⊢ (↑expMap : realSpace K → realSpace K) x w = Real.exp ((↑w.mult : ℝ)⁻¹ * x w)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', Pi.map, Real.exp, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
w : InfinitePlace K
⊢ 0 < (↑expMap : realSpace K → realSpace K) x w

Tactic:
Real.exp_pos _

Premises used: OpenPartialHomeomorph.toFun', Pi.map, Real.exp, Real.exp_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : realSpace K
h :
  ∀ (x_1 : InfinitePlace K),
    (↑expMap : realSpace K → realSpace K) (c • x) x_1 = ((↑expMap : realSpace K → realSpace K) x ^ c) x_1
⊢ (↑expMap : realSpace K → realSpace K) (c • x) = (↑expMap : realSpace K → realSpace K) x ^ c

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : realSpace K
x_1 : InfinitePlace K
⊢ (↑expMap : realSpace K → realSpace K) (c • x) x_1 = ((↑expMap : realSpace K → realSpace K) x ^ c) x_1

Tactic:
simp [mul_comm c _, ← mul_assoc, Real.exp_mul]

Premises used: Real.exp_mul, mul_assoc, mul_comm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : realSpace K
h :
  ∀ (x_1 : InfinitePlace K),
    (↑expMap : realSpace K → realSpace K) (x + y) x_1 =
      ((↑expMap : realSpace K → realSpace K) x * (↑expMap : realSpace K → realSpace K) y) x_1
⊢ (↑expMap : realSpace K → realSpace K) (x + y) =
    (↑expMap : realSpace K → realSpace K) x * (↑expMap : realSpace K → realSpace K) y

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : realSpace K
x_1 : InfinitePlace K
⊢ (↑expMap : realSpace K → realSpace K) (x + y) x_1 =
    ((↑expMap : realSpace K → realSpace K) x * (↑expMap : realSpace K → realSpace K) y) x_1

Tactic:
simp [mul_add, Real.exp_add]

Premises used: mul_add, Real.exp_add
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ι : Type u_2
s : Finset ι
f : ι → realSpace K
h :
  ∀ (x : InfinitePlace K),
    Eq (α := ℝ) ((↑expMap : realSpace K → realSpace K) (∑ i ∈ s, f i) x : ℝ)
      ((∏ i ∈ s, (↑expMap : realSpace K → realSpace K) (f i)) x : ℝ)
⊢ Eq.{u_1 + 1} (α := realSpace K) ((↑expMap : realSpace K → realSpace K) (∑ i ∈ s, f i))
    (∏ i ∈ s, (↑expMap : realSpace K → realSpace K) (f i))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ι : Type u_2
s : Finset ι
f : ι → realSpace K
x : InfinitePlace K
⊢ Eq (α := ℝ) ((↑expMap : realSpace K → realSpace K) (∑ i ∈ s, f i) x : ℝ)
    ((∏ i ∈ s, (↑expMap : realSpace K → realSpace K) (f i)) x : ℝ)

Tactic:
simp [← Real.exp_sum, ← mul_sum]

Premises used: Finset.mul_sum, Real.exp_sum
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
w : InfinitePlace K
⊢ (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K) x w = (↑w.mult : ℝ) * Real.log (x w)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', Pi.map, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
h :
  ∀ (x_1 : { w : InfinitePlace K // w ≠ w₀ }),
    logMap ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x)) x_1 =
      x (↑x_1 : InfinitePlace K)
⊢ Eq.{u_1 + 1} (α := logSpace K)
    (logMap ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x)))
    fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ x (↑w : InfinitePlace K)

Tactic:
ext