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
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this_1 : Measurable.{u_1, u_1} (α := realSpace K) (↑expMapBasis : realSpace K → realSpace K)
x : realSpace K
this :
  LE.le (α := ℝ) 0
    (∏ w : { w : InfinitePlace K // w.IsComplex },
        (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace 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 e_f : ENNReal.ofReal (Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ))) *
            (∏ i : { w : InfinitePlace K // w.IsComplex },
                ENNReal.ofReal ((↑expMapBasis : realSpace K → realSpace K) x (↑i : InfinitePlace K)))⁻¹ *
          HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) *
        (↑(finrank ℚ K) : ℝ≥0∞) *
      ENNReal.ofReal (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: rw [ofReal_mul (by positivity), ofReal_mul (by positivity), ofReal_mul (by positivity),
    ofReal_mul (by positivity), ofReal_pow (by positivity), ofReal_inv_of_pos (Finset.prod_pos
    fun _ _ ↦ expMapBasis_pos _ _), ofReal_inv_of_pos zero_lt_two, ofReal_ofNat, ofReal_natCast,
    ofReal_prod_of_nonneg (fun _ _ ↦ (expMapBasis_pos _ _).le)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurableSet (α := realSpace K) (paramSet K)
have refine : ∀ (x : InfinitePlace K), MeasurableSet (α := ℝ) (if x = w₀ then Set.Iic 0 else Set.Ico 0 1)
Tactic: refine MeasurableSet.univ_pi fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
⊢ MeasurableSet (α := ℝ) (if x = w₀ then Set.Iic 0 else Set.Ico 0 1)
have pos : x = w₀ → MeasurableSet (α := ℝ) (Set.Iic 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
pos : x = w₀ → MeasurableSet (α := ℝ) (Set.Iic 0)
⊢ MeasurableSet (α := ℝ) (if x = w₀ then Set.Iic 0 else Set.Ico 0 1)
have neg : ¬x = w₀ → MeasurableSet (α := ℝ) (Set.Ico 0 1)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Set (realSpace K)) (normAtAllPlaces '' normLeOne K)
    ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
have h : ∀ (x : realSpace K),
  Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x
Tactic: ext x
-- 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
⊢ Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x
have pos : ∀ (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: by_cases hx : ∀ w, 0 < x w
-- 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
pos :
  ∀ (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
⊢ Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x
have neg : ∀ (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: by_cases hx : ∀ w, 0 < x w
-- 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
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
have pos : Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K)
    ((↑expMapBasis : realSpace K → realSpace K)
      ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x)) ↔
  Membership.mem (γ := Set (realSpace K)) (paramSet K)
    ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x)
Tactic: rw [← expMapBasis.right_inv (Set.mem_univ_pi.mpr hx), (injective_expMapBasis K).mem_set_image]
-- 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
hx : ∀ (w : InfinitePlace K), 0 < x w
⊢ Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K)
      ((↑expMapBasis : realSpace K → realSpace K)
        ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x)) ↔
    Membership.mem (γ := Set (realSpace K)) (paramSet K)
      ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x)
have pos : (∀ (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 ↔
  ∀ (i : InfinitePlace K),
    Membership.mem (γ := Set ℝ) (if i = w₀ then Set.Iic 0 else Set.Ico 0 1)
      ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x i)
Tactic: simp only [normAtAllPlaces_normLeOne, Set.mem_inter_iff, Set.mem_setOf_eq, expMapBasis_nonneg,
      Set.mem_preimage, logMap_expMapBasis, implies_true, and_true, norm_expMapBasis,
      pow_le_one_iff_of_nonneg (Real.exp_nonneg _) Module.finrank_pos.ne', Real.exp_le_one_iff,
      ne_eq, pow_eq_zero_iff', Real.exp_ne_zero, false_and, not_false_eq_true, Set.mem_univ_pi]
-- 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
hx : ∀ (w : InfinitePlace K), 0 < x w
⊢ (∀ (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 ↔
    ∀ (i : InfinitePlace K),
      Membership.mem (γ := Set ℝ) (if i = w₀ then Set.Iic 0 else Set.Ico 0 1)
        ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x i)
have pos : (∀ (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),
    Membership.mem (γ := Set ℝ) (if w = w₀ then Set.Iic 0 else Set.Ico 0 1)
      ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)
Tactic: refine ⟨fun ⟨h₁, h₂⟩ w ↦ ?_, fun h ↦ ⟨fun w hw ↦ by simpa [hw] using h w, by simpa using h w₀⟩⟩
-- 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
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
⊢ Membership.mem (γ := Set ℝ) (if w = w₀ then Set.Iic 0 else Set.Ico 0 1)
    ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)
have pos : ∀ (hw : w = w₀),
  Membership.mem (γ := Set ℝ) (Set.Iic 0) ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)
Tactic: split_ifs with hw
-- 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
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
pos :
  ∀ (hw : w = w₀),
    Membership.mem (γ := Set ℝ) (Set.Iic 0)
      ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)
