-- 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
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) : ℝ)⁻¹)
h₄ :
  (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (((↑w : InfinitePlace K) : (a : K) → ℝ) x) -
      (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹ =
    (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log (((↑w : InfinitePlace K) : (a : K) → ℝ) x) -
        Real.log
            ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K)) *
          (↑(finrank ℚ K) : ℝ)⁻¹)
⊢ (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 (((↑w : InfinitePlace K) : (a : K) → ℝ) x) -
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹ =
  (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log (((↑w : InfinitePlace K) : (a : K) → ℝ) x) -
    (↑(↑w : InfinitePlace K).mult : ℝ) *
      (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]