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
c : ℝ
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hc : c ≠ 0
refine_2 : ¬|c| ^ Module.finrank ℚ K = 0 ∧ ¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ c • x ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}

Tactic:
rw [Set.mem_setOf_eq, mixedEmbedding.norm_smul, mul_eq_zero, not_or]

Premises used: Set.mem_setOf_eq, mul_eq_zero, NumberField.mixedEmbedding.norm_smul, not_or
-- 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
⊢ ¬|c| ^ Module.finrank ℚ K = 0 ∧ ¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
⟨pow_ne_zero _ (abs_ne_zero.mpr hc), hx.2⟩

Premises used: Iff.mpr, pow_ne_zero, abs_ne_zero, And.right, 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
⊢ ¬|c| ^ Module.finrank ℚ K = 0 ∧ ¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
exact ⟨pow_ne_zero _ (abs_ne_zero.mpr hc), hx.2⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
c : ℝ
hc : c ≠ 0
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c • x) ↔
    Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x

Tactic:
⟨fun h ↦ ?_, fun h ↦ smul_mem_of_mem h hc⟩

Premises used: NumberField.mixedEmbedding.fundamentalCone.smul_mem_of_mem, Iff.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
c : ℝ
hc : c ≠ 0
refine :
  ∀ (h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c • x)),
    Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c • x) ↔
    Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ smul_mem_of_mem h hc⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
c : ℝ
hc : c ≠ 0
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c • x)
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c⁻¹ • c • x)

Tactic:
smul_mem_of_mem h (inv_ne_zero hc)

Premises used: NumberField.mixedEmbedding.fundamentalCone.smul_mem_of_mem, inv_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
c : ℝ
hc : c ≠ 0
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c • x)
h₁ : x = c⁻¹ • c • x
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x

Tactic:
convert! smul_mem_of_mem h (inv_ne_zero hc)

Premises used: NumberField.mixedEmbedding.fundamentalCone.smul_mem_of_mem, inv_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
c : ℝ
hc : c ≠ 0
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c • x)
h₁ h₂ : c • x = c • x
⊢ x = c⁻¹ • c • x

Tactic:
rw [eq_inv_smul_iff₀ hc]

Premises used: eq_inv_smul_iff₀
-- 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 : ℝ)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
rsuffices :
  ∀ (u : Additive (𝓞 K)ˣ) (left : u ∈ (↑⊤ : Set (Additive (𝓞 K)ˣ)))
    (hu :
      HAdd.hAdd (α := logSpace K) (β := logSpace K)
          ((↑(Subtype.mk (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x)
                  ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) u) ⋯) :
              logSpace K) :
            logSpace K)
          (logMap x) ∈
        ZSpan.fundamentalDomain B),
    ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
rsuffices₁ : ∃ (e : ↥(unitLattice K)), (↑e : logSpace K) + logMap x ∈ ZSpan.fundamentalDomain B
⊢ ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)

Tactic:
rsuffices ⟨⟨_, ⟨u, _, rfl⟩⟩, hu⟩ : ∃ e : unitLattice K, e + logMap x ∈ ZSpan.fundamentalDomain B

Premises used: NumberField.mixedEmbedding.logMap, NumberField.Units.unitLattice, ZSpan.fundamentalDomain, rfl
-- 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 : ℝ)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left : u ∈ (↑⊤ : Set (Additive (𝓞 K)ˣ))
hu :
  HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((↑(Subtype.mk (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x)
              ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) u) ⋯) :
          logSpace K) :
        logSpace K)
      (logMap x) ∈
    ZSpan.fundamentalDomain B
rwa :
  Membership.mem (γ := Set (logSpace K))
    (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
    (logMap (u • x))
rwa₁ rwa₂ rwa₃ rwa₄ :
  Membership.mem (γ := Set (logSpace K))
    (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
    (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))
⊢ Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    (u • x)

Tactic:
rwa [Set.mem_preimage, logMap_unit_smul u hx]

Premises used: NumberField.mixedEmbedding.logMap_unit_smul, Set.mem_preimage
-- 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 : ℝ)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left : u ∈ (↑⊤ : Set (Additive (𝓞 K)ˣ))
hu :
  HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((↑(Subtype.mk (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x)
              ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) u) ⋯) :
          logSpace K) :
        logSpace K)
      (logMap x) ∈
    ZSpan.fundamentalDomain B
⊢ u • x ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}

