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
hx : ∀ (w : InfinitePlace K), 0 < x w
h :
  (∀ (w : InfinitePlace K),
      ¬w = w₀ →
        Membership.mem (γ := Set ℝ) (Set.Ico 0 1)
          ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)) ∧
    (↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w₀ ≤ 0
w : InfinitePlace K
h₁ :
  ∀ (w : InfinitePlace K),
    ¬w = w₀ →
      Membership.mem (γ := Set ℝ) (Set.Ico 0 1)
        ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)
h₂ : (↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w₀ ≤ 0
hw : w = w₀
⊢ Membership.mem (γ := Set ℝ) (Set.Iic 0) ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)

Tactic:
hw ▸ h₂

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
h :
  (∀ (w : InfinitePlace K),
      ¬w = w₀ →
        Membership.mem (γ := Set ℝ) (Set.Ico 0 1)
          ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)) ∧
    (↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w₀ ≤ 0
w : InfinitePlace K
h₁ :
  ∀ (w : InfinitePlace K),
    ¬w = w₀ →
      Membership.mem (γ := Set ℝ) (Set.Ico 0 1)
        ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)
h₂ : (↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w₀ ≤ 0
hw : w = w₀
⊢ Membership.mem (γ := Set ℝ) (Set.Iic 0) ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)

Tactic:
exact hw ▸ h₂
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
h :
  (∀ (w : InfinitePlace K),
      ¬w = w₀ →
        Membership.mem (γ := Set ℝ) (Set.Ico 0 1)
          ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)) ∧
    (↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w₀ ≤ 0
w : InfinitePlace K
h₁ :
  ∀ (w : InfinitePlace K),
    ¬w = w₀ →
      Membership.mem (γ := Set ℝ) (Set.Ico 0 1)
        ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)
h₂ : (↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w₀ ≤ 0
hw : ¬w = w₀
⊢ Membership.mem (γ := Set ℝ) (Set.Ico 0 1)
    ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)

Tactic:
h₁ w hw
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
h :
  (∀ (w : InfinitePlace K),
      ¬w = w₀ →
        Membership.mem (γ := Set ℝ) (Set.Ico 0 1)
          ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)) ∧
    (↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w₀ ≤ 0
w : InfinitePlace K
h₁ :
  ∀ (w : InfinitePlace K),
    ¬w = w₀ →
      Membership.mem (γ := Set ℝ) (Set.Ico 0 1)
        ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)
h₂ : (↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w₀ ≤ 0
hw : ¬w = w₀
⊢ Membership.mem (γ := Set ℝ) (Set.Ico 0 1)
    ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)

Tactic:
exact h₁ w hw
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx : ¬∀ (w : InfinitePlace K), 0 < x w
⊢ Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx : ¬∀ (w : InfinitePlace K), 0 < x w
neg :
  Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x →
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x
neg₁ :
  Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x →
    Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x
⊢ Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : mixedSpace K
ha : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) a
right :
  Membership.mem (γ := Set (mixedSpace K))
    {x : mixedSpace K | LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)} a
hx : ¬∀ (w : InfinitePlace K), 0 < normAtAllPlaces a w
⊢ Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) (normAtAllPlaces a)

Tactic:
(hx fun w ↦ fundamentalCone.normAtPlace_pos_of_mem ha w).elim

Premises used: False.elim, NumberField.mixedEmbedding.fundamentalCone.normAtPlace_pos_of_mem
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : mixedSpace K
ha : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) a
right :
  Membership.mem (γ := Set (mixedSpace K))
    {x : mixedSpace K | LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)} a
hx : ¬∀ (w : InfinitePlace K), 0 < normAtAllPlaces a w
⊢ Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) (normAtAllPlaces a)

Tactic:
exact (hx fun w ↦ fundamentalCone.normAtPlace_pos_of_mem ha w).elim

Premises used: False.elim, NumberField.mixedEmbedding.fundamentalCone.normAtPlace_pos_of_mem
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : realSpace K
left : Membership.mem (γ := Set (realSpace K)) (paramSet K) a
hx : ¬∀ (w : InfinitePlace K), 0 < (↑expMapBasis : realSpace K → realSpace K) a w
⊢ Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K)
    ((↑expMapBasis : realSpace K → realSpace K) a)

