awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
rw :
  Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
      ((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                  logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
                (a : logSpace K) → Fin (rank K) →₀ ℝ)
              fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
              (∑ i : { i : InfinitePlace K // i ≠ w₀ },
                  HSMul.hSMul (β := realSpace K) (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
                    ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K))
                (↑w : InfinitePlace K) :
            (a : Fin (rank K)) → ℝ)
          (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
              (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a ≠ w₀) w hw) :
            Fin (rank K)) :
        ℝ) ↔
    Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
⊢ Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
      (((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                    logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
                  (a : logSpace K) → Fin (rank K) →₀ ℝ)
                (logMap
                  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
                    ((↑expMapBasis : realSpace K → realSpace K) x))) :
              Fin (rank K) →₀ ℝ) :
            (a : Fin (rank K)) → ℝ)
          (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
              (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a ≠ w₀) w hw) :
            Fin (rank K)) :
        ℝ) ↔
    Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)

Tactic:
rw [expMapBasis_apply'', map_smul, logMap_real_smul (norm_expMapBasis_ne_zero _)
    (Real.exp_ne_zero _), expMapBasis_apply, logMap_expMap (by rw [← expMapBasis_apply,
    norm_expMapBasis, if_pos rfl, Real.exp_zero, one_pow]), Basis.equivFun_symm_apply,
    Fintype.sum_eq_add_sum_subtype_ne _ w₀, if_pos rfl, zero_smul, zero_add]

Premises used: Module.Basis.equivFun_symm_apply, Fintype.sum_eq_add_sum_subtype_ne, NumberField.mixedEmbedding.logMap_real_smul, if_pos, zero_add, NumberField.Units.dirichletUnitTheorem.w₀, zero_smul, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis_ne_zero, NumberField.mixedEmbedding.fundamentalCone.logMap_expMap, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply'', NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply, rfl, Real.exp_ne_zero, map_smul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
h :
  ∀ (w i : { i : InfinitePlace K // i ≠ w₀ }),
    HSMul.hSMul (β := realSpace K) (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
      ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K)
| Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
    ((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
              (a : logSpace K) → Fin (rank K) →₀ ℝ)
            fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
            (∑ i : { i : InfinitePlace K // i ≠ w₀ },
                HSMul.hSMul (β := realSpace K) (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
                  ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K))
              (↑w : InfinitePlace K) :
          (a : Fin (rank K)) → ℝ)
        (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
              (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
            (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a ≠ w₀) w hw) :
          Fin (rank K)) :
      ℝ)

Tactic:
enter [2, 1, 2, w, 2, i]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
w_1 : InfinitePlace K
hw : w_1 ≠ w₀
w i : { i : InfinitePlace K // i ≠ w₀ }
h :
  HSMul.hSMul (β := realSpace K) (x (↑i : InfinitePlace K))
    ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K)
| HSMul.hSMul (β := realSpace K) (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
    ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K)

Tactic:
rw [if_neg i.prop]

Premises used: Subtype.prop, if_neg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
h :
  ∀ (w 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)
| Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
    ((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
              (a : logSpace K) → Fin (rank K) →₀ ℝ)
            fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
            (∑ i : { i : InfinitePlace K // i ≠ w₀ },
                HSMul.hSMul (β := realSpace K) (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
                  ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K))
              (↑w : InfinitePlace K) :
          (a : Fin (rank K)) → ℝ)
        (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
              (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
            (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a ≠ w₀) w hw) :
          Fin (rank K)) :
      ℝ)

Tactic:
enter [2, 1, 2, w, 2, i]
    rw [if_neg i.prop]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
conv_lhs :
  Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
      ((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                  logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
                (a : logSpace K) → Fin (rank K) →₀ ℝ)
              fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
              (∑ 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))
                (↑w : InfinitePlace K) :
            (a : Fin (rank K)) → ℝ)
          (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
              (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a ≠ w₀) w hw) :
            Fin (rank K)) :
        ℝ) ↔
    Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
