-- 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) : ℝ)⁻¹)
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) : ℝ)⁻¹)
⊢ 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 (α := ℝ) (β := ℝ) ((↑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) : ℝ)⁻¹)
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]