awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
rw :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
rw₁ :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log 1 * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
⊢ logMap x w =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
have rw₂ : (↑(↑w : InfinitePlace K).mult : ℝ) *
    (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
      HMul.hMul (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)⁻¹) =
  (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
Tactic: rw [logMap_apply, hx, Real.log_one, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
rw :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
rw₁ :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log 1 * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
rw₂ :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        HMul.hMul (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
⊢ logMap x w =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
have rw₃ : (↑(↑w : InfinitePlace K).mult : ℝ) * (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) - 0) =
  (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
Tactic: rw [logMap_apply, hx, Real.log_one, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
rw :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
rw₁ :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log 1 * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
rw₂ :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        HMul.hMul (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
rw₃ :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) - 0) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
⊢ logMap x w =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
have rw₄ : (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) =
  (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
Tactic: rw [logMap_apply, hx, Real.log_one, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : (𝓞 K)ˣ
⊢ Eq.{u_1 + 1} (α := logSpace K)
    (logMap ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K))))
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ))
have h : ∀ (x : { w : InfinitePlace K // w ≠ w₀ }),
  logMap ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K))) x =
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ Ne (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K) :
      ℝ)
    (0 : ℝ)
have rw : Ne (α := ℝ) 1 0
Tactic: rw [norm_unit]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ logMap (u • x) =
    HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
        logSpace K)
      (logMap x)
have rw : logMap
    (HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K)
      x) =
  HAdd.hAdd (α := logSpace K) (β := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
      logSpace K)
    (logMap x)
Tactic: rw [unitSMul_smul, logMap_mul (by rw [norm_unit]; norm_num) hx, logMap_eq_logEmbedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
rw :
  logMap
      (HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K)
        x) =
    HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
        logSpace K)
      (logMap x)
⊢ logMap (u • x) =
    HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
        logSpace K)
      (logMap x)
have rw₁ : HAdd.hAdd (α := logSpace K)
    (logMap ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K))))
    (logMap x) =
  HAdd.hAdd (α := logSpace K) (β := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
      logSpace K)
    (logMap x)
Tactic: rw [unitSMul_smul, logMap_mul (by rw [norm_unit]; norm_num) hx, logMap_eq_logEmbedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
rw :
  logMap
      (HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K)
        x) =
    HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
        logSpace K)
      (logMap x)
rw₁ :
  HAdd.hAdd (α := logSpace K)
      (logMap ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K))))
      (logMap x) =
    HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
        logSpace K)
      (logMap x)
⊢ logMap (u • x) =
    HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
        logSpace K)
      (logMap x)
have rw₂ : HAdd.hAdd (α := logSpace K) (β := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
      logSpace K)
    (logMap x) =
  HAdd.hAdd (α := logSpace K) (β := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
      logSpace K)
    (logMap x)
Tactic: rw [unitSMul_smul, logMap_mul (by rw [norm_unit]; norm_num) hx, logMap_eq_logEmbedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
⊢ Eq (α := logSpace K) (logMap (ζ • x)) (logMap x)
have h : ∀ (x_1 : { w : InfinitePlace K // w ≠ w₀ }), logMap (ζ • x) x_1 = logMap x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
x_1 : { w : InfinitePlace K // w ≠ w₀ }
⊢ logMap (ζ • x) x_1 = logMap x x_1
have h : (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
    (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) (ζ • x)) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (ζ • x)) * (↑(finrank ℚ K) : ℝ)⁻¹) =
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
    (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹)
Tactic: simp_rw [logMap_apply, unitSMul_smul, map_mul, norm_eq_norm, Units.norm, Rat.cast_one, one_mul,
    normAtPlace_apply, (mem_torsion K).mp hζ, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
x_1 : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) (ζ • x)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (ζ • x)) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹)
⊢ logMap (ζ • x) x_1 = logMap x x_1
have h₁ : (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
    (Real.log
        ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ)
          (HMul.hMul (α := mixedSpace K)
            ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑ζ : 𝓞 K)) :
              mixedSpace K)
            x)) -
      Real.log
          ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
            (HMul.hMul (α := mixedSpace K)
              ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑ζ : 𝓞 K)) :
                mixedSpace K)
              x)) *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
    (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹)
Tactic: simp_rw [logMap_apply, unitSMul_smul, map_mul, norm_eq_norm, Units.norm, Rat.cast_one, one_mul,
    normAtPlace_apply, (mem_torsion K).mp hζ, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
x_1 : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) (ζ • x)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (ζ • x)) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹)
h₁ :
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ)
            (HMul.hMul (α := mixedSpace K)
              ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑ζ : 𝓞 K)) :
                mixedSpace K)
              x)) -
        Real.log
            ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              (HMul.hMul (α := mixedSpace K)
                ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑ζ : 𝓞 K)) :
                  mixedSpace K)
                x)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹)
⊢ logMap (ζ • x) x_1 = logMap x x_1
have h₂ : (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
    (Real.log
        (HMul.hMul (α := ℝ) (β := ℝ)
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ)
              ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑ζ : 𝓞 K)) :
                mixedSpace K) :
            ℝ)
          ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ)) -
      Real.log
          (HMul.hMul (α := ℝ) (β := ℝ)
            ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
                ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑ζ : 𝓞 K)) :
                  mixedSpace K) :
              ℝ)
            ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)) *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
    (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹)
Tactic: simp_rw [logMap_apply, unitSMul_smul, map_mul, norm_eq_norm, Units.norm, Rat.cast_one, one_mul,
    normAtPlace_apply, (mem_torsion K).mp hζ, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
⊢ Eq (α := logSpace K) (logMap (HSMul.hSMul (β := mixedSpace K) c 1)) 0
have h : ∀ (x : { w : InfinitePlace K // w ≠ w₀ }), logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h : (↑(↑x : InfinitePlace K).mult : ℝ) *
    (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
  0 x
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₁ : (↑(↑x : InfinitePlace K).mult : ℝ) *
    (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
  0 x
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₂ : (↑(↑x : InfinitePlace K).mult : ℝ) *
    (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
      Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
  0 x
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₃ : (↑(↑x : InfinitePlace K).mult : ℝ) *
    (Real.log (|c| * 1) -
      Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
        (↑(finrank ℚ K) : ℝ)⁻¹) =
  0 x
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₄ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log (|c| * 1) - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) =
  0 x
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]