awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
h : minkowskiBound K 1 ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
w : K
h_mem : Membership.mem (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K) w
h_nz : w ≠ 0
h_bd : (↑|(Algebra.norm ℚ : (a : K) → ℚ) w| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
obtain :
  ∀ (a : 𝓞 K)
    (h_mem :
      Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))
    (h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K))
    (h_bd :
      (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
        (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K),
    ∃ (a : 𝓞 K), a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
⊢ ∃ (a : 𝓞 K), a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K

Tactic:
obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem

Premises used: FractionalIdeal.mem_one_iff, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
h : minkowskiBound K 1 ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
a : 𝓞 K
h_mem :
  Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_bd :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
⊢ ∃ (a : 𝓞 K), a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K

Tactic:
⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩

Premises used: And.intro, Exists.intro, Iff.mp, NumberField.RingOfIntegers.coe_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
h : minkowskiBound K 1 ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
a : 𝓞 K
h_mem :
  Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_bd :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
⊢ ∃ (a : 𝓞 K), a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K

Tactic:
exact ⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
x x_1 : (𝓞 K)ˣ
x_2 : mixedSpace K
simp_rw :
  HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x * x_1) : 𝓞 K)) :
        mixedSpace K)
      x_2 =
    HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) : mixedSpace K)
      (HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K)) : mixedSpace K)
        x_2)
simp_rw₁ :
  HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K) : K)) :
        mixedSpace K)
      x_2 =
    HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) : mixedSpace K)
      (HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K)) : mixedSpace K)
        x_2)
simp_rw₂ :
  HMul.hMul (α := mixedSpace K) (β := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) : mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K)) :
          mixedSpace K) *
      x_2 =
    HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) : mixedSpace K)
      (HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K)) : mixedSpace K)
        x_2)
⊢ (x * x_1) • x_2 = x • x_1 • x_2

Tactic:
simp_rw [unitSMul_smul, Units.coe_mul, map_mul, mul_assoc]

Premises used: NumberField.Units.coe_mul, mul_assoc, map_mul, NumberField.mixedEmbedding.unitSMul_smul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
simp_rw :
  HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑1 : 𝓞 K)) : mixedSpace K) x =
    x
simp_rw₁ : (mixedEmbedding K : (a : K) → mixedSpace K) 1 * x = x
simp_rw₂ : 1 * x = x
⊢ HSMul.hSMul (α := (𝓞 K)ˣ) 1 x = x

Tactic:
simp_rw [unitSMul_smul, Units.coe_one, map_one, one_mul]

Premises used: NumberField.Units.coe_one, NumberField.mixedEmbedding.unitSMul_smul, map_one, one_mul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : x = 0
rw : HSMul.hSMul (β := mixedSpace K) u 0 = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := mixedSpace K) 0 0
⊢ u • x = 0

Tactic:
rw [h, smul_zero]

Premises used: smul_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
refine : ∀ (h : u • x = 0), x = 0
⊢ u • x = 0 ↔ x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, smul_zero]⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : u • x = 0
contrapose! : ∀ (h : x ≠ 0), u • x ≠ 0
⊢ x = 0

Tactic:
contrapose! h
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : x ≠ 0
obtain : ∀ (w : InfinitePlace K) (h : Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)), u • x ≠ 0
⊢ u • x ≠ 0

Tactic:
obtain ⟨w, h⟩ := exists_normAtPlace_ne_zero_iff.mpr h

Premises used: Iff.mpr, NumberField.mixedEmbedding.exists_normAtPlace_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h_1 : x ≠ 0
w : InfinitePlace K
h : Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ u • x ≠ 0

Tactic:
exists_normAtPlace_ne_zero_iff.mp ⟨w, ?_⟩

Premises used: Exists.intro, Iff.mp, NumberField.mixedEmbedding.exists_normAtPlace_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h_1 : x ≠ 0
w : InfinitePlace K
h : Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
refine : Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (u • x) : ℝ) (0 : ℝ)
⊢ u • x ≠ 0

Tactic:
refine exists_normAtPlace_ne_zero_iff.mp ⟨w, ?_⟩

Premises used: Exists.intro, Iff.mp, NumberField.mixedEmbedding.exists_normAtPlace_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h_1 : x ≠ 0
w : InfinitePlace K
h : Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
rw :
  HMul.hMul (α := ℝ) (β := ℝ)
      ((normAtPlace w : (a : mixedSpace K) → ℝ)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) :
            mixedSpace K) :
        ℝ)
      ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) ≠
    0
⊢ Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (u • x) : ℝ) (0 : ℝ)

Tactic:
rw [unitSMul_smul, map_mul]

Premises used: map_mul, NumberField.mixedEmbedding.unitSMul_smul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h_1 : x ≠ 0
w : InfinitePlace K
h : Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ Ne (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K) :
      ℝ)
    (0 : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h_1 : x ≠ 0
w : InfinitePlace K
h : Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ)
      ((normAtPlace w : (a : mixedSpace K) → ℝ)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) :
            mixedSpace K) :
        ℝ)
      ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) ≠
    0