Tactic:
simp [hx]
-- 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 : ℝ)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left : u ∈ (↑⊤ : Set (Additive (𝓞 K)ˣ))
hu :
  HAdd.hAdd (α := logSpace K) (β := logSpace K)
      ((↑(Subtype.mk (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x)
              ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) u) ⋯) :
          logSpace K) :
        logSpace K)
      (logMap x) ∈
    ZSpan.fundamentalDomain B
⊢ ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)

Tactic:
exact ⟨u, by rwa [Set.mem_preimage, logMap_unit_smul u hx], by simp [hx]⟩
-- 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 : ℝ)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
obtain :
  ∀ (e : logSpace K)
    (h₁ :
      Membership.mem (γ := Submodule ℤ (logSpace K))
        (Submodule.span ℤ (Set.range (ι := Fin (rank K)) (⇑B : (a : Fin (rank K)) → logSpace K))) e)
    (h₂ :
      HVAdd.hVAdd (β := logSpace K)
          (Subtype.mk (p := fun (x : logSpace K) ↦
            Membership.mem (γ := Submodule ℤ (logSpace K))
              (Submodule.span ℤ (Set.range (ι := Fin (rank K)) (⇑B : (a : Fin (rank K)) → logSpace K))) x)
            e h₁)
          (logMap x) ∈
        ZSpan.fundamentalDomain B),
    ∃ (e : ↥(unitLattice K)), (↑e : logSpace K) + logMap x ∈ ZSpan.fundamentalDomain B
⊢ ∃ (e : ↥(unitLattice K)), (↑e : logSpace K) + logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
obtain ⟨⟨e, h₁⟩, h₂, -⟩ := ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)

Premises used: NumberField.mixedEmbedding.logMap, ZSpan.exist_unique_vadd_mem_fundamentalDomain
-- 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 : ℝ)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
e : logSpace K
h₁ :
  Membership.mem (γ := Submodule ℤ (logSpace K))
    (Submodule.span ℤ (Set.range (ι := Fin (rank K)) (⇑B : (a : Fin (rank K)) → logSpace K))) e
h₂ :
  HVAdd.hVAdd (β := logSpace K)
      (Subtype.mk (p := fun (x : logSpace K) ↦
        Membership.mem (γ := Submodule ℤ (logSpace K))
          (Submodule.span ℤ (Set.range (ι := Fin (rank K)) (⇑B : (a : Fin (rank K)) → logSpace K))) x)
        e h₁)
      (logMap x) ∈
    ZSpan.fundamentalDomain B
