awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
rw :
  logMap
      (HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K)
        x) =
    HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
        logSpace K)
      (logMap x)
rw₁ :
  HAdd.hAdd (α := logSpace K)
      (logMap ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K))))
      (logMap x) =
    HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
        logSpace K)
      (logMap x)
rw₂ rw₃ :
  HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
        logSpace K)
      (logMap x) =
    HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
        logSpace K)
      (logMap x)
⊢ logMap (u • x) =
    HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
        logSpace K)
      (logMap x)

Tactic:
rw [unitSMul_smul, logMap_mul (by rw [norm_unit]; norm_num) hx, logMap_eq_logEmbedding]

Premises used: NumberField.mixedEmbedding.logMap_eq_logEmbedding, NumberField.mixedEmbedding.unitSMul_smul, NumberField.mixedEmbedding.logMap_mul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
h : ∀ (x_1 : { w : InfinitePlace K // w ≠ w₀ }), logMap (ζ • x) x_1 = logMap x x_1
⊢ Eq (α := logSpace K) (logMap (ζ • x)) (logMap x)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
h : ∀ (x : { w : InfinitePlace K // w ≠ w₀ }), logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
⊢ Eq (α := logSpace K) (logMap (HSMul.hSMul (β := mixedSpace K) c 1)) 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₅ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₆ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₇ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - (↑(finrank ℚ K) : ℝ) * Real.log |c| * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₈ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * (↑(finrank ℚ K) : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₉ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log |c| - Real.log |c| * HMul.hMul (α := ℝ) (↑(finrank ℚ K) : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁₀ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * 1) = 0 x
h₁₁ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c|) = 0 x
h₁₂ : HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) 0 = 0 x
h₁₃ : Eq (α := ℝ) 0 (0 x)
h₁₄ h₁₅ : Eq (α := ℝ) 0 0
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x

Tactic:
rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]

Premises used: mul_inv_cancel₀, sub_self, Rat, mul_assoc, Pi.zero_apply, Nat.cast, NumberField.mixedEmbedding.norm_smul, MulZeroClass.mul_zero, map_one, NumberField.mixedEmbedding.logMap_apply, mul_comm, NumberField.mixedEmbedding.normAtPlace_smul, Real.log_pow, mul_one, Module.finrank
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
c : ℝ
hc : c ≠ 0
rw : |c| ^ finrank ℚ K ≠ 0
⊢ Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1) : ℝ) (0 : ℝ)

Tactic:
rw [norm_smul, map_one, mul_one]

Premises used: NumberField.mixedEmbedding.norm_smul, map_one, mul_one
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
c : ℝ
hc : c ≠ 0
⊢ |c| ^ finrank ℚ K ≠ 0

Tactic:
pow_ne_zero _ (abs_ne_zero.mpr hc)

Premises used: Iff.mpr, pow_ne_zero, abs_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
c : ℝ
hc : c ≠ 0
⊢ |c| ^ finrank ℚ K ≠ 0

Tactic:
exact pow_ne_zero _ (abs_ne_zero.mpr hc)

Premises used: Iff.mpr, pow_ne_zero, abs_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
c : ℝ
hc : c ≠ 0
⊢ Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1) : ℝ) (0 : ℝ)

Tactic:
have : mixedEmbedding.norm (c • (1 : mixedSpace K)) ≠ 0 := by
    rw [norm_smul, map_one, mul_one]
    exact pow_ne_zero _ (abs_ne_zero.mpr hc)
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
c : ℝ
hc : c ≠ 0
this : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1) : ℝ) (0 : ℝ)
rw : Eq (α := logSpace K) (logMap (HSMul.hSMul (β := mixedSpace K) c 1 * x)) (logMap x)
rw₁ : HAdd.hAdd (α := logSpace K) (logMap (HSMul.hSMul (β := mixedSpace K) c 1)) (logMap x) = logMap x
rw₂ : HAdd.hAdd (α := logSpace K) 0 (logMap x) = logMap x
rw₃ rw₄ : Eq (α := logSpace K) (logMap x) (logMap x)
⊢ Eq (α := logSpace K) (logMap (c • x)) (logMap x)

Tactic:
rw [← smul_one_mul, logMap_mul this hx, logMap_real, zero_add]

