-- 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 :
  (↑expMap : realSpace K → realSpace K)
      ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x) =
    HSMul.hSMul (β := (w : InfinitePlace K) → ℝ) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
      ∏ i : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          ((w : (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))
                          i)) :
                    𝓞 K) :
                K) :
            ℝ)
          (x (↑i : InfinitePlace K))
simp_rw₁ :
  (↑expMap : realSpace K → realSpace K)
      (∑ i : InfinitePlace K,
        HSMul.hSMul (β := realSpace K) (x i)
          ((completeBasis K : (a : InfinitePlace K) → realSpace K) i : realSpace K)) =
    HSMul.hSMul (β := (w : InfinitePlace K) → ℝ) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
      ∏ i : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          ((w : (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))
                          i)) :
                    𝓞 K) :
                K) :
            ℝ)
          (x (↑i : InfinitePlace K))
simp_rw₂ :
  (↑expMap : realSpace K → realSpace K)
      (HSMul.hSMul (β := realSpace K) (x w₀)
          ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀ : realSpace K) +
        ∑ i : { i : InfinitePlace K // i ≠ w₀ },
          HSMul.hSMul (β := realSpace K) (x (↑i : InfinitePlace K))
            ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K)) =
    HSMul.hSMul (β := (w : InfinitePlace K) → ℝ) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
      ∏ i : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          ((w : (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))
                          i)) :
                    𝓞 K) :
                K) :
            ℝ)
          (x (↑i : InfinitePlace K))
simp_rw₃ :
  (↑expMap : realSpace K → realSpace K)
        (HSMul.hSMul (β := realSpace K) (x w₀)
          ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀ : realSpace K)) *
      (↑expMap : realSpace K → realSpace K)
        (∑ i : { i : InfinitePlace K // i ≠ w₀ },
          HSMul.hSMul (β := realSpace K) (x (↑i : InfinitePlace K))
            ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K)) =
    HSMul.hSMul (β := (w : InfinitePlace K) → ℝ) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
      ∏ i : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          ((w : (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))
                          i)) :
                    𝓞 K) :
                K) :
            ℝ)
          (x (↑i : InfinitePlace K))
⊢ (↑expMapBasis : realSpace K → realSpace K) x =
    HSMul.hSMul (β := (w : InfinitePlace K) → ℝ) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
      ∏ i : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          ((w : (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))
                          i)) :
                    𝓞 K) :
                K) :
            ℝ)
          (x (↑i : InfinitePlace K))
have simp_rw₄ : HPow.hPow (α := realSpace K)
      ((↑expMap : realSpace K → realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀)) (x w₀) *
    (↑expMap : realSpace K → realSpace K)
      (∑ i : { i : InfinitePlace K // i ≠ w₀ },
        HSMul.hSMul (β := realSpace K) (x (↑i : InfinitePlace K))
          ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K)) =
  HSMul.hSMul (β := (w : InfinitePlace K) → ℝ) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
    ∏ i : { w : InfinitePlace K // w ≠ w₀ },
      HPow.hPow (α := ℝ)
        ((w : (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))
                        i)) :
                  𝓞 K) :
              K) :
          ℝ)
        (x (↑i : InfinitePlace K))
Tactic: simp_rw [expMapBasis_apply, Basis.equivFun_symm_apply, Fintype.sum_eq_add_sum_subtype_ne _ w₀,
    expMap_add, expMap_smul, expMap_basis_of_eq, Pi.pow_def, Real.exp_one_rpow, Pi.mul_def,
    expMap_sum, expMap_smul, expMap_basis_of_ne, Pi.smul_def, smul_eq_mul, prod_apply, Pi.pow_apply,
    normAtAllPlaces_mixedEmbedding]