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
x : realSpace K
simp_rw :
  (∀ (i : Fin (rank 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) →₀ ℝ)
                  (logMap
                    ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
                      ((↑expMapBasis : realSpace K → realSpace K) x))) :
                Fin (rank K) →₀ ℝ) :
              (a : Fin (rank K)) → ℝ)
            i :
          ℝ)) ↔
    ∀ (w : InfinitePlace K), w ≠ w₀ → Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
⊢ Membership.mem (γ := Set (logSpace K))
      (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
      (logMap
        ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ((↑expMapBasis : realSpace K → realSpace K) x))) ↔
    ∀ (w : InfinitePlace K), w ≠ w₀ → Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
have simp_rw₁ : (∀ (b : { w : InfinitePlace K // w ≠ 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))
              b :
            Fin (rank K)) :
        ℝ)) ↔
  ∀ (w : InfinitePlace K), w ≠ w₀ → Membership.mem (γ := Set ℝ) (Set.Ico 0 1) (x w)
Tactic: classical
  simp_rw [ZSpan.mem_fundamentalDomain, equivFinRank.forall_congr_left, Subtype.forall]
  refine forall₂_congr fun w hw ↦ ?_
  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]
  conv_lhs =>
    enter [2, 1, 2, w, 2, i]
    rw [if_neg i.prop]
  simp_rw [sum_apply, ← sum_fn, map_sum, Pi.smul_apply, ← Pi.smul_def, map_smul,
    completeBasis_apply_of_ne, expMap_symm_apply, normAtAllPlaces_mixedEmbedding,
    ← logEmbedding_component, logEmbedding_fundSystem, Finsupp.coe_finsetSum, Finsupp.coe_smul,
    sum_apply, Pi.smul_apply, Basis.ofZLatticeBasis_repr_apply, Basis.repr_self,
    Finsupp.single_apply, EmbeddingLike.apply_eq_iff_eq, Int.cast_ite, Int.cast_one, Int.cast_zero,
    smul_ite, smul_eq_mul, mul_one, mul_zero, Fintype.sum_ite_eq']
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
⊢ normAtAllPlaces '' normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' s =
    (↑expMapBasis : realSpace K → realSpace K) '' s
have hs : ∀ x ∈ (↑expMapBasis : realSpace K → realSpace K) '' s, ∀ (w : InfinitePlace K), 0 ≤ x w
Tactic: apply normAtAllPlaces_image_preimage_of_nonneg
-- 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
⊢ ∏ 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)
have 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)
Tactic: rw [Finset.prod_mul_distrib]
-- 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
⊢ 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)
have 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))⁻¹
Tactic: congr 1
-- 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
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))⁻¹
⊢ 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)
have e_a₁ : ∏ x : InfinitePlace K, (↑x.mult : ℝ)⁻¹ = HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K)
Tactic: congr 1
-- 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
⊢ ∏ 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))⁻¹
have 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)) =
  HMul.hMul (α := ℝ) (∏ w : InfinitePlace K, (↑expMapBasis : realSpace K → realSpace K) x w ^ w.mult)
    (∏ w : { w : InfinitePlace K // w.IsComplex },
        (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹
Tactic: simp_rw [← prod_expMapBasis_pow, prod_eq_prod_mul_prod, expMapBasis_apply, expMap_apply,
      mult_isReal, mult_isComplex, pow_one, Finset.prod_pow, pow_two, mul_assoc, mul_inv_cancel₀
      (Finset.prod_ne_zero_iff.mpr <| fun _ _ ↦ Real.exp_ne_zero _), 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
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)) =
    HMul.hMul (α := ℝ) (∏ w : InfinitePlace K, (↑expMapBasis : realSpace K → realSpace K) x w ^ w.mult)
      (∏ w : { w : InfinitePlace K // w.IsComplex },
          (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace 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)) =
    Real.exp (x w₀) ^ finrank ℚ K *
      (∏ w : { w : InfinitePlace K // w.IsComplex },
          (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹
have e_a₁ : HMul.hMul (α := ℝ)
    (∏ w : { w : InfinitePlace K // w.IsReal },
      Real.exp
        (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)⁻¹
          ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
            (↑w : InfinitePlace K))))
    (∏ w : { w : InfinitePlace K // w.IsComplex },
      Real.exp
        (HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ)⁻¹
          ((LinearEquiv.symm (Basis.equivFun (completeBasis K)) : (a : InfinitePlace K → ℝ) → realSpace K) x
            (↑w : InfinitePlace K)))) =
  HMul.hMul (α := ℝ)
      (∏ w : { w : InfinitePlace K // w.IsReal },
        (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)
      (∏ w : { w : InfinitePlace K // w.IsComplex },
        (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult) *
    (∏ w : { w : InfinitePlace K // w.IsComplex },
        (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹
Tactic: simp_rw [← prod_expMapBasis_pow, prod_eq_prod_mul_prod, expMapBasis_apply, expMap_apply,
      mult_isReal, mult_isComplex, pow_one, Finset.prod_pow, pow_two, mul_assoc, mul_inv_cancel₀
      (Finset.prod_ne_zero_iff.mpr <| fun _ _ ↦ Real.exp_ne_zero _), 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
⊢ |(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
have 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
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]
-- 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 *
            (∏ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ ∫⁻ (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)
have 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)
Tactic: rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume hs
    (fun x _ ↦ (hasFDerivAt_expMapBasis K x).hasFDerivWithinAt) (injective_expMapBasis K).injOn]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ ∫⁻ (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)
have 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)
Tactic: simp_rw [abs_det_fderiv_expMapBasis]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (hypothesis)
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
⊢ ∫⁻ (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)
have this : Measurable.{u_1, u_1} (α := realSpace K) (↑expMapBasis : realSpace K → realSpace K)
Tactic: have : Measurable expMapBasis := (continuous_expMapBasis K).measurable
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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)
⊢ ∫⁻ (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)
have 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) =
  ∫⁻ (a : realSpace K) in s,
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
      (ENNReal.ofReal (Real.exp (a w₀ * (↑(finrank ℚ K) : ℝ))) *
          (∏ i : { w : InfinitePlace K // w.IsComplex },
              ENNReal.ofReal
                ((↑expMapBasis : realSpace K → realSpace K) (fun (w : InfinitePlace K) ↦ a w)
                  (↑i : InfinitePlace K)))⁻¹ *
        f ((↑expMapBasis : realSpace K → realSpace K) a))
Tactic: rw [← lintegral_const_mul _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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)
⊢ ∫⁻ (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) =
    ∫⁻ (a : realSpace K) in s,
      HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
        (ENNReal.ofReal (Real.exp (a w₀ * (↑(finrank ℚ K) : ℝ))) *
            (∏ i : { w : InfinitePlace K // w.IsComplex },
                ENNReal.ofReal
                  ((↑expMapBasis : realSpace K → realSpace K) (fun (w : InfinitePlace K) ↦ a w)
                    (↑i : InfinitePlace K)))⁻¹ *
          f ((↑expMapBasis : realSpace K → realSpace K) a))
have e_f : ∀ (x : realSpace K),
  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∞) *
      (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: congr with x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (hypothesis)
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)
x : realSpace K
⊢ 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∞) *
      (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))
have this₁ : LE.le (α := ℝ) 0
  (∏ w : { w : InfinitePlace K // w.IsComplex }, (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹
Tactic: have : 0 ≤ (∏ w : {w // IsComplex w}, expMapBasis x w.1)⁻¹ :=
    inv_nonneg.mpr <| Finset.prod_nonneg fun _ _ ↦ (expMapBasis_pos _ _).le