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
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
u : (𝓞 K)ˣ
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
refine_1 :
  Membership.mem (α := logSpace K) (γ := Submodule ℤ (logSpace K)) (unitLattice K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
      logSpace K)
⊢ Membership.mem (α := logSpace K) (γ := Submodule ℤ (logSpace K))
    (Submodule.span ℤ (Set.range (ι := Fin (rank K)) (⇑B : (a : Fin (rank K)) → logSpace K)))
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
      logSpace K)

Tactic:
rw [Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]

Premises used: Real, Module.Basis.ofZLatticeBasis_span, NumberField.Units.unitLattice
-- 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
u : (𝓞 K)ˣ
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ Membership.mem (α := logSpace K) (γ := Submodule ℤ (logSpace K)) (unitLattice K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
      logSpace K)

Tactic:
⟨u, trivial, rfl⟩

Premises used: trivial, Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- 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
u : (𝓞 K)ˣ
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ Membership.mem (α := logSpace K) (γ := Submodule ℤ (logSpace K)) (unitLattice K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
      logSpace K)

Tactic:
exact ⟨u, trivial, rfl⟩
-- 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
u : (𝓞 K)ˣ
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
refine_2 : logMap (u • x) ∈ ZSpan.fundamentalDomain B
⊢ HVAdd.hVAdd (α := ↥(Submodule.span ℤ (Set.range (ι := Fin (rank K)) (⇑B : (a : Fin (rank K)) → logSpace K)))) (β :=
      logSpace K)
      (Subtype.mk (p :=
          Membership.mem (γ := Submodule ℤ (logSpace K))
            (Submodule.span ℤ (Set.range (ι := Fin (rank K)) (⇑B : (a : Fin (rank K)) → logSpace K))))
          ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
            ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ))
          ⋯ :
        Subtype
          (Membership.mem (γ := Submodule ℤ (logSpace K))
            (Submodule.span ℤ (Set.range (ι := Fin (rank K)) (⇑B : (a : Fin (rank K)) → logSpace K)))))
      (logMap x) ∈
    ZSpan.fundamentalDomain B

Tactic:
rw [AddSubmonoid.mk_vadd, vadd_eq_add, ← logMap_unit_smul _ hx.2]

Premises used: NumberField.mixedEmbedding.logMap_unit_smul, And.right, vadd_eq_add, AddSubmonoid.mk_vadd
-- 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
u : (𝓞 K)ˣ
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ logMap (u • x) ∈ ZSpan.fundamentalDomain B

Tactic:
h.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
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
u : (𝓞 K)ˣ
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ logMap (u • x) ∈ ZSpan.fundamentalDomain B

Tactic:
exact h.1

Premises used: And.left
-- 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
u : (𝓞 K)ˣ
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
refine_3 : logMap x ∈ ZSpan.fundamentalDomain B
⊢ HVAdd.hVAdd (α := ↥(Submodule.span ℤ (Set.range (ι := Fin (rank K)) (⇑B : (a : Fin (rank K)) → logSpace K)))) (β :=
      logSpace K)
      (Subtype.mk (p :=
        Membership.mem (γ := Submodule ℤ (logSpace K))
          (Submodule.span ℤ (Set.range (ι := Fin (rank K)) (⇑B : (a : Fin (rank K)) → logSpace K))))
        0 ⋯)
      (logMap x) ∈
    ZSpan.fundamentalDomain B

Tactic:
rw [AddSubmonoid.mk_vadd, vadd_eq_add, zero_add]

Premises used: zero_add, vadd_eq_add, AddSubmonoid.mk_vadd
-- 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
u : (𝓞 K)ˣ
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ logMap x ∈ ZSpan.fundamentalDomain B

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
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
u : (𝓞 K)ˣ
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
exact hx.1

Premises used: And.left
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : mixedSpace K
⊢ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) a ↔
    Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) a ∧
      ∃ (x : 𝓞 K), (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = a

Tactic:
simp only [integerSet, Set.mem_inter_iff, SetLike.mem_coe, LinearMap.mem_range,
    AlgHom.toLinearMap_apply, RingHom.toIntAlgHom_coe, RingHom.coe_comp, Function.comp_apply]

Premises used: Set.mem_inter_iff, AlgHom.toLinearMap_apply, LinearMap.mem_range, SetLike.mem_coe, NumberField.mixedEmbedding.fundamentalCone.integerSet, RingHom.coe_comp, RingHom.toIntAlgHom_coe, Function.comp_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : mixedSpace K
ha : Membership.mem (γ := Set (mixedSpace K)) (integerSet K) a
obtain :
  ∀ (x : 𝓞 K)
    (ha :
      Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)),
    Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K) →
      ∃! x_1 : 𝓞 K,
        Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x_1 : K) : mixedSpace K)
          ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
⊢ ∃! x : 𝓞 K, (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = a

Tactic:
obtain ⟨_, ⟨x, rfl⟩⟩ := mem_integerSet.mp ha

Premises used: Iff.mp, NumberField.mixedEmbedding.fundamentalCone.mem_integerSet, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
ha :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
left :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
⊢ ∃! x_1 : 𝓞 K,
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x_1 : K) : mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)

