-- 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
simp_rw :
  Real.exp (x w₀) ^ finrank ℚ K *
      ∏ x_1 : { w : InfinitePlace K // w ≠ w₀ },
        ∏ x_2 : InfinitePlace K,
          HPow.hPow (α := ℝ)
              ((x_2 : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K
                            (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                              x_1)) :
                        𝓞 K) :
                    K) :
                ℝ)
              x_2.mult ^
            x (↑x_1 : InfinitePlace K) =
    Real.exp (x w₀) ^ finrank ℚ K
simp_rw₁ :
  Real.exp (x w₀) ^ finrank ℚ K *
      ∏ x_1 : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          (∏ i : InfinitePlace K,
            HPow.hPow (α := ℝ)
              ((i : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K
                            (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                              x_1)) :
                        𝓞 K) :
                    K) :
                ℝ)
              i.mult)
          (x (↑x_1 : InfinitePlace K)) =
    Real.exp (x w₀) ^ finrank ℚ K
simp_rw₂ :
  Real.exp (x w₀) ^ finrank ℚ K *
      ∏ x_1 : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          (↑|(Algebra.norm ℚ : (a : K) → ℚ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K
                            (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                              x_1)) :
                        𝓞 K) :
                    K)| :
            ℝ)
          (x (↑x_1 : InfinitePlace K)) =
    Real.exp (x w₀) ^ finrank ℚ K
simp_rw₃ :
  Real.exp (x w₀) ^ finrank ℚ K *
      ∏ x_1 : { w : InfinitePlace K // w ≠ w₀ }, HPow.hPow (α := ℝ) (↑1 : ℝ) (x (↑x_1 : InfinitePlace K)) =
    Real.exp (x w₀) ^ finrank ℚ K
⊢ Real.exp (x w₀) ^ finrank ℚ K *
      ∏ y : { w : InfinitePlace K // w ≠ w₀ },
        ∏ x_1 : InfinitePlace K,
          HPow.hPow (α := ℝ)
              ((x_1 : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K
                            (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                              y)) :
                        𝓞 K) :
                    K) :
                ℝ)
              (x (↑y : InfinitePlace K)) ^
            x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K
have simp_rw₄ : Real.exp (x w₀) ^ finrank ℚ K *
    ∏ x_1 : { w : InfinitePlace K // w ≠ w₀ }, HPow.hPow (α := ℝ) 1 (x (↑x_1 : InfinitePlace K)) =
  Real.exp (x w₀) ^ finrank ℚ K
Tactic: simp_rw [Real.rpow_pow_comm (apply_nonneg _ _), Real.finsetProd_rpow _ _
    fun _ _ ↦ pow_nonneg (apply_nonneg _ _) _, prod_eq_abs_norm, Units.norm, Rat.cast_one,
    Real.one_rpow, prod_const_one, mul_one]