-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
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) : ℝ)⁻¹)
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) : ℝ)⁻¹)
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 (α := ℝ) (β := ℝ)
              ((↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑ζ : 𝓞 K) : 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) : ℝ)⁻¹)
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 (α := ℝ) (β := ℝ) ((↑1 : ℝ) : ℝ) ((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
          (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 (α := ℝ) (β := ℝ) (1 : ℝ) ((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
          (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 ((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
          (HMul.hMul (α := ℝ) (β := ℝ)
            (((↑x_1 : InfinitePlace K) : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑ζ : 𝓞 K) : K) : ℝ)
            ((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
          (HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ)
            ((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

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]

Premises used: NumberField.mixedEmbedding.norm_eq_norm, NumberField.Units.norm, NumberField.Units.mem_torsion, map_mul, NumberField.mixedEmbedding.unitSMul_smul, NumberField.mixedEmbedding.normAtPlace_apply, NumberField.mixedEmbedding.logMap_apply, Iff.mp, one_mul, Rat.cast_one