Tactic:
Function.Injective.existsUnique_of_mem_range ?_ (Set.mem_range_self x)

Premises used: Set.mem_range_self, Function.Injective.existsUnique_of_mem_range
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
ha :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
left :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
refine : Function.Injective (β := mixedSpace K) fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K)
⊢ ∃! x_1 : 𝓞 K,
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x_1 : K) : mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)

Tactic:
refine Function.Injective.existsUnique_of_mem_range ?_ (Set.mem_range_self x)

Premises used: Set.mem_range_self, Function.Injective.existsUnique_of_mem_range
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
ha :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
left :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
⊢ Function.Injective (β := mixedSpace K) fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K)

Tactic:
(mixedEmbedding_injective K).comp RingOfIntegers.coe_injective

Premises used: NumberField.RingOfIntegers.coe_injective, Function.Injective.comp, NumberField.mixedEmbedding_injective
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
ha :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
left :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
⊢ Function.Injective (β := mixedSpace K) fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K)

Tactic:
exact (mixedEmbedding_injective K).comp RingOfIntegers.coe_injective

Premises used: NumberField.RingOfIntegers.coe_injective, Function.Injective.comp, NumberField.mixedEmbedding_injective
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
by_contra! : ∀ (this : (↑a : mixedSpace K) = 0), False
⊢ (↑a : mixedSpace K) ≠ 0

Tactic:
by_contra!
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
this : (↑a : mixedSpace K) = 0
⊢ False

Tactic:
a.prop.1.2 (this.symm ▸ mixedEmbedding.norm.map_zero')

Premises used: ZeroHom.map_zero', MonoidWithZeroHom.toZeroHom, Eq.rec, And.right, And.left, Subtype.prop, NumberField.mixedEmbedding.norm, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
this : (↑a : mixedSpace K) = 0
⊢ False

Tactic:
exact a.prop.1.2 (this.symm ▸ mixedEmbedding.norm.map_zero')

Premises used: ZeroHom.map_zero', MonoidWithZeroHom.toZeroHom, Eq.rec, And.right, And.left, Subtype.prop, NumberField.mixedEmbedding.norm, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
a : (↑(integerSet K) : Type u_1)
simp_rw :
  ¬⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) = 0
simp_rw₁ :
  ¬Eq (α := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K))) :
        K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0 : K)
simp_rw₂ :
  ¬Eq (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (⋯.choose (p := fun (x : 𝓞 K) ↦
              (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)))) :
        mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0) : mixedSpace K)
simp_rw₃ :
  ¬Eq (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (⋯.choose (p := fun (x : 𝓞 K) ↦
              (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)))) :
        mixedSpace K)
      (0 : mixedSpace K)
simp_rw₄ : ¬(↑a : mixedSpace K) = 0
simp_rw₅ : ¬False
⊢ ⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) ≠ 0

Tactic:
simp_rw [ne_eq, ← RingOfIntegers.coe_injective.eq_iff, ← (mixedEmbedding_injective K).eq_iff,
    map_zero, (mem_integerSet.mp a.prop).2.choose_spec, ne_zero_of_mem_integerSet,
    not_false_eq_true]

Premises used: Exists.choose_spec, Function.Injective.eq_iff, map_zero, ne_eq, NumberField.RingOfIntegers.coe_injective, And.right, NumberField.mixedEmbedding_injective, Subtype.prop, NumberField.mixedEmbedding.fundamentalCone.ne_zero_of_mem_integerSet, Iff.mp, NumberField.mixedEmbedding.fundamentalCone.mem_integerSet, not_false_eq_true
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
rw :
  (mixedEmbedding K : (a : K) → mixedSpace K)
      (↑(↑(Subtype.mk (p := fun (x : 𝓞 K) ↦ Membership.mem (γ := Submonoid (𝓞 K)) (𝓞 K)⁰ x)
                (⋯.choose (p := fun (x : 𝓞 K) ↦
                  (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)))
                ⋯) :
            𝓞 K) :
        K) =
    (↑a : mixedSpace K)
rw₁ rw₂ : (↑a : mixedSpace K) = (↑a : mixedSpace K)
⊢ (mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑(preimageOfMemIntegerSet a) : 𝓞 K) : K) = (↑a : mixedSpace K)

Tactic:
rw [preimageOfMemIntegerSet, (mem_integerSet.mp a.prop).2.choose_spec]

Premises used: NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet, Exists.choose_spec, And.right, Subtype.prop, Iff.mp, NumberField.mixedEmbedding.fundamentalCone.mem_integerSet
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
hx :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
simp_rw :
  (↑(↑(preimageOfMemIntegerSet
              (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
                ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K)) hx)) :
          𝓞 K) :
      K) =
    (↑x : K)
simp_rw₁ :
  Eq (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        (↑(↑(preimageOfMemIntegerSet
                  (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
                    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K)) hx)) :
              𝓞 K) :
          K) :
      mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
