-- 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
e_a :
  ∏ x_1 : InfinitePlace K,
      Real.exp
        (HMul.hMul (α := ℝ) (↑x_1.mult : ℝ)⁻¹
          ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x x_1)) =
    HMul.hMul (α := ℝ) (∏ w : InfinitePlace K, (↑expMapBasis : realSpace K → realSpace K) x w ^ w.mult)
      (∏ w : { w : InfinitePlace K // w.IsComplex },
          (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹
e_a₁ :
  HMul.hMul (α := ℝ)
      (∏ w : { w : InfinitePlace K // w.IsReal },
        Real.exp
          (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)⁻¹
            ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
              (↑w : InfinitePlace K))))
      (∏ w : { w : InfinitePlace K // w.IsComplex },
        Real.exp
          (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)⁻¹
            ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
              (↑w : InfinitePlace K)))) =
    HMul.hMul (α := ℝ)
        (∏ w : { w : InfinitePlace K // w.IsReal },
          (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)
        (∏ w : { w : InfinitePlace K // w.IsComplex },
          (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult) *
      (∏ w : { w : InfinitePlace K // w.IsComplex },
          (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹
e_a₂ :
  HMul.hMul (α := ℝ)
      (∏ w : { w : InfinitePlace K // w.IsReal },
        Real.exp
          (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)⁻¹
            ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
              (↑w : InfinitePlace K))))
      (∏ w : { w : InfinitePlace K // w.IsComplex },
        Real.exp
          (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)⁻¹
            ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
              (↑w : InfinitePlace K)))) =
    HMul.hMul (α := ℝ)
        (∏ x_1 : { w : InfinitePlace K // w.IsReal },
          HPow.hPow (α := ℝ)
            ((↑expMap : realSpace K → realSpace K)
                ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x)
                (↑x_1 : InfinitePlace K) :
              ℝ)
            (↑x_1 : InfinitePlace K).mult)
        (∏ x_1 : { w : InfinitePlace K // w.IsComplex },
          HPow.hPow (α := ℝ)
            ((↑expMap : realSpace K → realSpace K)
                ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x)
                (↑x_1 : InfinitePlace K) :
              ℝ)
            (↑x_1 : InfinitePlace K).mult) *
      (∏ x_1 : { w : InfinitePlace K // w.IsComplex },
          (↑expMap : realSpace K → realSpace K)
            ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x)
            (↑x_1 : InfinitePlace K))⁻¹
e_a₃ :
  HMul.hMul (α := ℝ)
      (∏ w : { w : InfinitePlace K // w.IsReal },
        Real.exp
          (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)⁻¹
            ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
              (↑w : InfinitePlace K))))
      (∏ w : { w : InfinitePlace K // w.IsComplex },
        Real.exp
          (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)⁻¹
            ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
              (↑w : InfinitePlace K)))) =
    HMul.hMul (α := ℝ)
        (∏ x_1 : { w : InfinitePlace K // w.IsReal },
          Real.exp
              (HMul.hMul (α := ℝ) (↑(↑x_1 : InfinitePlace K).mult : ℝ)⁻¹
                ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
                  (↑x_1 : InfinitePlace K))) ^
            (↑x_1 : InfinitePlace K).mult)
        (∏ x_1 : { w : InfinitePlace K // w.IsComplex },
          Real.exp
              (HMul.hMul (α := ℝ) (↑(↑x_1 : InfinitePlace K).mult : ℝ)⁻¹
                ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
                  (↑x_1 : InfinitePlace K))) ^
            (↑x_1 : InfinitePlace K).mult) *
      (∏ w : { w : InfinitePlace K // w.IsComplex },
          Real.exp
            (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)⁻¹
              ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
                (↑w : InfinitePlace K))))⁻¹
e_a₄ :
  HMul.hMul (α := ℝ)
      (∏ x_1 : { w : InfinitePlace K // w.IsReal },
        Real.exp
          (HMul.hMul (α := ℝ) (↑1 : ℝ)⁻¹
            ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
              (↑x_1 : InfinitePlace K))))
      (∏ w : { w : InfinitePlace K // w.IsComplex },
        Real.exp
          (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)⁻¹
            ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
              (↑w : InfinitePlace K)))) =
    HMul.hMul (α := ℝ)
        (∏ x_1 : { w : InfinitePlace K // w.IsReal },
          HPow.hPow (β := ℕ)
            (Real.exp
              (HMul.hMul (α := ℝ) (↑1 : ℝ)⁻¹
                ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
                  (↑x_1 : InfinitePlace K))))
            1)
        (∏ x_1 : { w : InfinitePlace K // w.IsComplex },
          Real.exp
              (HMul.hMul (α := ℝ) (↑(↑x_1 : InfinitePlace K).mult : ℝ)⁻¹
                ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
                  (↑x_1 : InfinitePlace K))) ^
            (↑x_1 : InfinitePlace K).mult) *
      (∏ w : { w : InfinitePlace K // w.IsComplex },
          Real.exp
            (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)⁻¹
              ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
                (↑w : InfinitePlace K))))⁻¹
⊢ ∏ x_1 : InfinitePlace K,
      Real.exp
        (HMul.hMul (α := ℝ) (↑x_1.mult : ℝ)⁻¹
          ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x x_1)) =
    Real.exp (x w₀) ^ finrank ℚ K *
      (∏ w : { w : InfinitePlace K // w.IsComplex },
          (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹
have e_a₅ : HMul.hMul (α := ℝ)
    (∏ x_1 : { w : InfinitePlace K // w.IsReal },
      Real.exp
        (HMul.hMul (α := ℝ) (↑1 : ℝ)⁻¹
          ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
            (↑x_1 : InfinitePlace K))))
    (∏ x_1 : { w : InfinitePlace K // w.IsComplex },
      Real.exp
        (HMul.hMul (α := ℝ) (↑2 : ℝ)⁻¹
          ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
            (↑x_1 : InfinitePlace K)))) =
  HMul.hMul (α := ℝ)
      (∏ x_1 : { w : InfinitePlace K // w.IsReal },
        HPow.hPow (β := ℕ)
          (Real.exp
            (HMul.hMul (α := ℝ) (↑1 : ℝ)⁻¹
              ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
                (↑x_1 : InfinitePlace K))))
          1)
      (∏ x_1 : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ)
          (Real.exp
            (HMul.hMul (α := ℝ) (↑2 : ℝ)⁻¹
              ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
                (↑x_1 : InfinitePlace K))))
          2) *
    (∏ x_1 : { w : InfinitePlace K // w.IsComplex },
        Real.exp
          (HMul.hMul (α := ℝ) (↑2 : ℝ)⁻¹
            ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
              (↑x_1 : InfinitePlace K))))⁻¹
Tactic: simp_rw [← prod_expMapBasis_pow, prod_eq_prod_mul_prod, expMapBasis_apply, expMap_apply,
      mult_isReal, mult_isComplex, pow_one, Finset.prod_pow, pow_two, mul_assoc, mul_inv_cancel₀
      (Finset.prod_ne_zero_iff.mpr <| fun _ _ ↦ Real.exp_ne_zero _), mul_one]