Tactic:
(hx fun w ↦ expMapBasis_pos a w).elim

Premises used: False.elim, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : realSpace K
left : Membership.mem (γ := Set (realSpace K)) (paramSet K) a
hx : ¬∀ (w : InfinitePlace K), 0 < (↑expMapBasis : realSpace K → realSpace K) a w
⊢ Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K)
    ((↑expMapBasis : realSpace K → realSpace K) a)

Tactic:
exact (hx fun w ↦ expMapBasis_pos a w).elim

Premises used: False.elim, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Eq (α := Set (mixedSpace K)) (normAtAllPlaces ⁻¹' normAtAllPlaces '' normLeOne K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
rw₁ rw₂ :
  Eq (α := Set (mixedSpace K)) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
⊢ Eq (α := Set (mixedSpace K)) (normLeOne K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)

Tactic:
rw [normLeOne_eq_preimage_image, normAtAllPlaces_normLeOne_eq_image]

Premises used: NumberField.mixedEmbedding.fundamentalCone.normLeOne_eq_preimage_image, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne_eq_image
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Subset (α := Set (mixedSpace K))
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
    (interior (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K))
⊢ Subset (α := Set (mixedSpace K))
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K)) (interior (normLeOne K))

Tactic:
rw [normLeOne_eq_preimage]

Premises used: NumberField.mixedEmbedding.fundamentalCone.normLeOne_eq_preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (mixedSpace K))
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
    (interior (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K))

Tactic:
subset_trans (Set.preimage_mono ?_) <|
    preimage_interior_subset_interior_preimage (continuous_normAtAllPlaces K)

Premises used: subset_trans, preimage_interior_subset_interior_preimage, Set.preimage_mono, NumberField.mixedEmbedding.continuous_normAtAllPlaces
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine :
  Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
    (interior ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K))
⊢ Subset (α := Set (mixedSpace K))
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
    (interior (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K))

Tactic:
refine subset_trans (Set.preimage_mono ?_) <|
    preimage_interior_subset_interior_preimage (continuous_normAtAllPlaces K)

Premises used: subset_trans, preimage_interior_subset_interior_preimage, Set.preimage_mono, NumberField.mixedEmbedding.continuous_normAtAllPlaces
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (realSpace K)) (interior (paramSet K))
    (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv expMapBasis))

Tactic:
simp [expMapBasis_source]

Premises used: NumberField.mixedEmbedding.fundamentalCone.expMapBasis_source
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsOpen (X := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))

Tactic:
have : IsOpen (expMapBasis '' (interior (paramSet K))) :=
    expMapBasis.isOpen_image_of_subset_source isOpen_interior (by simp [expMapBasis_source])
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : IsOpen (X := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
⊢ Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
    (interior ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K))

Tactic:
interior_maximal (Set.image_mono interior_subset) this

Premises used: interior_subset, Set.image_mono, interior_maximal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : IsOpen (X := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
⊢ Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
    (interior ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K))

Tactic:
exact interior_maximal (Set.image_mono interior_subset) this