Tactic:
exact mul_ne_zero (by simp) h

Premises used: mul_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
I : Function.Injective (α := K) (β := mixedSpace K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
⊢ HSMul.hSMul (β := mixedSpace K) u ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K) =
      (mixedEmbedding K : (a : K) → mixedSpace K) (↑y : K) ↔
    (↑u : 𝓞 K) * x = y

Tactic:
rw [unitSMul_smul, ← map_mul, Function.Injective.eq_iff, ← RingOfIntegers.coe_eq_algebraMap,
    ← map_mul, ← RingOfIntegers.ext_iff]

Premises used: Function.Injective.eq_iff, map_mul, NumberField.mixedEmbedding.unitSMul_smul, NumberField.RingOfIntegers.coe_eq_algebraMap, NumberField.RingOfIntegers.ext_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ Function.Injective (α := K) (β := mixedSpace K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)

Tactic:
mixedEmbedding_injective K

Premises used: NumberField.mixedEmbedding_injective
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ Function.Injective (α := K) (β := mixedSpace K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)

Tactic:
exact mixedEmbedding_injective K

Premises used: NumberField.mixedEmbedding_injective
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : (𝓞 K)ˣ
x : mixedSpace K
rw :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        (HMul.hMul (α := mixedSpace K)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K)
          x) :
      ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
rw₁ :
  HMul.hMul (α := ℝ) (β := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) :
            mixedSpace K) :
        ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) =
    (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x
rw₂ :
  HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) =
    (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x
rw₃ rw₄ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (u • x) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)

Tactic:
rw [unitSMul_smul, map_mul, norm_unit, one_mul]

Premises used: map_mul, NumberField.mixedEmbedding.unitSMul_smul, NumberField.mixedEmbedding.norm_unit, one_mul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ logMap x w =
    (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹)

Tactic:
rfl

Premises used: NumberField.mixedEmbedding.logMap, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : ∀ (x : { w : InfinitePlace K // w ≠ w₀ }), logMap 0 x = 0 x
⊢ Eq.{u_1 + 1} (α := logSpace K) (logMap 0) 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w ≠ w₀ }
⊢ logMap 0 x = 0 x

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

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w ≠ w₀ }
⊢ logMap 1 x = 0 x

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
hy : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)
h :
  ∀ (w : { w : InfinitePlace K // w ≠ w₀ }),
    logMap (x * y) w = HAdd.hAdd (α := logSpace K) (β := logSpace K) (logMap x) (logMap y) w
⊢ logMap (x * y) = HAdd.hAdd (α := logSpace K) (logMap x) (logMap y)

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

Tactic:
rw [map_mul, map_mul, Real.log_mul, Real.log_mul hx hy, add_mul]

Premises used: add_mul, map_mul, Real.log_mul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
hy : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) +
          Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
        (Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹ +
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)) =
    (↑(↑w : InfinitePlace K).mult : ℝ) *
        (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) +
      (↑(↑w : InfinitePlace K).mult : ℝ) *
        (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
hy : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ Ne (α := ℝ) ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
mixedEmbedding.norm_ne_zero_iff.mp hx w

Premises used: NumberField.mixedEmbedding.norm_ne_zero_iff, Iff.mp, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
hy : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ Ne (α := ℝ) ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
exact mixedEmbedding.norm_ne_zero_iff.mp hx w

Premises used: NumberField.mixedEmbedding.norm_ne_zero_iff, Iff.mp, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
hy : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ Ne (α := ℝ) ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)

Tactic:
mixedEmbedding.norm_ne_zero_iff.mp hy w

Premises used: NumberField.mixedEmbedding.norm_ne_zero_iff, Iff.mp, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
hy : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ Ne (α := ℝ) ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)

Tactic:
exact mixedEmbedding.norm_ne_zero_iff.mp hy w

Premises used: NumberField.mixedEmbedding.norm_ne_zero_iff, Iff.mp, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
rw :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
rw₁ :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log 1 * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
rw₂ :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        HMul.hMul (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
rw₃ :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) - 0) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
rw₄ rw₅ :
  (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
⊢ logMap x w =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)

Tactic:
rw [logMap_apply, hx, Real.log_one, zero_mul, sub_zero]

Premises used: sub_zero, MulZeroClass.zero_mul, Real.log_one, NumberField.mixedEmbedding.logMap_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : (𝓞 K)ˣ
h :
  ∀ (x : { w : InfinitePlace K // w ≠ w₀ }),
    logMap ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K))) x =
      (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) x
⊢ Eq.{u_1 + 1} (α := logSpace K)
    (logMap ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K))))
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : (𝓞 K)ˣ
x : { w : InfinitePlace K // w ≠ w₀ }
⊢ logMap ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K))) x =
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) x

Tactic:
simp
-- 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 : Ne (α := ℝ) 1 0
⊢ Ne (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K) :
      ℝ)
    (0 : ℝ)

Tactic:
rw [norm_unit]

Premises used: NumberField.mixedEmbedding.norm_unit
-- 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 : ℝ)
⊢ Ne (α := ℝ) 1 0

Tactic:
norm_num