⊢ (↑(preimageOfMemIntegerSet
          (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
            ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K)) hx)) :
      𝓞 K) =
    x

Tactic:
simp_rw [RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff,
    mixedEmbedding_preimageOfMemIntegerSet]

Premises used: Function.Injective.eq_iff, NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, NumberField.mixedEmbedding_injective, NumberField.RingOfIntegers.ext_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : x ≠ 0
hx' :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.image (α := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
      (Set.range (ι := 𝓞 K) (⇑(algebraMap (𝓞 K) K) : (a : 𝓞 K) → K)))
    x
⊢ Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
replace hx : mixedEmbedding.norm x ≠ 0 :=
      (norm_eq_zero_iff' (Set.mem_range_of_mem_image (mixedEmbedding K) _ hx')).not.mpr hx
-- 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))
    (Set.image (α := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
      (Set.range (ι := 𝓞 K) (⇑(algebraMap (𝓞 K) K) : (a : 𝓞 K) → K)))
    x
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
obtain :
  ∀ (u : (𝓞 K)ˣ) (hu : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)),
    ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (integerSet K) (u • x)
⊢ ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (integerSet K) (u • x)

Tactic:
obtain ⟨u, hu⟩ := exists_unit_smul_mem hx

Premises used: NumberField.mixedEmbedding.fundamentalCone.exists_unit_smul_mem
-- 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))
    (Set.image (α := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
      (Set.range (ι := 𝓞 K) (⇑(algebraMap (𝓞 K) K) : (a : 𝓞 K) → K)))
    x
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
u : (𝓞 K)ˣ
hu : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
obtain :
  ∀ (x : 𝓞 K)
    (hx :
      Ne (α := ℝ)
        ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
            ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : mixedSpace K) :
          ℝ)
        (0 : ℝ))
    (hu :
      Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K)
        (HSMul.hSMul (β := mixedSpace K) u
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : mixedSpace K))),
    ∃ (u : (𝓞 K)ˣ),
      Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
        (HSMul.hSMul (β := mixedSpace K) u
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : mixedSpace K))
⊢ ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (integerSet K) (u • x)

Tactic:
obtain ⟨_, ⟨x, rfl⟩, _, rfl⟩ := hx'

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : (𝓞 K)ˣ
x : 𝓞 K
hx :
  Ne (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : mixedSpace K) :
      ℝ)
    (0 : ℝ)
hu :
  Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K)
    (HSMul.hSMul (β := mixedSpace K) u
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : mixedSpace K))
⊢ ∃ (u : (𝓞 K)ˣ),
    Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
      (HSMul.hSMul (β := mixedSpace K) u
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : mixedSpace K))

Tactic:
exact ⟨u, mem_integerSet.mpr ⟨hu, u * x, by simp_rw [unitSMul_smul, ← map_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) ζ
hx : Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x
obtain :
  ∀ (a : 𝓞 K)
    (hx :
      Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) (↑a : K) : mixedSpace K)),
    Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
      (HSMul.hSMul (β := mixedSpace K) ζ ((mixedEmbedding K : (a : K) → mixedSpace K) (↑a : K) : mixedSpace K))
⊢ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) (ζ • x)

Tactic:
obtain ⟨a, ⟨_, rfl⟩, rfl⟩ := (mem_integerSet.mp hx).2

Premises used: And.right, Iff.mp, NumberField.mixedEmbedding.fundamentalCone.mem_integerSet, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
a : 𝓞 K
hx :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑a : K) : mixedSpace K)
⊢ (mixedEmbedding K : (a : K) → mixedSpace K) (↑((↑ζ : 𝓞 K) * a) : K) =
    HSMul.hSMul (β := mixedSpace K) ζ ((mixedEmbedding K : (a : K) → mixedSpace K) (↑a : K) : mixedSpace K)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
a : 𝓞 K
hx :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑a : K) : mixedSpace K)
⊢ Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
    (HSMul.hSMul (β := mixedSpace K) ζ ((mixedEmbedding K : (a : K) → mixedSpace K) (↑a : K) : mixedSpace K))

Tactic:
refine mem_integerSet.mpr ⟨torsion_smul_mem_of_mem hx.1 hζ, ⟨ζ * a, by simp⟩⟩

Premises used: Iff.mpr, Units.val, HMul.hMul, NumberField.mixedEmbedding.fundamentalCone.torsion_smul_mem_of_mem, And.left, And.intro, Exists.intro, NumberField.mixedEmbedding.fundamentalCone.mem_integerSet
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
x_1 x_2 : ↥(torsion K)
x_3 : (↑(integerSet K) : Type u_1)
rw : (↑((x_1 * x_2) • x_3) : mixedSpace K) = (↑(x_1 • x_2 • x_3) : mixedSpace K)
⊢ (x_1 * x_2) • x_3 = x_1 • x_2 • x_3

Tactic:
rw [Subtype.mk_eq_mk]

Premises used: Subtype.mk_eq_mk