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
this : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
C : ℝ
hC :
  ∀ (x : realSpace K),
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x → ‖x‖ ≤ C
x : mixedSpace K
hx :
  Membership.mem (γ := Set (mixedSpace K))
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x
rw : (sup' univ ⋯ fun (w : InfinitePlace K) ↦ (normAtPlace w : (a : mixedSpace K) → ℝ) x) ≤ C
⊢ ‖x‖ ≤ C

Tactic:
rw [norm_eq_sup'_normAtPlace]

Premises used: NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
C : ℝ
hC :
  ∀ (x : realSpace K),
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x → ‖x‖ ≤ C
x : mixedSpace K
hx :
  Membership.mem (γ := Set (mixedSpace K))
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x
⊢ (sup' univ ⋯ fun (w : InfinitePlace K) ↦ (normAtPlace w : (a : mixedSpace K) → ℝ) x) ≤ C

Tactic:
sup'_le _ _ fun w _ ↦ ?_

Premises used: Finset.sup'_le
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
C : ℝ
hC :
  ∀ (x : realSpace K),
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x → ‖x‖ ≤ C
x : mixedSpace K
hx :
  Membership.mem (γ := Set (mixedSpace K))
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x
refine :
  ∀ (w : InfinitePlace K),
    Membership.mem (γ := Finset (InfinitePlace K)) univ w → (normAtPlace w : (a : mixedSpace K) → ℝ) x ≤ C
⊢ (sup' univ ⋯ fun (w : InfinitePlace K) ↦ (normAtPlace w : (a : mixedSpace K) → ℝ) x) ≤ C

Tactic:
refine sup'_le _ _ fun w _ ↦ ?_

Premises used: Finset.sup'_le
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
C : ℝ
hC :
  ∀ (x : realSpace K),
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x → ‖x‖ ≤ C
x : mixedSpace K
hx :
  Membership.mem (γ := Set (mixedSpace K))
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x
w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) univ w
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ) x ≤ C

Tactic:
simpa [normAtAllPlaces_apply, Real.norm_of_nonneg (normAtPlace_nonneg w x)]
      using (pi_norm_le_iff_of_nonempty _).mp (hC _ hx) w

Premises used: NumberField.mixedEmbedding.normAtAllPlaces_apply, pi_norm_le_iff_of_nonempty, NumberField.mixedEmbedding.normAtPlace_nonneg, Iff.mp, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
suffices : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
⊢ IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)

Tactic:
suffices IsBounded (expMapBasis '' paramSet K) by
    obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this
    refine isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩
    rw [norm_eq_sup'_normAtPlace]
    refine sup'_le _ _ fun w _ ↦ ?_
    simpa [normAtAllPlaces_apply, Real.norm_of_nonneg (normAtPlace_nonneg w x)]
      using (pi_norm_le_iff_of_nonempty _).mp (hC _ hx) w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)

Tactic:
IsBounded.subset ?_ (Set.image_mono subset_closure)

Premises used: subset_closure, Set.image_mono, Bornology.IsBounded.subset
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K))
⊢ IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)

Tactic:
refine IsBounded.subset ?_ (Set.image_mono subset_closure)

Premises used: subset_closure, Set.image_mono, Bornology.IsBounded.subset
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K))

Tactic:
(isCompact_compactSet K).isBounded.subset (expMapBasis_closure_subset_compactSet K)

Premises used: IsCompact.isBounded, NumberField.mixedEmbedding.fundamentalCone.isCompact_compactSet, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_closure_subset_compactSet, Bornology.IsBounded.subset
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K))

Tactic:
exact (isCompact_compactSet K).isBounded.subset (expMapBasis_closure_subset_compactSet K)

Premises used: IsCompact.isBounded, NumberField.mixedEmbedding.fundamentalCone.isCompact_compactSet, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_closure_subset_compactSet, Bornology.IsBounded.subset
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw rw₁ rw₂ :
  IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
rw₃ : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
rw₄ : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K))
⊢ IsBounded (α := mixedSpace K) (normLeOne K)

