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
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)
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)
⊢ 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 : ℝ) *
    ((↑(↑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]
-- 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)
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)
h₃ :
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      ((↑(↑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)
⊢ 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 : ℝ) * ((↑(↑x_1 : InfinitePlace K).mult : ℝ)⁻¹ * x (↑x_1 : InfinitePlace K)) -
    (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (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 : K
hx : x ≠ 0
⊢ ∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w =
    Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)
have simp_rw : ∑ w : InfinitePlace K,
    (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
      (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w =
  Real.log (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
Tactic: simp_rw [← prod_eq_abs_norm, Real.log_prod (fun _ _ ↦ pow_ne_zero _ ((map_ne_zero _).mpr hx)),
    Real.log_pow, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
hx : x ≠ 0
simp_rw :
  ∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w =
    Real.log (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
⊢ ∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w =
    Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)
have simp_rw₁ : Eq (α := ℝ)
  (∑ w : InfinitePlace K,
    (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
      (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w)
  (∑ i : InfinitePlace K, Real.log (HPow.hPow (α := ℝ) ((i : (a : K) → ℝ) x : ℝ) i.mult))
Tactic: simp_rw [← prod_eq_abs_norm, Real.log_prod (fun _ _ ↦ pow_ne_zero _ ((map_ne_zero _).mpr hx)),
    Real.log_pow, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
hx : x ≠ 0
simp_rw :
  ∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w =
    Real.log (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
simp_rw₁ :
  Eq (α := ℝ)
    (∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w)
    (∑ i : InfinitePlace K, Real.log (HPow.hPow (α := ℝ) ((i : (a : K) → ℝ) x : ℝ) i.mult))
⊢ ∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w =
    Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)
have simp_rw₂ : Eq (α := ℝ)
  (∑ w : InfinitePlace K,
    (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
      (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w)
  (∑ x_1 : InfinitePlace K, (↑x_1.mult : ℝ) * Real.log ((x_1 : (a : K) → ℝ) x))
Tactic: simp_rw [← prod_eq_abs_norm, Real.log_prod (fun _ _ ↦ pow_ne_zero _ ((map_ne_zero _).mpr hx)),
    Real.log_pow, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
hx : x ≠ 0
simp_rw :
  ∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w =
    Real.log (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
simp_rw₁ :
  Eq (α := ℝ)
    (∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w)
    (∑ i : InfinitePlace K, Real.log (HPow.hPow (α := ℝ) ((i : (a : K) → ℝ) x : ℝ) i.mult))
simp_rw₂ :
  Eq (α := ℝ)
    (∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w)
    (∑ x_1 : InfinitePlace K, (↑x_1.mult : ℝ) * Real.log ((x_1 : (a : K) → ℝ) x))
⊢ ∑ w : InfinitePlace K,
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w =
    Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)
have simp_rw₃ : Eq (α := ℝ)
  (∑ x_1 : InfinitePlace K,
    (↑x_1.mult : ℝ) * Real.log (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x) x_1))
  (∑ x_1 : InfinitePlace K, (↑x_1.mult : ℝ) * Real.log ((x_1 : (a : K) → ℝ) x))
Tactic: simp_rw [← prod_eq_abs_norm, Real.log_prod (fun _ _ ↦ pow_ne_zero _ ((map_ne_zero _).mpr hx)),
    Real.log_pow, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Fintype.card (Fin (rank K)) = Fintype.card.{u_1} { w : InfinitePlace K // w ≠ w₀ }
have rw : Fintype.card (Fin (rank K)) =
  Fintype.card.{u_1} (InfinitePlace K) - Fintype.card.{u_1} { x : InfinitePlace K // x = w₀ }
Tactic: rw [Fintype.card_subtype_compl, Fintype.card_ofSubsingleton, Fintype.card_fin, rank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Fintype.card (Fin (rank K)) =
    Fintype.card.{u_1} (InfinitePlace K) - Fintype.card.{u_1} { x : InfinitePlace K // x = w₀ }
⊢ Fintype.card (Fin (rank K)) = Fintype.card.{u_1} { w : InfinitePlace K // w ≠ w₀ }
have rw₁ : Fintype.card (Fin (rank K)) = Fintype.card.{u_1} (InfinitePlace K) - 1
Tactic: rw [Fintype.card_subtype_compl, Fintype.card_ofSubsingleton, Fintype.card_fin, rank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Fintype.card (Fin (rank K)) =
    Fintype.card.{u_1} (InfinitePlace K) - Fintype.card.{u_1} { x : InfinitePlace K // x = w₀ }
rw₁ : Fintype.card (Fin (rank K)) = Fintype.card.{u_1} (InfinitePlace K) - 1
⊢ Fintype.card (Fin (rank K)) = Fintype.card.{u_1} { w : InfinitePlace K // w ≠ w₀ }
have rw₂ : rank K = Fintype.card.{u_1} (InfinitePlace K) - 1
Tactic: rw [Fintype.card_subtype_compl, Fintype.card_ofSubsingleton, Fintype.card_fin, rank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Fintype.card (Fin (rank K)) =
    Fintype.card.{u_1} (InfinitePlace K) - Fintype.card.{u_1} { x : InfinitePlace K // x = w₀ }
rw₁ : Fintype.card (Fin (rank K)) = Fintype.card.{u_1} (InfinitePlace K) - 1
rw₂ : rank K = Fintype.card.{u_1} (InfinitePlace K) - 1
⊢ Fintype.card (Fin (rank K)) = Fintype.card.{u_1} { w : InfinitePlace K // w ≠ w₀ }
have rw₃ : Fintype.card.{u_1} (InfinitePlace K) - 1 = Fintype.card.{u_1} (InfinitePlace K) - 1
Tactic: rw [Fintype.card_subtype_compl, Fintype.card_ofSubsingleton, Fintype.card_fin, rank]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x x_1 : realSpace K
x_2 : { w : InfinitePlace K // w ≠ w₀ }
⊢ (x + x_1) (↑x_2 : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x_2 : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, (x + x_1) w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    HAdd.hAdd (α := { w : InfinitePlace K // w ≠ w₀ } → ℝ) (β := { w : InfinitePlace K // w ≠ w₀ } → ℝ)
      (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        x (↑w : InfinitePlace K) -
          HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, x w') * (↑(finrank ℚ K) : ℝ)⁻¹)
      (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        x_1 (↑w : InfinitePlace K) -
          HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, x_1 w') *
            (↑(finrank ℚ K) : ℝ)⁻¹)
      x_2
have simp : x (↑x_2 : InfinitePlace K) + x_1 (↑x_2 : InfinitePlace K) -
    (↑(↑x_2 : InfinitePlace K).mult : ℝ) *
        HAdd.hAdd (α := ℝ) (∑ x_3 : InfinitePlace K, x x_3) (∑ x : InfinitePlace K, x_1 x) *
      (↑(finrank ℚ K) : ℝ)⁻¹ =
  x (↑x_2 : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x_2 : InfinitePlace K).mult : ℝ) (∑ x_3 : InfinitePlace K, x x_3) *
        (↑(finrank ℚ K) : ℝ)⁻¹ +
    (x_1 (↑x_2 : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x_2 : InfinitePlace K).mult : ℝ) (∑ x : InfinitePlace K, x_1 x) * (↑(finrank ℚ K) : ℝ)⁻¹)
Tactic: simp [sum_add_distrib]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : ℝ
x_1 : realSpace K
x_2 : { w : InfinitePlace K // w ≠ w₀ }
⊢ (x • x_1) (↑x_2 : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x_2 : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, (x • x_1) w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    HSMul.hSMul (α := ℝ) (β := { w : InfinitePlace K // w ≠ w₀ } → ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) x : ℝ)
      (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        x_1 (↑w : InfinitePlace K) -
          HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, x_1 w') *
            (↑(finrank ℚ K) : ℝ)⁻¹)
      x_2
have simp : x * x_1 (↑x_2 : InfinitePlace K) -
    (↑(↑x_2 : InfinitePlace K).mult : ℝ) * (x * ∑ i : InfinitePlace K, x_1 i) * (↑(finrank ℚ K) : ℝ)⁻¹ =
  x *
    (x_1 (↑x_2 : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x_2 : InfinitePlace K).mult : ℝ) (∑ i : InfinitePlace K, x_1 i) * (↑(finrank ℚ K) : ℝ)⁻¹)
Tactic: simp [← mul_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
hx : x ≠ 0
⊢ Eq.{u_1 + 1} (α := { w : InfinitePlace K // w ≠ w₀ } → ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ)
        ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
          (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x))) :
      { w : InfinitePlace K // w ≠ w₀ } → ℝ)
    (logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) : logSpace K)
have h : ∀ (w : { w : InfinitePlace K // w ≠ w₀ }),
  (realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)))
      w =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
Tactic: ext w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
hx : x ≠ 0
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ (realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)))
      w =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
have h : HSub.hSub (α := ℝ)
    ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) (↑w : InfinitePlace K) :
      ℝ)
    (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)
        (∑ w' : InfinitePlace K,
          (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
            (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w') *
      (↑(finrank ℚ K) : ℝ)⁻¹) =
  logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
Tactic: simp_rw [realSpaceToLogSpace_apply, sum_expMap_symm_apply hx, expMap_symm_apply,
    logMap, normAtPlace_apply, mul_sub, mul_assoc, norm_eq_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
hx : x ≠ 0
w : { w : InfinitePlace K // w ≠ w₀ }
h :
  HSub.hSub (α := ℝ)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
          (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) (↑w : InfinitePlace K) :
        ℝ)
      (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)
          (∑ w' : InfinitePlace K,
            (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
              (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w') *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
⊢ (realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)))
      w =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
have h₁ : HSub.hSub (α := ℝ)
    ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) (↑w : InfinitePlace K) :
      ℝ)
    ((↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹) =
  logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
Tactic: simp_rw [realSpaceToLogSpace_apply, sum_expMap_symm_apply hx, expMap_symm_apply,
    logMap, normAtPlace_apply, mul_sub, mul_assoc, norm_eq_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
hx : x ≠ 0
w : { w : InfinitePlace K // w ≠ w₀ }
h :
  HSub.hSub (α := ℝ)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
          (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) (↑w : InfinitePlace K) :
        ℝ)
      (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)
          (∑ w' : InfinitePlace K,
            (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
              (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w') *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
h₁ :
  HSub.hSub (α := ℝ)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
          (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) (↑w : InfinitePlace K) :
        ℝ)
      ((↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
⊢ (realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)))
      w =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
have h₂ : (↑(↑w : InfinitePlace K).mult : ℝ) *
      Real.log (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x) (↑w : InfinitePlace K)) -
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹ =
  logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
Tactic: simp_rw [realSpaceToLogSpace_apply, sum_expMap_symm_apply hx, expMap_symm_apply,
    logMap, normAtPlace_apply, mul_sub, mul_assoc, norm_eq_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
hx : x ≠ 0
w : { w : InfinitePlace K // w ≠ w₀ }
h :
  HSub.hSub (α := ℝ)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
          (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) (↑w : InfinitePlace K) :
        ℝ)
      (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)
          (∑ w' : InfinitePlace K,
            (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
              (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) w') *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
h₁ :
  HSub.hSub (α := ℝ)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
          (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)) (↑w : InfinitePlace K) :
        ℝ)
      ((↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
h₂ :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
        Real.log (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x) (↑w : InfinitePlace K)) -
      (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹ =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
⊢ (realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x)))
      w =
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) x) w
have h₃ : (↑(↑w : InfinitePlace K).mult : ℝ) *
      Real.log (normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x) (↑w : InfinitePlace K)) -
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹ =
  (↑(↑w : InfinitePlace K).mult : ℝ) *
    (Real.log
        ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ)
          ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K)) -
      Real.log
          ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
            ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K)) *
        (↑(finrank ℚ K) : ℝ)⁻¹)
Tactic: simp_rw [realSpaceToLogSpace_apply, sum_expMap_symm_apply hx, expMap_symm_apply,
    logMap, normAtPlace_apply, mul_sub, mul_assoc, norm_eq_norm]