-- 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)
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)
h₅ :
  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)
h₆ :
  x (↑x_1 : InfinitePlace K) - (↑(↑x_1 : InfinitePlace K).mult : ℝ) * (Real.log 1 * (↑(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 (↑x_1 : InfinitePlace K) - (↑(↑x_1 : InfinitePlace K).mult : ℝ) * HMul.hMul (α := ℝ) 0 (↑(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]