rwa :
  Membership.mem (γ := Submodule ℤ (logSpace K))
    (Submodule.span ℤ
      (Set.range (ι := Fin (rank K))
        (⇑(Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
    e
rwa₁ : Module.Basis (Fin (rank K)) ℤ ↥(unitLattice K)
rwa₂ : Type
rwa₃ :
  Membership.mem (γ := Submodule ℤ (logSpace K))
    (Submodule.span ℤ
      (Set.range (ι := Fin (rank K))
        (⇑(Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
    e
rwa₄ : Module.Basis (Fin (rank K)) ℤ ↥(unitLattice K)
rwa₅ : Type
rwa₆ :
  Membership.mem (γ := Submodule ℤ (logSpace K))
    (Submodule.span ℤ
      (Set.range (ι := Fin (rank K))
        (⇑(Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
    e
rwa₇ : Module.Basis (Fin (rank K)) ℤ ↥(unitLattice K)
rwa₈ : Type
rwa₉ :
  Membership.mem (γ := Submodule ℤ (logSpace K))
    (Submodule.span ℤ
      (Set.range (ι := Fin (rank K))
        (⇑(Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
    e
rwa₁₀ : Module.Basis (Fin (rank K)) ℤ ↥(unitLattice K)
rwa₁₁ : Type
⊢ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) e

Tactic:
rwa [← 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 : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
e : logSpace K
h₁ :
  Membership.mem (γ := Submodule ℤ (logSpace K))
    (Submodule.span ℤ (Set.range (ι := Fin (rank K)) (⇑B : (a : Fin (rank K)) → logSpace K))) e
h₂ :
  HVAdd.hVAdd (β := logSpace K)
      (Subtype.mk (p := fun (x : logSpace K) ↦
        Membership.mem (γ := Submodule ℤ (logSpace K))
          (Submodule.span ℤ (Set.range (ι := Fin (rank K)) (⇑B : (a : Fin (rank K)) → logSpace K))) x)
        e h₁)
      (logMap x) ∈
    ZSpan.fundamentalDomain B
⊢ ∃ (e : ↥(unitLattice K)), (↑e : logSpace K) + logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
exact ⟨⟨e, by rwa [← Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]⟩, h₂⟩
-- 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 : ℝ)
let let₁ let₂ : ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
let₃ :
  let B : Module.Basis (Fin (rank K)) ℝ (logSpace K) :=
    Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K);
  ∀ (u : Additive (𝓞 K)ˣ) (left : u ∈ (↑⊤ : Set (Additive (𝓞 K)ˣ)))
    (hu :
      HAdd.hAdd (α := logSpace K) (β := logSpace K)
          ((↑(Subtype.mk (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x)
                  ((AddMonoidHom.toIntLinearMap (logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K) u) ⋯) :
              logSpace K) :
            logSpace K)
          (logMap x) ∈
        ZSpan.fundamentalDomain B),
    ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
let₄ let₅ :
  let B : Module.Basis (Fin (rank K)) ℝ (logSpace K) :=
    Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K);
  ∃ (e : ↥(unitLattice K)), (↑e : logSpace K) + logMap x ∈ ZSpan.fundamentalDomain B
⊢ ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)

Tactic:
classical
  let B := (basisUnitLattice K).ofZLatticeBasis ℝ
  rsuffices ⟨⟨_, ⟨u, _, rfl⟩⟩, hu⟩ : ∃ e : unitLattice K, e + logMap x ∈ ZSpan.fundamentalDomain B
  · exact ⟨u, by rwa [Set.mem_preimage, logMap_unit_smul u hx], by simp [hx]⟩
  · obtain ⟨⟨e, h₁⟩, h₂, -⟩ := ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)
    exact ⟨⟨e, by rwa [← Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]⟩, h₂⟩

Premises used: NumberField.mixedEmbedding.logMap, NumberField.Units.unitLattice, 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
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
left :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    (ζ • x)
right : ζ • x ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (ζ • x)

Tactic:
constructor
-- 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
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
left :
  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))))
    (ζ • x)

Tactic:
rw [Set.mem_preimage, logMap_torsion_smul _ hζ]

Premises used: NumberField.mixedEmbedding.logMap_torsion_smul, Set.mem_preimage
-- 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
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
⊢ 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
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
⊢ 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
-- 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
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
right : ¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ ζ • x ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}

Tactic:
rw [Set.mem_setOf_eq, unitSMul_smul, map_mul, norm_unit, one_mul]

Premises used: Set.mem_setOf_eq, 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
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
⊢ ¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
hx.2

Premises used: Set.Mem, setOf, And.right
-- 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
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
⊢ ¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
exact hx.2

Premises used: And.right
-- 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)ˣ
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) u

Tactic:
⟨fun h ↦ ?_, fun h ↦ torsion_smul_mem_of_mem hx h⟩

Premises used: NumberField.mixedEmbedding.fundamentalCone.torsion_smul_mem_of_mem, Iff.intro
-- 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)ˣ
refine :
  ∀ (h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)),
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) u
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) u

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ torsion_smul_mem_of_mem hx h⟩
-- 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)
rw :
  Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
      logSpace K)
    (0 : logSpace K)
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) u

Tactic:
rw [← logEmbedding_eq_zero_iff]

Premises used: NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff
-- 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)
⊢ Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
      logSpace K)
    (0 : logSpace K)

Tactic:
(Subtype.mk_eq_mk (h := ?_) (h' := Submodule.zero_mem _)).mp <|
    (ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)).unique ?_ ?_

Premises used: NumberField.mixedEmbedding.logMap, ZSpan.exist_unique_vadd_mem_fundamentalDomain, Subtype.mk_eq_mk, Iff.mp, ExistsUnique.unique
-- 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))
    (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)
refine_2 :
  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
refine_3 :
  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
⊢ Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
      logSpace K)
    (0 : logSpace K)

Tactic:
refine (Subtype.mk_eq_mk (h := ?_) (h' := Submodule.zero_mem _)).mp <|
    (ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)).unique ?_ ?_

Premises used: NumberField.mixedEmbedding.logMap, ZSpan.exist_unique_vadd_mem_fundamentalDomain, Subtype.mk_eq_mk, Iff.mp, ExistsUnique.unique