-- 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))
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))
simp_rw₅ :
  HPow.hPow (α := realSpace K) (fun (x : InfinitePlace K) ↦ Real.exp 1) (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))
simp_rw₆ :
  HMul.hMul (α := realSpace K) (fun (i : InfinitePlace K) ↦ Real.exp 1 ^ 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))
simp_rw₇ :
  HMul.hMul (α := realSpace K) (fun (i : InfinitePlace K) ↦ Real.exp (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))
simp_rw₈ :
  (fun (i : InfinitePlace K) ↦
      HMul.hMul (β := ℝ) (Real.exp (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))
            i :
          ℝ)) =
    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₉ :
  (fun (i : InfinitePlace K) ↦
      Real.exp (x w₀) *
        (∏ i : { i : InfinitePlace K // i ≠ w₀ },
            (↑expMap : realSpace K → realSpace K)
              (HSMul.hSMul (β := realSpace K) (x (↑i : InfinitePlace K))
                ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K)))
          i) =
    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₁₀ :
  (fun (i : InfinitePlace K) ↦
      Real.exp (x w₀) *
        (∏ x_1 : { i : InfinitePlace K // i ≠ w₀ },
            HPow.hPow (α := realSpace K)
              ((↑expMap : realSpace K → realSpace K)
                ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑x_1 : InfinitePlace K)))
              (x (↑x_1 : InfinitePlace K)))
          i) =
    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₁₁ :
  (fun (i : InfinitePlace K) ↦
      Real.exp (x w₀) *
        (∏ x_1 : { i : InfinitePlace K // i ≠ w₀ },
            HPow.hPow (α := realSpace K)
              (normAtAllPlaces
                ((mixedEmbedding K : (a : K) → mixedSpace 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))))
              (x (↑x_1 : InfinitePlace K)))
          i) =
    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₁₂ :
  Eq.{u_1 + 1} (α := realSpace K)
    (fun (i : InfinitePlace K) ↦
      Real.exp (x w₀) *
        (∏ x_1 : { i : InfinitePlace K // i ≠ w₀ },
            HPow.hPow (α := realSpace K)
              (normAtAllPlaces
                ((mixedEmbedding K : (a : K) → mixedSpace 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))))
              (x (↑x_1 : InfinitePlace K)))
          i)
    fun (i : InfinitePlace K) ↦
    HSMul.hSMul (β := ℝ) (Real.exp (x w₀))
      (∏ i_1 : { w : InfinitePlace K // w ≠ w₀ },
        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))
                          i_1)) :
                    𝓞 K) :
                K) :
            ℝ)
          (x (↑i_1 : 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₁₃ : Eq.{u_1 + 1} (α := realSpace K)
  (fun (i : InfinitePlace K) ↦
    Real.exp (x w₀) *
      (∏ x_1 : { i : InfinitePlace K // i ≠ w₀ },
          HPow.hPow (α := realSpace K)
            (normAtAllPlaces
              ((mixedEmbedding K : (a : K) → mixedSpace 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))))
            (x (↑x_1 : InfinitePlace K)))
        i)
  fun (i : InfinitePlace K) ↦
  Real.exp (x w₀) *
    ∏ i_1 : { w : InfinitePlace K // w ≠ w₀ },
      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))
                        i_1)) :
                  𝓞 K) :
              K) :
          ℝ)
        (x (↑i_1 : 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]