⊢ Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
      ((((Basis.repr (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) :
                  logSpace K ≃ₗ[ℝ] Fin (rank K) →₀ ℝ) :
                (a : logSpace K) → Fin (rank K) →₀ ℝ)
              fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
              (∑ i : { i : InfinitePlace K // i ≠ w₀ },
                  HSMul.hSMul (β := realSpace K) (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
                    ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K))
                (↑w : InfinitePlace K) :
            (a : Fin (rank K)) → ℝ)
          (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
              (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a ≠ w₀) w hw) :
            Fin (rank K)) :
        ℝ) ↔
    Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)

Tactic:
conv_lhs =>
    enter [2, 1, 2, w, 2, i]
    rw [if_neg i.prop]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : ∀ x ∈ (↑expMapBasis : realSpace K → realSpace K) '' s, ∀ (w : InfinitePlace K), 0 ≤ x w
⊢ normAtAllPlaces '' normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' s =
    (↑expMapBasis : realSpace K → realSpace K) '' s

Tactic:
apply normAtAllPlaces_image_preimage_of_nonneg

Premises used: NumberField.mixedEmbedding.normAtAllPlaces_image_preimage_of_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
x : realSpace K
left : x ∈ s
w : InfinitePlace K
⊢ 0 ≤ (↑expMapBasis : realSpace K → realSpace K) x w

Tactic:
(expMapBasis_pos _ _).le

Premises used: LT.lt.le, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
x : realSpace K
left : x ∈ s
w : InfinitePlace K
⊢ 0 ≤ (↑expMapBasis : realSpace K → realSpace K) x w

Tactic:
exact (expMapBasis_pos _ _).le