Premises used: interior_subset, Set.image_mono, interior_maximal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w = w₀ then Set.Iic 0
      else
        Set.Icc 0
          1) =ᶠ[ae (F := Measure (realSpace K))
      (Measure.pi (α := fun (a : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume)]
    Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w = w₀ then Set.Iio 0 else Set.Ioo 0 1
⊢ closure (paramSet K) =ᶠ[ae (F := Measure (realSpace K)) volume] interior (paramSet K)

Tactic:
rw [closure_paramSet, interior_paramSet, volume_pi]

Premises used: NumberField.mixedEmbedding.fundamentalCone.interior_paramSet, MeasureTheory.volume_pi, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w = w₀ then Set.Iic 0
      else
        Set.Icc 0
          1) =ᶠ[ae (F := Measure (realSpace K))
      (Measure.pi (α := fun (a : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume)]
    Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w = w₀ then Set.Iio 0 else Set.Ioo 0 1

Tactic:
Measure.ae_eq_set_pi fun w _ ↦ ?_

Premises used: MeasureTheory.Measure.ae_eq_set_pi
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine :
  ∀ (w : InfinitePlace K),
    Membership.mem (γ := Set (InfinitePlace K)) Set.univ w →
      (if w = w₀ then Set.Iic 0 else Set.Icc 0 1) =ᶠ[ae (F := Measure ℝ) volume]
        if w = w₀ then Set.Iio 0 else Set.Ioo 0 1
⊢ (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w = w₀ then Set.Iic 0
      else
        Set.Icc 0
          1) =ᶠ[ae (F := Measure (realSpace K))
      (Measure.pi (α := fun (a : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume)]
    Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w = w₀ then Set.Iio 0 else Set.Ioo 0 1

Tactic:
refine Measure.ae_eq_set_pi fun w _ ↦ ?_

Premises used: MeasureTheory.Measure.ae_eq_set_pi
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
h : Membership.mem (γ := Set (InfinitePlace K)) Set.univ w
pos : w = w₀ → Set.Iic 0 =ᶠ[ae (F := Measure ℝ) volume] Set.Iio 0
neg : ¬w = w₀ → Set.Icc 0 1 =ᶠ[ae (F := Measure ℝ) volume] Set.Ioo 0 1
⊢ (if w = w₀ then Set.Iic 0 else Set.Icc 0 1) =ᶠ[ae (F := Measure ℝ) volume] if w = w₀ then Set.Iio 0 else Set.Ioo 0 1

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
h : Membership.mem (γ := Set (InfinitePlace K)) Set.univ w
h_1 : w = w₀
⊢ Set.Iic 0 =ᶠ[ae (F := Measure ℝ) volume] Set.Iio 0

Tactic:
Iio_ae_eq_Iic.symm

Premises used: Filter.EventuallyEq.symm, MeasureTheory.Iio_ae_eq_Iic
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
h : Membership.mem (γ := Set (InfinitePlace K)) Set.univ w
h_1 : w = w₀
⊢ Set.Iic 0 =ᶠ[ae (F := Measure ℝ) volume] Set.Iio 0

Tactic:
exact Iio_ae_eq_Iic.symm

Premises used: Filter.EventuallyEq.symm, MeasureTheory.Iio_ae_eq_Iic
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
h : Membership.mem (γ := Set (InfinitePlace K)) Set.univ w
h_1 : ¬w = w₀
⊢ Set.Icc 0 1 =ᶠ[ae (F := Measure ℝ) volume] Set.Ioo 0 1

Tactic:
Ioo_ae_eq_Icc.symm

Premises used: MeasureTheory.Ioo_ae_eq_Icc, Filter.EventuallyEq.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
h : Membership.mem (γ := Set (InfinitePlace K)) Set.univ w
h_1 : ¬w = w₀
⊢ Set.Icc 0 1 =ᶠ[ae (F := Measure ℝ) volume] Set.Ioo 0 1

Tactic:
exact Ioo_ae_eq_Icc.symm

Premises used: MeasureTheory.Ioo_ae_eq_Icc, Filter.EventuallyEq.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn : 0 < n
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
have hn : 0 < (n : ℝ) := Nat.cast_pos.mpr hn
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn_1 : 0 < n
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ Measurable (β := ℝ≥0∞) fun (x : realSpace K) ↦ ENNReal.ofReal (Real.exp (x w₀ * (↑n : ℝ)))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn_1 : 0 < n
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw :
  lmarginal (X := fun (a : InfinitePlace K) ↦ ℝ)
      (fun (i : InfinitePlace K) ↦ Measure.restrict volume (if i = w₀ then Set.Iic 0 else Set.Ico 0 1)) (erase univ w₀)
      (fun (x : (i : InfinitePlace K) → ℝ) ↦
        ∫⁻ (xᵢ : ℝ) in Set.Iic 0,
          ENNReal.ofReal (Real.exp (Function.update (β := fun (a : InfinitePlace K) ↦ ℝ) x w₀ xᵢ w₀ * (↑n : ℝ))))
      0 =
    (↑n : ℝ≥0∞)⁻¹
⊢ ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑n : ℝ))) = (↑n : ℝ≥0∞)⁻¹

Tactic:
rw [volume_pi, paramSet, Measure.restrict_pi_pi, lintegral_eq_lmarginal_univ 0,
    lmarginal_erase' _ (by fun_prop) (Finset.mem_univ w₀), if_pos rfl]

Premises used: Finset.mem_univ, MeasureTheory.volume_pi, MeasureTheory.lintegral_eq_lmarginal_univ, MeasureTheory.Measure.restrict_pi_pi, MeasureTheory.lmarginal_erase', if_pos, NumberField.Units.dirichletUnitTheorem.w₀, NumberField.mixedEmbedding.fundamentalCone.paramSet, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn_1 : 0 < n
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
simp_rw : ∫⁻ (xᵢ : ℝ) in Set.Iic 0, ENNReal.ofReal (Real.exp ((↑n : ℝ) * xᵢ)) = (↑n : ℝ≥0∞)⁻¹
⊢ lmarginal (X := fun (a : InfinitePlace K) ↦ ℝ)
      (fun (i : InfinitePlace K) ↦ Measure.restrict volume (if i = w₀ then Set.Iic 0 else Set.Ico 0 1)) (erase univ w₀)
      (fun (x : (i : InfinitePlace K) → ℝ) ↦
        ∫⁻ (xᵢ : ℝ) in Set.Iic 0,
          ENNReal.ofReal (Real.exp (Function.update (β := fun (a : InfinitePlace K) ↦ ℝ) x w₀ xᵢ w₀ * (↑n : ℝ))))
      0 =
    (↑n : ℝ≥0∞)⁻¹

Tactic:
simp_rw [Function.update_self, lmarginal, lintegral_const, Measure.pi_univ, if_neg
    (Finset.ne_of_mem_erase (Subtype.prop _)), Measure.restrict_apply_univ, Real.volume_Ico,
    sub_zero, ofReal_one, prod_const_one, mul_one, mul_comm _ (n : ℝ)]

Premises used: MeasureTheory.lintegral_const, sub_zero, Finset.ne_of_mem_erase, Real.volume_Ico, MeasureTheory.Measure.restrict_apply_univ, MeasureTheory.Measure.pi_univ, Nat.cast, ENNReal.ofReal_one, Finset.prod_const_one, Subtype.prop, MeasureTheory.lmarginal, mul_comm, Function.update_self, mul_one, if_neg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn_1 : 0 < n
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw :
  (ae (F := Measure ℝ) (Measure.restrict volume (Set.Iic 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    Real.exp ((↑n : ℝ) * x)
⊢ ∫⁻ (xᵢ : ℝ) in Set.Iic 0, ENNReal.ofReal (Real.exp ((↑n : ℝ) * xᵢ)) = (↑n : ℝ≥0∞)⁻¹

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal (integrableOn_exp_mul_Iic hn _), integral_exp_mul_Iic
    hn, mul_zero, Real.exp_zero, ofReal_div_of_pos hn, ofReal_one, ofReal_natCast, one_div]

Premises used: integrableOn_exp_mul_Iic, integral_exp_mul_Iic, ENNReal.ofReal_div_of_pos, ENNReal.ofReal_one, MulZeroClass.mul_zero, MeasureTheory.ofReal_integral_eq_lintegral_ofReal, one_div, Real.exp_zero, ENNReal.ofReal_natCast
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn_1 : 0 < n
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
a : ℝ
⊢ 0 a ≤ Real.exp ((↑n : ℝ) * a)

Tactic:
Real.exp_nonneg _

Premises used: Real.exp_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn_1 : 0 < n
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ | (fun (x : ℝ) ↦ LE.le (α := ℝ) (0 x) ((fun (x : ℝ) ↦ Real.exp ((↑n : ℝ) * x)) x)) x} a
h₁ h₂ : ∀ (a : ℝ), 0 a ≤ Real.exp ((↑n : ℝ) * a)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Set.Iic 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    Real.exp ((↑n : ℝ) * x)

Tactic:
filter_upwards with _ using Real.exp_nonneg _

Premises used: Real.exp_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn : 0 < n
have have₁ have₂ :
  ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)),
    ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑n : ℝ))) = (↑n : ℝ≥0∞)⁻¹