⊢ Membership.mem (γ := Set ℝ) (if w = w₀ then Set.Iic 0 else Set.Ico 0 1)
    ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)
have neg : ∀ (hw : ¬w = w₀),
  Membership.mem (γ := Set ℝ) (Set.Ico 0 1)
    ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)
Tactic: split_ifs with hw
-- 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
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
have neg : Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x →
  Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x
Tactic: refine ⟨?_, ?_⟩
-- 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
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
⊢ Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x
have neg₁ : Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x →
  Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Set (mixedSpace K)) (normLeOne K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
have rw : Eq (α := Set (mixedSpace K)) (normAtAllPlaces ⁻¹' normAtAllPlaces '' normLeOne K)
  (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
Tactic: rw [normLeOne_eq_preimage_image, normAtAllPlaces_normLeOne_eq_image]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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)
⊢ Eq (α := Set (mixedSpace K)) (normLeOne K)
    (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
have rw₁ : Eq (α := Set (mixedSpace K)) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
  (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
Tactic: rw [normLeOne_eq_preimage_image, normAtAllPlaces_normLeOne_eq_image]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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 (normLeOne K))
have rw : Subset (α := Set (mixedSpace K))
  (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
  (interior (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K))
Tactic: rw [normLeOne_eq_preimage]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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))
have refine : Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
  (interior ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K))
Tactic: refine subset_trans (Set.preimage_mono ?_) <|
    preimage_interior_subset_interior_preimage (continuous_normAtAllPlaces K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' interior (paramSet K))
    (interior ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K))
have this : 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])
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ closure (paramSet K) =ᶠ[ae (F := Measure (realSpace K)) volume] interior (paramSet K)
have 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
Tactic: rw [closure_paramSet, interior_paramSet, volume_pi]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
have 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
Tactic: refine Measure.ae_eq_set_pi fun w _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
h : 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
have pos : w = w₀ → Set.Iic 0 =ᶠ[ae (F := Measure ℝ) volume] Set.Iio 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ (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
have neg : ¬w = w₀ → Set.Icc 0 1 =ᶠ[ae (F := Measure ℝ) volume] Set.Ioo 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn : 0 < n
⊢ ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑n : ℝ))) = (↑n : ℝ≥0∞)⁻¹
have hn₁ : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: have hn : 0 < (n : ℝ) := Nat.cast_pos.mpr hn
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn_1 : 0 < n
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑n : ℝ))) = (↑n : ℝ≥0∞)⁻¹
have 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∞)⁻¹
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn_1 : 0 < n
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 simp_rw : ∫⁻ (xᵢ : ℝ) in Set.Iic 0, ENNReal.ofReal (Real.exp ((↑n : ℝ) * xᵢ)) = (↑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 : ℝ)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn_1 : 0 < n
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ ∫⁻ (xᵢ : ℝ) in Set.Iic 0, ENNReal.ofReal (Real.exp ((↑n : ℝ) * xᵢ)) = (↑n : ℝ≥0∞)⁻¹
have rw : (ae (F := Measure ℝ) (Measure.restrict volume (Set.Iic 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
  Real.exp ((↑n : ℝ) * x)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn_1 : 0 < n
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Set.Iic 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    Real.exp ((↑n : ℝ) * x)
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ | (fun (x : ℝ) ↦ LE.le (α := ℝ) (0 x) ((fun (x : ℝ) ↦ Real.exp ((↑n : ℝ) * x)) x)) x} a
Tactic: filter_upwards with _ using Real.exp_nonneg _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Set.Iic 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    Real.exp ((↑n : ℝ) * x)
have h₁ : ∀ (a : ℝ), 0 a ≤ Real.exp ((↑n : ℝ) * a)
Tactic: filter_upwards with _ using Real.exp_nonneg _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn : 0 < n
⊢ ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑n : ℝ))) = (↑n : ℝ≥0∞)⁻¹
have have : ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)),
  ∫⁻ (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 _