Premises used: LT.lt.le, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
rw :
  HMul.hMul (α := ℝ)
      (∏ 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)))
      (∏ x : InfinitePlace K, (↑x.mult : ℝ)⁻¹) =
    Real.exp (x w₀) ^ finrank ℚ K *
        (∏ w : { w : InfinitePlace K // w.IsComplex },
            (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹ *
      HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces 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)) *
        (↑x_1.mult : ℝ)⁻¹ =
    Real.exp (x w₀) ^ finrank ℚ K *
        (∏ w : { w : InfinitePlace K // w.IsComplex },
            (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹ *
      HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K)

Tactic:
rw [Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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)) =
    Real.exp (x w₀) ^ finrank ℚ K *
      (∏ w : { w : InfinitePlace K // w.IsComplex },
          (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹
e_a₁ : ∏ x : InfinitePlace K, (↑x.mult : ℝ)⁻¹ = HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K)
⊢ HMul.hMul (α := ℝ)
      (∏ 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)))
      (∏ x : InfinitePlace K, (↑x.mult : ℝ)⁻¹) =
    Real.exp (x w₀) ^ finrank ℚ K *
        (∏ w : { w : InfinitePlace K // w.IsComplex },
            (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹ *
      HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K)

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
⊢ ∏ x : InfinitePlace K, (↑x.mult : ℝ)⁻¹ = HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K)

Tactic:
simp [prod_eq_prod_mul_prod, mult_isReal, mult_isComplex]

Premises used: NumberField.InfinitePlace.mult_isComplex, NumberField.InfinitePlace.mult_isReal, NumberField.InfinitePlace.prod_eq_prod_mul_prod
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
⊢ HasFDerivAt
    ((↑expMap : realSpace K → realSpace K) ∘
      (⇑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) : (a : InfinitePlace K → ℝ) → realSpace K))
    (fderiv_expMapBasis K x) x

Tactic:
(hasFDerivAt_expMap _).comp x (completeBasis K).equivFunL.symm.hasFDerivAt

Premises used: ContinuousLinearEquiv.symm, Module.Basis.equivFunL, ContinuousLinearEquiv.hasFDerivAt, NumberField.mixedEmbedding.fundamentalCone.completeBasis, HasFDerivAt.comp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
⊢ HasFDerivAt
    ((↑expMap : realSpace K → realSpace K) ∘
      (⇑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) : (a : InfinitePlace K → ℝ) → realSpace K))
    (fderiv_expMapBasis K x) x

Tactic:
exact (hasFDerivAt_expMap _).comp x (completeBasis K).equivFunL.symm.hasFDerivAt

Premises used: ContinuousLinearEquiv.symm, Module.Basis.equivFunL, ContinuousLinearEquiv.hasFDerivAt, NumberField.mixedEmbedding.fundamentalCone.completeBasis, HasFDerivAt.comp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
simp_rw :
  |Real.exp (x w₀) ^ finrank ℚ K *
            (∏ w : { w : InfinitePlace K // w.IsComplex },
                (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹ *
          HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K)| *
      ((↑(finrank ℚ K) : ℝ) * regulator K) =
    Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ)) *
            (∏ w : { w : InfinitePlace K // w.IsComplex },
                (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹ *
          HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        (↑(finrank ℚ K) : ℝ) *
      regulator K
⊢ |(fderiv_expMapBasis K x).det| =
    Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ)) *
            (∏ w : { w : InfinitePlace K // w.IsComplex },
                (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹ *
          HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        (↑(finrank ℚ K) : ℝ) *
      regulator K

Tactic:
simp_rw [fderiv_expMapBasis, det, coe_comp, LinearMap.det_comp, fderiv_expMap, coe_pi, coe_comp,
    coe_proj, LinearMap.det_pi, LinearMap.det_ring, ContinuousLinearMap.coe_coe, smulRight_apply,
    one_apply, one_smul, abs_mul, abs_det_completeBasis_equivFunL_symm, prod_deriv_expMap_single]

Premises used: LinearMap.det_pi, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, abs_mul, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, ContinuousLinearMap.det, ContinuousLinearMap.coe_coe, ContinuousLinearMap.coe_comp, ContinuousLinearMap.coe_pi, ContinuousLinearMap.one_apply, one_smul, NumberField.mixedEmbedding.fundamentalCone.fderiv_expMap, LinearMap.det_comp, ContinuousLinearMap.coe_proj, LinearMap.det_ring, ContinuousLinearMap.smulRight_apply, NumberField.mixedEmbedding.fundamentalCone.fderiv_expMapBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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.IsComplex },
              (↑expMapBasis : realSpace K → realSpace K) x (↑x_1 : InfinitePlace K))⁻¹ *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      ((↑(finrank ℚ K) : ℝ) * regulator K) =
    Real.exp (x w₀) ^ finrank ℚ K *
            (∏ x_1 : { w : InfinitePlace K // w.IsComplex },
                (↑expMapBasis : realSpace K → realSpace K) x (↑x_1 : InfinitePlace K))⁻¹ *
          HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        (↑(finrank ℚ K) : ℝ) *
      regulator K
⊢ |Real.exp (x w₀) ^ finrank ℚ K *
            (∏ w : { w : InfinitePlace K // w.IsComplex },
                (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹ *
          HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K)| *
      ((↑(finrank ℚ K) : ℝ) * regulator K) =
    Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ)) *
            (∏ w : { w : InfinitePlace K // w.IsComplex },
                (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹ *
          HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        (↑(finrank ℚ K) : ℝ) *
      regulator K

Tactic:
simp_rw [abs_mul, Real.exp_mul, abs_pow, Real.rpow_natCast, abs_of_nonneg (Real.exp_nonneg _),
    abs_inv, abs_prod, abs_of_nonneg (expMapBasis_nonneg _ _), Nat.abs_ofNat]

Premises used: Real.exp_mul, abs_inv, abs_mul, abs_of_nonneg, Real.exp_nonneg, Nat.abs_ofNat, Finset.abs_prod, Real.rpow_natCast, abs_pow, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
⊢ Real.exp (x w₀) ^ finrank ℚ K *
          (∏ x_1 : { w : InfinitePlace K // w.IsComplex },
              (↑expMapBasis : realSpace K → realSpace K) x (↑x_1 : InfinitePlace K))⁻¹ *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      ((↑(finrank ℚ K) : ℝ) * regulator K) =
    Real.exp (x w₀) ^ finrank ℚ K *
            (∏ x_1 : { w : InfinitePlace K // w.IsComplex },
                (↑expMapBasis : realSpace K → realSpace K) x (↑x_1 : InfinitePlace K))⁻¹ *
          HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        (↑(finrank ℚ K) : ℝ) *
      regulator K

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
rw :
  ∫⁻ (x : realSpace K) in s,
      ENNReal.ofReal |(fderiv_expMapBasis K x).det| * f ((↑expMapBasis : realSpace K → realSpace K) x) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
      ∫⁻ (x : realSpace K) in s,
        ENNReal.ofReal (Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ))) *
            (∏ i : { w : InfinitePlace K // w.IsComplex },
                ENNReal.ofReal
                  ((↑expMapBasis : realSpace K → realSpace K) (fun (w : InfinitePlace K) ↦ x w)
                    (↑i : InfinitePlace K)))⁻¹ *
          f ((↑expMapBasis : realSpace K → realSpace K) x)
⊢ ∫⁻ (x : realSpace K) in (↑expMapBasis : realSpace K → realSpace K) '' s, f x =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
      ∫⁻ (x : realSpace K) in s,
        ENNReal.ofReal (Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ))) *
            (∏ i : { w : InfinitePlace K // w.IsComplex },
                ENNReal.ofReal
                  ((↑expMapBasis : realSpace K → realSpace K) (fun (w : InfinitePlace K) ↦ x w)
                    (↑i : InfinitePlace K)))⁻¹ *
          f ((↑expMapBasis : realSpace K → realSpace K) x)

Tactic:
rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume hs
    (fun x _ ↦ (hasFDerivAt_expMapBasis K x).hasFDerivWithinAt) (injective_expMapBasis K).injOn]

Premises used: HasFDerivAt.hasFDerivWithinAt, Function.Injective.injOn, MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul, NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMapBasis, MeasureTheory.MeasureSpace.volume, NumberField.mixedEmbedding.fundamentalCone.injective_expMapBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
simp_rw :
  ∫⁻ (x : realSpace K) in s,
      ENNReal.ofReal
          (Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ)) *
                  (∏ w : { w : InfinitePlace K // w.IsComplex },
                      (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹ *
                HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
              (↑(finrank ℚ K) : ℝ) *
            regulator K) *
        f ((↑expMapBasis : realSpace K → realSpace K) x) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
      ∫⁻ (x : realSpace K) in s,
        ENNReal.ofReal (Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ))) *
            (∏ i : { w : InfinitePlace K // w.IsComplex },
                ENNReal.ofReal
                  ((↑expMapBasis : realSpace K → realSpace K) (fun (w : InfinitePlace K) ↦ x w)
                    (↑i : InfinitePlace K)))⁻¹ *
          f ((↑expMapBasis : realSpace K → realSpace K) x)
⊢ ∫⁻ (x : realSpace K) in s,
      ENNReal.ofReal |(fderiv_expMapBasis K x).det| * f ((↑expMapBasis : realSpace K → realSpace K) x) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
      ∫⁻ (x : realSpace K) in s,
        ENNReal.ofReal (Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ))) *
            (∏ i : { w : InfinitePlace K // w.IsComplex },
                ENNReal.ofReal
                  ((↑expMapBasis : realSpace K → realSpace K) (fun (w : InfinitePlace K) ↦ x w)
                    (↑i : InfinitePlace K)))⁻¹ *
          f ((↑expMapBasis : realSpace K → realSpace K) x)

Tactic:
simp_rw [abs_det_fderiv_expMapBasis]

Premises used: NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
⊢ Measurable.{u_1, u_1} (α := realSpace K) (↑expMapBasis : realSpace K → realSpace K)

Tactic:
have : Measurable expMapBasis := (continuous_expMapBasis K).measurable
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this : Measurable.{u_1, u_1} (α := realSpace K) (↑expMapBasis : realSpace K → realSpace K)
⊢ Measurable (β := ℝ≥0∞) fun (x : realSpace K) ↦
    ENNReal.ofReal (Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ))) *
        (∏ i : { w : InfinitePlace K // w.IsComplex },
            ENNReal.ofReal
              ((↑expMapBasis : realSpace K → realSpace K) (fun (w : InfinitePlace K) ↦ x w) (↑i : InfinitePlace K)))⁻¹ *
      f ((↑expMapBasis : realSpace K → realSpace K) x)

Tactic:
fun_prop