Premises used: zero_add, smul_one_mul, NumberField.mixedEmbedding.logMap_real, NumberField.mixedEmbedding.logMap_mul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
h :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) y : ℝ)
h₁ : ∀ (x_1 : { w : InfinitePlace K // w ≠ w₀ }), logMap x x_1 = logMap y x_1
⊢ Eq (α := logSpace K) (logMap x) (logMap y)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
h :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) y : ℝ)
x_1 : { w : InfinitePlace K // w ≠ w₀ }
h₁ :
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)
h₂ :
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)
⊢ logMap x x_1 = logMap y x_1

Tactic:
simp_rw [logMap_apply, h, norm_eq_of_normAtPlace_eq h]

Premises used: NumberField.mixedEmbedding.logMap_apply, NumberField.mixedEmbedding.norm_eq_of_normAtPlace_eq
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurableSet (α := mixedSpace K) (fundamentalCone K)

Tactic:
MeasurableSet.diff ?_ ?_

Premises used: MeasurableSet.diff, NumberField.mixedEmbedding.fundamentalCone
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_1 :
  MeasurableSet.{u_1} (α := mixedSpace K)
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
refine_2 :
  MeasurableSet.{u_1} (α := mixedSpace K)
    {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
⊢ MeasurableSet (α := mixedSpace K) (fundamentalCone K)

Tactic:
refine MeasurableSet.diff ?_ ?_

Premises used: MeasurableSet.diff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurableSet.{u_1} (α := mixedSpace K)
    (Set.preimage (β := logSpace K)
      (fun (x : mixedSpace K) (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        (↑(↑w : InfinitePlace K).mult : ℝ) *
          (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
            Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(Module.finrank ℚ K) : ℝ)⁻¹))
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))

Tactic:
MeasurableSet.preimage (ZSpan.fundamentalDomain_measurableSet _) <|
      measurable_pi_iff.mpr fun w ↦ measurable_const.mul ?_

Premises used: Iff.mpr, MeasurableSet.preimage, ZSpan.fundamentalDomain_measurableSet, Measurable.mul, measurable_pi_iff, measurable_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_1 :
  ∀ (w : { w : InfinitePlace K // w ≠ w₀ }),
    Measurable (β := ℝ) fun (x : mixedSpace K) ↦
      Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(Module.finrank ℚ K) : ℝ)⁻¹
⊢ MeasurableSet.{u_1} (α := mixedSpace K)
    (Set.preimage (β := logSpace K)
      (fun (x : mixedSpace K) (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        (↑(↑w : InfinitePlace K).mult : ℝ) *
          (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
            Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(Module.finrank ℚ K) : ℝ)⁻¹))
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))

Tactic:
refine MeasurableSet.preimage (ZSpan.fundamentalDomain_measurableSet _) <|
      measurable_pi_iff.mpr fun w ↦ measurable_const.mul ?_

Premises used: Iff.mpr, MeasurableSet.preimage, ZSpan.fundamentalDomain_measurableSet, Measurable.mul, measurable_pi_iff, measurable_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ Measurable (β := ℝ) fun (x : mixedSpace K) ↦
    Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(Module.finrank ℚ K) : ℝ)⁻¹

Tactic:
(continuous_normAtPlace _).measurable.log.sub <|
      (mixedEmbedding.continuous_norm _).measurable.log.mul measurable_const

Premises used: Measurable.mul, Measurable.sub, NumberField.mixedEmbedding.continuous_norm, Measurable.log, NumberField.mixedEmbedding.continuous_normAtPlace, Continuous.measurable, measurable_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ Measurable (β := ℝ) fun (x : mixedSpace K) ↦
    Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(Module.finrank ℚ K) : ℝ)⁻¹

Tactic:
exact (continuous_normAtPlace _).measurable.log.sub <|
      (mixedEmbedding.continuous_norm _).measurable.log.mul measurable_const

Premises used: Measurable.mul, Measurable.sub, NumberField.mixedEmbedding.continuous_norm, Measurable.log, NumberField.mixedEmbedding.continuous_normAtPlace, Continuous.measurable, measurable_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurableSet.{u_1} (α := mixedSpace K)
    {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}

Tactic:
measurableSet_eq_fun (mixedEmbedding.continuous_norm K).measurable measurable_const

Premises used: measurableSet_eq_fun, NumberField.mixedEmbedding.continuous_norm, Continuous.measurable, measurable_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurableSet.{u_1} (α := mixedSpace K)
    {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}

Tactic:
exact measurableSet_eq_fun (mixedEmbedding.continuous_norm K).measurable measurable_const

