awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  |(LinearMap.det : (a : (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ) → ℝ)
        (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
              (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
          (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ)| =
    (↑(finrank ℚ K) : ℝ) * regulator K
rw₁ :
  |Matrix.det.{0, u_1} (n := InfinitePlace K)
        ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
            (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
          (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
                (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
            (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ))| =
    (↑(finrank ℚ K) : ℝ) * regulator K
rw₂ :
  |Matrix.det.{0, u_1} (n := InfinitePlace K)
        (Matrix.transpose
          ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
              (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
            (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
                  (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
              (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ)))| =
    (↑(finrank ℚ K) : ℝ) * regulator K
⊢ |ContinuousLinearMap.det (M := InfinitePlace K → ℝ)
        (↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) : (InfinitePlace K → ℝ) →L[ℝ] realSpace K)| =
    (↑(finrank ℚ K) : ℝ) * regulator K
have rw₃ : |Matrix.det.{0, u_1} (n := InfinitePlace K)
      (Matrix.transpose
        ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
            (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
          (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
                (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
            (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ)))| =
  (↑(finrank ℚ K) : ℝ) * regOfFamily (fundSystem K)
Tactic: classical
  rw [ContinuousLinearMap.det, ← LinearMap.det_toMatrix (completeBasis K), ← Matrix.det_transpose,
    regulator_eq_regOfFamily_fundSystem, finrank_mul_regOfFamily_eq_det _ w₀ equivFinRank.symm]
  congr 2 with w i
  rw [Matrix.transpose_apply, LinearMap.toMatrix_apply, Matrix.of_apply, ← Basis.equivFunL_apply,
    ContinuousLinearMap.coe_coe, ContinuousLinearEquiv.coe_apply,
    (completeBasis K).equivFunL.apply_symm_apply]
  split_ifs with hw
  · rw [hw, completeBasis_apply_of_eq]
  · simp_rw [completeBasis_apply_of_ne K ⟨w, hw⟩, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]
-- 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
⊢ (↑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 : (↑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))
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]
-- 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))
⊢ (↑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₁ : (↑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))
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]
-- 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
⊢ (↑expMapBasis : realSpace K → realSpace K) x =
    HSMul.hSMul (β := realSpace K) (Real.exp (x w₀))
      ((↑expMapBasis : realSpace K → realSpace K) fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else x i)
have rw : (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))) =
  HSMul.hSMul (β := realSpace 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) :
          ℝ)
        (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
Tactic: rw [expMapBasis_apply', expMapBasis_apply', if_pos rfl, smul_smul, ← Real.exp_add, add_zero]
-- 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
| HSMul.hSMul (β := realSpace 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) :
          ℝ)
        (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
have h : ∀ (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) :
      ℝ)
    (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
Tactic: enter [2, w, 2, i]
-- 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
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) :
      ℝ)
    (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
have h : 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: rw [if_neg i.prop]
-- 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
| HSMul.hSMul (β := realSpace 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) :
          ℝ)
        (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
have h : ∀ (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: enter [2, w, 2, i]
    rw [if_neg i.prop]
-- 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
⊢ (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))) =
    HSMul.hSMul (β := realSpace 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) :
            ℝ)
          (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
have conv_rhs : (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))) =
  HSMul.hSMul (β := realSpace 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) :
          ℝ)
        (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
Tactic: conv_rhs =>
    enter [2, w, 2, i]
    rw [if_neg i.prop]
-- 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
⊢ ∏ w : InfinitePlace K, (↑expMapBasis : realSpace K → realSpace K) x w ^ w.mult = Real.exp (x w₀) ^ finrank ℚ K
have simp_rw : Real.exp (x w₀) ^ finrank ℚ K *
    ∏ x_1 : InfinitePlace K,
      ∏ x_2 : { w : InfinitePlace K // w ≠ w₀ },
        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))
                            x_2)) :
                      𝓞 K) :
                  K) :
              ℝ)
            (x (↑x_2 : InfinitePlace K)) ^
          x_1.mult =
  Real.exp (x w₀) ^ finrank ℚ K
Tactic: simp_rw [expMapBasis_apply', Pi.smul_def, smul_eq_mul, mul_pow, prod_mul_distrib,
    prod_pow_eq_pow_sum, sum_mult_eq, ← prod_pow]
-- 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
⊢ Real.exp (x w₀) ^ finrank ℚ K *
      ∏ x_1 : InfinitePlace K,
        ∏ x_2 : { w : InfinitePlace K // w ≠ w₀ },
          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))
                              x_2)) :
                        𝓞 K) :
                    K) :
                ℝ)
              (x (↑x_2 : InfinitePlace K)) ^
            x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K
have rw : 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
Tactic: rw [prod_comm]
-- 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
⊢ 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₀ },
      ∏ 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
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]
-- 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
⊢ 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 (α := ℝ)
        (∏ 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
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]