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
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)
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))
⊢ ∫⁻ (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:
rw [← lintegral_const_mul _ (by fun_prop)]

Premises used: MeasureTheory.lintegral_const_mul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this : Measurable.{u_1, u_1} (α := realSpace K) (↑expMapBasis : realSpace K → realSpace K)
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))
⊢ ∫⁻ (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:
congr with x
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this : Measurable.{u_1, u_1} (α := realSpace K) (↑expMapBasis : realSpace K → realSpace K)
x : realSpace K
⊢ 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
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this_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))⁻¹
⊢ 0 ≤
    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) : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this_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))⁻¹
⊢ 0 ≤
    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:
positivity
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this_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))⁻¹
⊢ 0 ≤
    Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ)) *
      (∏ w : { w : InfinitePlace K // w.IsComplex },
          (↑expMapBasis : realSpace K → realSpace K) x (↑w : InfinitePlace K))⁻¹

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this_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))⁻¹
⊢ 0 ≤ Real.exp (x w₀ * (↑(finrank ℚ K) : ℝ))

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this_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))⁻¹
⊢ LE.le (α := ℝ) 0 2⁻¹

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this_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))⁻¹
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))
⊢ 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:
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)]

Premises used: ENNReal.ofReal_mul, LT.lt.le, ENNReal.ofReal_ofNat, ENNReal.ofReal_inv_of_pos, ENNReal.ofReal_prod_of_nonneg, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_pos, Finset.prod_pos, zero_lt_two, ENNReal.ofReal_natCast, ENNReal.ofReal_pow
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this_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) : ℝ))) *
              (∏ 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:
ring
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurableSet (α := realSpace K) (paramSet K)

Tactic:
MeasurableSet.univ_pi fun _ ↦ ?_

Premises used: MeasurableSet.univ_pi
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine : ∀ (x : InfinitePlace K), MeasurableSet (α := ℝ) (if x = w₀ then Set.Iic 0 else Set.Ico 0 1)
⊢ MeasurableSet (α := realSpace K) (paramSet K)

Tactic:
refine MeasurableSet.univ_pi fun _ ↦ ?_

Premises used: MeasurableSet.univ_pi
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
pos : x = w₀ → MeasurableSet (α := ℝ) (Set.Iic 0)
neg : ¬x = w₀ → MeasurableSet (α := ℝ) (Set.Ico 0 1)
⊢ MeasurableSet (α := ℝ) (if x = w₀ then Set.Iic 0 else Set.Ico 0 1)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : x = w₀
⊢ MeasurableSet (α := ℝ) (Set.Iic 0)

Tactic:
measurableSet_Iic

Premises used: measurableSet_Iic
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : x = w₀
⊢ MeasurableSet (α := ℝ) (Set.Iic 0)

Tactic:
exact measurableSet_Iic

Premises used: measurableSet_Iic
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : ¬x = w₀
⊢ MeasurableSet (α := ℝ) (Set.Ico 0 1)

Tactic:
measurableSet_Ico

Premises used: measurableSet_Ico
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : ¬x = w₀
⊢ MeasurableSet (α := ℝ) (Set.Ico 0 1)

Tactic:
exact measurableSet_Ico

Premises used: measurableSet_Ico
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Set (realSpace K)) (interior (paramSet K))
    (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:
simp [interior_pi_set Set.finite_univ, apply_ite]

Premises used: apply_ite, Set.finite_univ, interior_pi_set
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Set (realSpace K)) (closure (paramSet 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)

Tactic:
simp [closure_pi_set, apply_ite]

Premises used: apply_ite, closure_pi_set
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
⊢ Eq (α := Set (realSpace K)) (normAtAllPlaces '' normLeOne K)
    ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
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
⊢ 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
-- 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
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)
⊢ Membership.mem (γ := Set (realSpace K)) (normAtAllPlaces '' normLeOne K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x

Tactic:
rw [← expMapBasis.right_inv (Set.mem_univ_pi.mpr hx), (injective_expMapBasis K).mem_set_image]

Premises used: Iff.mpr, NumberField.mixedEmbedding.fundamentalCone.injective_expMapBasis, NumberField.mixedEmbedding.fundamentalCone.expMapBasis, Set.mem_univ_pi, Function.Injective.mem_set_image, OpenPartialHomeomorph.right_inv
-- 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
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)
⊢ 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:
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]

Premises used: and_true, Set.mem_inter_iff, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, false_and, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, pow_eq_zero_iff', Set.mem_setOf_eq, ne_eq, LT.lt.ne', pow_le_one_iff_of_nonneg, Real.exp_nonneg, implies_true, Real.exp_le_one_iff, not_false_eq_true, Set.mem_univ_pi, Module.finrank_pos, Set.mem_preimage, Real.exp_ne_zero, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_nonneg, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne
-- 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 :
  ∀ (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)
w : InfinitePlace K
hw : ¬w = w₀
⊢ Membership.mem (γ := Set ℝ) (Set.Ico 0 1)
    ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)

Tactic:
simpa [hw] using h w
-- 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 :
  ∀ (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)
⊢ (↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w₀ ≤ 0

Tactic:
simpa using h w₀

Premises used: NumberField.Units.dirichletUnitTheorem.w₀
-- 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
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)
⊢ (∀ (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:
refine ⟨fun ⟨h₁, h₂⟩ w ↦ ?_, fun h ↦ ⟨fun w hw ↦ by simpa [hw] using h w, by simpa using h w₀⟩⟩
-- 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
pos :
  ∀ (hw : w = w₀),
    Membership.mem (γ := Set ℝ) (Set.Iic 0)
      ((↑(OpenPartialHomeomorph.symm expMapBasis) : realSpace K → realSpace K) x w)
neg :
  ∀ (hw : ¬w = w₀),
    Membership.mem (γ := Set ℝ) (Set.Ico 0 1)
      ((↑(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)

Tactic:
split_ifs with hw