Premises used: measurableSet_eq_fun, NumberField.mixedEmbedding.continuous_norm, Continuous.measurable, measurable_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_1 :
  MeasurableSet.{u_1} (α := mixedSpace K)
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
refine_2 refine_2₁ :
  MeasurableSet.{u_1} (α := mixedSpace K)
    {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
⊢ MeasurableSet (α := mixedSpace K) (fundamentalCone K)

Tactic:
classical
  refine MeasurableSet.diff ?_ ?_
  · unfold logMap
    refine MeasurableSet.preimage (ZSpan.fundamentalDomain_measurableSet _) <|
      measurable_pi_iff.mpr fun w ↦ measurable_const.mul ?_
    exact (continuous_normAtPlace _).measurable.log.sub <|
      (mixedEmbedding.continuous_norm _).measurable.log.mul measurable_const
  · exact measurableSet_eq_fun (mixedEmbedding.continuous_norm K).measurable measurable_const

Premises used: Iff.mpr, MeasurableSet.preimage, MeasurableSet.diff, ZSpan.fundamentalDomain_measurableSet, NumberField.mixedEmbedding.logMap, Measurable.mul, measurable_pi_iff, measurableSet_eq_fun, Measurable.sub, NumberField.mixedEmbedding.continuous_norm, Measurable.log, NumberField.mixedEmbedding.continuous_normAtPlace, Continuous.measurable, measurable_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
⊢ LT.lt (α := ℝ) (0 : ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)

Tactic:
lt_of_le_of_ne (mixedEmbedding.norm_nonneg _) (Ne.symm hx.2)

Premises used: Ne.symm, NumberField.mixedEmbedding.norm_nonneg, And.right, lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
w : InfinitePlace K
⊢ LT.lt (α := ℝ) (0 : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)

Tactic:
lt_of_le_of_ne (normAtPlace_nonneg _ _)
    (mixedEmbedding.norm_ne_zero_iff.mp (norm_pos_of_mem hx).ne' w).symm

Premises used: NumberField.mixedEmbedding.fundamentalCone.norm_pos_of_mem, Ne.symm, NumberField.mixedEmbedding.norm_ne_zero_iff, LT.lt.ne', NumberField.mixedEmbedding.normAtPlace_nonneg, Iff.mp, lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hy :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) y : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
⊢ y ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}

Tactic:
simpa [norm_eq_of_normAtPlace_eq hy] using hx.2

Premises used: And.right, NumberField.mixedEmbedding.norm_eq_of_normAtPlace_eq
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hy :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) y : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
refine :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    y
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) y

Tactic:
refine ⟨?_, by simpa [norm_eq_of_normAtPlace_eq hy] using hx.2⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hy :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) y : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
rw :
  Membership.mem (γ := Set (logSpace K))
    (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
    (logMap x)
⊢ Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    y

Tactic:
rw [Set.mem_preimage, logMap_eq_of_normAtPlace_eq hy]

Premises used: NumberField.mixedEmbedding.logMap_eq_of_normAtPlace_eq, Set.mem_preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hy :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) y : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
⊢ Membership.mem (γ := Set (logSpace K))
    (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
    (logMap x)

Tactic:
hx.1

Premises used: Set.Mem, setOf, Set.preimage, And.left, ZSpan.fundamentalDomain
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
c : ℝ
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hc : c ≠ 0
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c • x)

Tactic:
⟨?_, ?_⟩

Premises used: Set.Mem, Set.diff, setOf, NumberField.mixedEmbedding.fundamentalCone, And.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
c : ℝ
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hc : c ≠ 0
refine_1 :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    (c • x)
refine_2 : c • x ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c • x)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
c : ℝ
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hc : c ≠ 0
refine_1 :
  Membership.mem (γ := Set (logSpace K))
    (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
    (logMap x)
⊢ Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    (c • x)

Tactic:
rw [Set.mem_preimage, logMap_real_smul hx.2 hc]

Premises used: NumberField.mixedEmbedding.logMap_real_smul, And.right, Set.mem_preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
c : ℝ
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hc : c ≠ 0
⊢ Membership.mem (γ := Set (logSpace K))
    (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
    (logMap x)

Tactic:
hx.1

Premises used: Set.Mem, setOf, Set.preimage, And.left, ZSpan.fundamentalDomain
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
c : ℝ
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hc : c ≠ 0
⊢ Membership.mem (γ := Set (logSpace K))
    (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
    (logMap x)

Tactic:
exact hx.1

Premises used: And.left