Tactic:
classical
  rw [normLeOne_eq_preimage]
  suffices IsBounded (expMapBasis '' paramSet K) by
    obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this
    refine isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩
    rw [norm_eq_sup'_normAtPlace]
    refine sup'_le _ _ fun w _ ↦ ?_
    simpa [normAtAllPlaces_apply, Real.norm_of_nonneg (normAtPlace_nonneg w x)]
      using (pi_norm_le_iff_of_nonempty _).mp (hC _ hx) w
  refine IsBounded.subset ?_ (Set.image_mono subset_closure)
  exact (isCompact_compactSet K).isBounded.subset (expMapBasis_closure_subset_compactSet K)

Premises used: IsCompact.isBounded, subset_closure, NumberField.mixedEmbedding.fundamentalCone.isCompact_compactSet, Set.image_mono, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_closure_subset_compactSet, Bornology.IsBounded.subset, NumberField.mixedEmbedding.fundamentalCone.normLeOne_eq_preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Measurable (β := ℝ≥0∞) fun (x : realSpace K) ↦
    ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
        ∫⁻ (x : realSpace K) in paramSet 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)))⁻¹ *
            ∏ w : { w : InfinitePlace K // w.IsComplex },
              ENNReal.ofReal ((↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normLeOne K) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)

Tactic:
rw [volume_eq_two_pow_mul_two_pi_pow_mul_integral (normLeOne_eq_preimage_image K).symm
    (measurableSet_normLeOne K), normLeOne_eq_preimage,
    normAtAllPlaces_image_preimage_expMapBasis,
    setLIntegral_expMapBasis_image (measurableSet_paramSet K) (by fun_prop)]

Premises used: NumberField.mixedEmbedding.fundamentalCone.normLeOne_eq_preimage_image, NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_image_preimage_expMapBasis, Eq.symm, NumberField.mixedEmbedding.fundamentalCone.measurableSet_paramSet, NumberField.mixedEmbedding.fundamentalCone.measurableSet_normLeOne, NumberField.mixedEmbedding.fundamentalCone.normLeOne_eq_preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
simp_rw :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
        ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ)))) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
⊢ HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * ENNReal.ofReal (regulator K) * (↑(finrank ℚ K) : ℝ≥0∞) *
        ∫⁻ (x : realSpace K) in paramSet 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)))⁻¹ *
            ∏ w : { w : InfinitePlace K // w.IsComplex },
              ENNReal.ofReal ((↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * (↑NNReal.pi : ℝ≥0∞) ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)

Tactic:
simp_rw [ENNReal.inv_mul_cancel_right
    (Finset.prod_ne_zero_iff.mpr fun _ _ ↦ ofReal_ne_zero_iff.mpr (expMapBasis_pos _ _))
    (prod_ne_top fun _ _ ↦ ofReal_ne_top)]

Premises used: Iff.mpr, Finset.prod_ne_zero_iff, ENNReal.prod_ne_top, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_pos, ENNReal.ofReal_ne_top, ENNReal.inv_mul_cancel_right, ENNReal.ofReal_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)

Tactic:
have h₁ : MeasurableSet (normAtAllPlaces ⁻¹' compactSet K) :=
    (isCompact_compactSet K).measurableSet.preimage (continuous_normAtAllPlaces K).measurable
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
⊢ MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))

Tactic:
MeasurableSet.preimage ?_ (continuous_normAtAllPlaces K).measurable

Premises used: MeasurableSet.preimage, Continuous.measurable, NumberField.mixedEmbedding.continuous_normAtAllPlaces
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
refine : MeasurableSet (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
⊢ MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))

Tactic:
refine MeasurableSet.preimage ?_ (continuous_normAtAllPlaces K).measurable

Premises used: MeasurableSet.preimage, Continuous.measurable, NumberField.mixedEmbedding.continuous_normAtAllPlaces
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
⊢ MeasurableSet (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))

Tactic:
MeasurableSet.image_of_continuousOn_injOn ?_ (continuous_expMapBasis K).continuousOn
      (injective_expMapBasis K).injOn

Premises used: Continuous.continuousOn, Function.Injective.injOn, NumberField.mixedEmbedding.fundamentalCone.continuous_expMapBasis, MeasurableSet.image_of_continuousOn_injOn, NumberField.mixedEmbedding.fundamentalCone.injective_expMapBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
refine : MeasurableSet (α := realSpace K) (interior (paramSet K))
⊢ MeasurableSet (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))

Tactic:
refine MeasurableSet.image_of_continuousOn_injOn ?_ (continuous_expMapBasis K).continuousOn
      (injective_expMapBasis K).injOn

Premises used: Continuous.continuousOn, Function.Injective.injOn, NumberField.mixedEmbedding.fundamentalCone.continuous_expMapBasis, MeasurableSet.image_of_continuousOn_injOn, NumberField.mixedEmbedding.fundamentalCone.injective_expMapBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
⊢ MeasurableSet (α := realSpace K) (interior (paramSet K))

