awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
    {x : realSpace K |
      Ne (α := ℝ)
        ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
            ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) :
          ℝ)
        (0 : ℝ)}
    (normAtAllPlaces y)
have 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)
Tactic: rwa [Set.mem_setOf_eq, ← norm_normAtAllPlaces] at h₂
Cleared hypotheses: 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₂ : ¬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)
⊢ 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)
have 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)
Tactic: rwa [Set.mem_setOf_eq, ← norm_normAtAllPlaces] at h₂
Cleared hypotheses: 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))
    {x : realSpace K |
      LE.le (α := ℝ)
        ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
            ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) :
          ℝ)
        (1 : ℝ)}
    (normAtAllPlaces y)
have 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)
Tactic: rwa [Set.mem_setOf_eq, ← norm_normAtAllPlaces] at h₃
Cleared hypotheses: 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 : ℝ)}
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)
⊢ 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)
have 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)
Tactic: rwa [Set.mem_setOf_eq, ← norm_normAtAllPlaces] at h₃
Cleared hypotheses: 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
⊢ Eq.{u_1 + 1} (α := Set (realSpace K)) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv expMap)) Set.univ
have 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
Tactic: simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_source, expMap_single,
    Set.pi_univ Set.univ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ Eq.{u_1 + 1} (α := Set (realSpace K)) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv expMap)) Set.univ
have 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
Tactic: simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_source, expMap_single,
    Set.pi_univ Set.univ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ Eq.{u_1 + 1} (α := Set (realSpace K)) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv expMap)) Set.univ
have 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
Tactic: simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_source, expMap_single,
    Set.pi_univ Set.univ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ Eq.{u_1 + 1} (α := Set (realSpace K)) (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv expMap)) Set.univ
have 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
Tactic: simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_source, expMap_single,
    Set.pi_univ Set.univ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 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)
have 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)
Tactic: simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_target, expMap_single]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_target, expMap_single]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_target, expMap_single]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : realSpace K
⊢ (↑expMap : realSpace K → realSpace K) (c • x) = (↑expMap : realSpace K → realSpace K) x ^ c
have h : ∀ (x_1 : InfinitePlace K),
  (↑expMap : realSpace K → realSpace K) (c • x) x_1 = ((↑expMap : realSpace K → realSpace K) x ^ c) x_1
Tactic: ext
-- 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 : realSpace K
⊢ (↑expMap : realSpace K → realSpace K) (x + y) =
    (↑expMap : realSpace K → realSpace K) x * (↑expMap : realSpace K → realSpace K) y
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ι : Type u_2
s : Finset ι
f : ι → realSpace K
⊢ Eq.{u_1 + 1} (α := realSpace K) ((↑expMap : realSpace K → realSpace K) (∑ i ∈ s, f i))
    (∏ i ∈ s, (↑expMap : realSpace K → realSpace K) (f i))
have 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 : ℝ)
Tactic: ext
-- 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
hx :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
⊢ 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)
have 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)
Tactic: ext
-- 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
hx :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
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)
have h : (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
    (Real.log
        ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ)
          ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
            mixedSpace K)) -
      Real.log
          ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
            ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
              mixedSpace K)) *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
  x (↑x_1 : InfinitePlace K)
Tactic: rw [logMap, normAtPlace_mixedSpaceOfRealSpace (Real.exp_nonneg _), expMap_apply, Real.log_exp,
    mul_sub, mul_inv_cancel_left₀ mult_coe_ne_zero, hx, Real.log_one, zero_mul, mul_zero, sub_zero]
-- 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
hx :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
x_1 : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ)
            ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
              mixedSpace K)) -
        Real.log
            ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
                mixedSpace K)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    x (↑x_1 : InfinitePlace K)
⊢ logMap ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x)) x_1 =
    x (↑x_1 : InfinitePlace K)
have h₁ : (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
    (Real.log ((↑expMap : realSpace K → realSpace K) x (↑x_1 : InfinitePlace K)) -
      Real.log
          ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
            ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
              mixedSpace K)) *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
  x (↑x_1 : InfinitePlace K)
Tactic: rw [logMap, normAtPlace_mixedSpaceOfRealSpace (Real.exp_nonneg _), expMap_apply, Real.log_exp,
    mul_sub, mul_inv_cancel_left₀ mult_coe_ne_zero, hx, Real.log_one, zero_mul, mul_zero, sub_zero]
-- 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
hx :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
          mixedSpace K) :
      ℝ)
    (1 : ℝ)
x_1 : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ)
            ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
              mixedSpace K)) -
        Real.log
            ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
                mixedSpace K)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    x (↑x_1 : InfinitePlace K)
h₁ :
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log ((↑expMap : realSpace K → realSpace K) x (↑x_1 : InfinitePlace K)) -
        Real.log
            ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
                mixedSpace K)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    x (↑x_1 : InfinitePlace K)
⊢ logMap ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x)) x_1 =
    x (↑x_1 : InfinitePlace K)
have h₂ : (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
    (Real.log (Real.exp ((↑(↑x_1 : InfinitePlace K).mult : ℝ)⁻¹ * x (↑x_1 : InfinitePlace K))) -
      Real.log
          ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
            ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMap : realSpace K → realSpace K) x) :
              mixedSpace K)) *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
  x (↑x_1 : InfinitePlace K)
Tactic: rw [logMap, normAtPlace_mixedSpaceOfRealSpace (Real.exp_nonneg _), expMap_apply, Real.log_exp,
    mul_sub, mul_inv_cancel_left₀ mult_coe_ne_zero, hx, Real.log_one, zero_mul, mul_zero, sub_zero]