have₃ :
  ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)),
    lmarginal (X := fun (a : InfinitePlace K) ↦ ℝ)
        (fun (i : InfinitePlace K) ↦ Measure.restrict volume (if i = w₀ then Set.Iic 0 else Set.Ico 0 1))
        (erase univ w₀)
        (fun (x : (i : InfinitePlace K) → ℝ) ↦
          ∫⁻ (xᵢ : ℝ) in Set.Iic 0,
            ENNReal.ofReal (Real.exp (Function.update (β := fun (a : InfinitePlace K) ↦ ℝ) x w₀ xᵢ w₀ * (↑n : ℝ))))
        0 =
      (↑n : ℝ≥0∞)⁻¹
have₄ :
  ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)),
    ∫⁻ (xᵢ : ℝ) in Set.Iic 0, ENNReal.ofReal (Real.exp ((↑n : ℝ) * xᵢ)) = (↑n : ℝ≥0∞)⁻¹
have₅ :
  ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)),
    (ae (F := Measure ℝ) (Measure.restrict volume (Set.Iic 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
      Real.exp ((↑n : ℝ) * x)
⊢ ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑n : ℝ))) = (↑n : ℝ≥0∞)⁻¹

Tactic:
classical
  have hn : 0 < (n : ℝ) := Nat.cast_pos.mpr hn
  rw [volume_pi, paramSet, Measure.restrict_pi_pi, lintegral_eq_lmarginal_univ 0,
    lmarginal_erase' _ (by fun_prop) (Finset.mem_univ w₀), if_pos rfl]
  simp_rw [Function.update_self, lmarginal, lintegral_const, Measure.pi_univ, if_neg
    (Finset.ne_of_mem_erase (Subtype.prop _)), Measure.restrict_apply_univ, Real.volume_Ico,
    sub_zero, ofReal_one, prod_const_one, mul_one, mul_comm _ (n : ℝ)]
  rw [← ofReal_integral_eq_lintegral_ofReal (integrableOn_exp_mul_Iic hn _), integral_exp_mul_Iic
    hn, mul_zero, Real.exp_zero, ofReal_div_of_pos hn, ofReal_one, ofReal_natCast, one_div]
  filter_upwards with _ using Real.exp_nonneg _

Premises used: Finset.mem_univ, MeasureTheory.lintegral_const, MeasureTheory.volume_pi, integrableOn_exp_mul_Iic, integral_exp_mul_Iic, sub_zero, MeasureTheory.lintegral_eq_lmarginal_univ, ENNReal.ofReal_div_of_pos, Finset.ne_of_mem_erase, Real.volume_Ico, MeasureTheory.Measure.restrict_pi_pi, MeasureTheory.Measure.restrict_apply_univ, MeasureTheory.Measure.pi_univ, MeasureTheory.lmarginal_erase', if_pos, Nat.cast, ENNReal.ofReal_one, MulZeroClass.mul_zero, Finset.prod_const_one, NumberField.Units.dirichletUnitTheorem.w₀, MeasureTheory.ofReal_integral_eq_lintegral_ofReal, Subtype.prop, MeasureTheory.lmarginal, one_div, NumberField.mixedEmbedding.fundamentalCone.paramSet, mul_comm, Real.exp_nonneg, Real.exp_zero, Function.update_self, mul_one, OfNat.ofNat, if_neg, ENNReal.ofReal_natCast, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsCompact (X := realSpace K) (compactSet K)

Tactic:
isCompact_Icc.smul_set <| (isCompact_univ_pi fun w ↦ ?_).image_of_continuousOn
    (continuous_expMapBasis K).continuousOn

Premises used: Continuous.continuousOn, isCompact_univ_pi, CompactIccSpace.isCompact_Icc, NumberField.mixedEmbedding.fundamentalCone.continuous_expMapBasis, IsCompact.image_of_continuousOn, IsCompact.smul_set