Tactic:
measurableSet_interior

Premises used: measurableSet_interior
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
⊢ MeasurableSet (α := realSpace K) (interior (paramSet K))

Tactic:
exact measurableSet_interior

Premises used: measurableSet_interior
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
⊢ MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))

Tactic:
have h₂ : MeasurableSet (normAtAllPlaces ⁻¹' expMapBasis '' interior (paramSet K)) := by
    refine MeasurableSet.preimage ?_ (continuous_normAtAllPlaces K).measurable
    refine MeasurableSet.image_of_continuousOn_injOn ?_ (continuous_expMapBasis K).continuousOn
      (injective_expMapBasis K).injOn
    exact measurableSet_interior
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (closure (normLeOne K)) : ℝ≥0∞)

Tactic:
le_antisymm (measure_mono interior_subset_closure) ?_

Premises used: le_antisymm, MeasureTheory.measure_mono, interior_subset_closure
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
refine :
  LE.le (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (closure (normLeOne K)) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (closure (normLeOne K)) : ℝ≥0∞)

Tactic:
refine le_antisymm (measure_mono interior_subset_closure) ?_

Premises used: le_antisymm, MeasureTheory.measure_mono, interior_subset_closure
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
⊢ LE.le (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (closure (normLeOne K)) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)

Tactic:
(measure_mono (closure_normLeOne_subset K)).trans ?_

Premises used: NumberField.mixedEmbedding.fundamentalCone.closure_normLeOne_subset, MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
refine :
  LE.le (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normAtAllPlaces ⁻¹' compactSet K) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (closure (normLeOne K)) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)

Tactic:
refine (measure_mono (closure_normLeOne_subset K)).trans ?_

Premises used: NumberField.mixedEmbedding.fundamentalCone.closure_normLeOne_subset, MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
⊢ LE.le (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normAtAllPlaces ⁻¹' compactSet K) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)

Tactic:
le_of_eq_of_le ?_ (measure_mono (subset_interior_normLeOne K))

Premises used: NumberField.mixedEmbedding.fundamentalCone.subset_interior_normLeOne, MeasureTheory.measure_mono, le_of_eq_of_le
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
refine :
  Eq (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normAtAllPlaces ⁻¹' compactSet K) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K)) :
      ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (normAtAllPlaces ⁻¹' compactSet K) : ℝ≥0∞)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)

Tactic:
refine le_of_eq_of_le ?_ (measure_mono (subset_interior_normLeOne K))

Premises used: NumberField.mixedEmbedding.fundamentalCone.subset_interior_normLeOne, MeasureTheory.measure_mono, le_of_eq_of_le
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ : MeasurableSet (α := mixedSpace K) (normAtAllPlaces ⁻¹' compactSet K)
h₂ :
  MeasurableSet (α := mixedSpace K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
⊢ Measurable (β := ℝ≥0∞) fun (x : realSpace K) ↦
    ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Subset (α := Set (mixedSpace K)) (interior (normLeOne K)) (closure (normLeOne K))
h₂ : NullMeasurableSet (α := mixedSpace K) (interior (normLeOne K)) volume
h_fin :
  Ne (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (frontier (normLeOne K)) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [frontier, measure_diff, volume_interior_eq_volume_closure, tsub_self]

Premises used: frontier, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, tsub_self, MeasureTheory.measure_diff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (mixedSpace K)) (interior (normLeOne K)) (closure (normLeOne K))

Tactic:
interior_subset_closure

Premises used: interior_subset_closure
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (mixedSpace K)) (interior (normLeOne K)) (closure (normLeOne K))

Tactic:
exact interior_subset_closure

Premises used: interior_subset_closure
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ NullMeasurableSet (α := mixedSpace K) (interior (normLeOne K)) volume

Tactic:
measurableSet_interior.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, measurableSet_interior
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ NullMeasurableSet (α := mixedSpace K) (interior (normLeOne K)) volume

Tactic:
exact measurableSet_interior.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, measurableSet_interior
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Ne (α := ℝ≥0∞) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (interior (normLeOne K)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
lt_top_iff_ne_top.mp <| lt_of_le_of_lt (measure_mono interior_subset) ?_

Premises used: lt_of_le_of_lt, interior_subset, lt_top_iff_ne_top, MeasureTheory.measure_mono, Iff.mp