-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem exists_unit_smul_mem (hx : mixedEmbedding.norm x ≠ 0) :
    ∃ u : (𝓞 K)ˣ, u • x ∈ fundamentalCone K

Proof state:
case intro.mk.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
e : { w // w ≠ w₀ } → ℝ
h₁ : e ∈ Submodule.span ℤ (Set.range ⇑B)
h₂ : ⟨e, h₁⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B
⊢ ∃ e, ↑e + logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
exact ⟨⟨e, by rwa [← Basis.ofZLatticeBasis_span ℝ (unitLattice K)]⟩, h₂⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left✝ : u ∈ ↑⊤
hu : ↑⟨(logEmbedding K).toIntLinearMap u, ⋯⟩ + logMap x ∈ ZSpan.fundamentalDomain B
⊢ u • x ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

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

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left✝ : u ∈ ↑⊤
hu : ↑⟨(logEmbedding K).toIntLinearMap u, ⋯⟩ + logMap x ∈ ZSpan.fundamentalDomain B
⊢ u • x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
simp [hx]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ∃ e, ↑e + logMap x ∈ ZSpan.fundamentalDomain B

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

Result:
case intro.mk.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
e : { w // w ≠ w₀ } → ℝ
h₁ : e ∈ Submodule.span ℤ (Set.range ⇑B)
h₂ : ⟨e, h₁⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B
⊢ ∃ e, ↑e + logMap x ∈ ZSpan.fundamentalDomain B

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ∃ u, u • x ∈ fundamentalCone K

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

Result:
case intro.mk.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left✝ : u ∈ ↑⊤
hu : ↑⟨(logEmbedding K).toIntLinearMap u, ⋯⟩ + logMap x ∈ ZSpan.fundamentalDomain B
⊢ ∃ u, u • x ∈ fundamentalCone K

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ∃ e, ↑e + logMap x ∈ ZSpan.fundamentalDomain B

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
e : { w // w ≠ w₀ } → ℝ
h₁ : e ∈ Submodule.span ℤ (Set.range ⇑B)
h₂ : ⟨e, h₁⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B
⊢ e ∈ unitLattice K

Tactic:
rwa [← Basis.ofZLatticeBasis_span ℝ (unitLattice K)]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
⊢ ∃ u, u • x ∈ fundamentalCone K

Tactic:
let B := (basisUnitLattice K).ofZLatticeBasis ℝ

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ∃ u, u • x ∈ fundamentalCone K

Proof state:
case intro.mk.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left✝ : u ∈ ↑⊤
hu : ↑⟨(logEmbedding K).toIntLinearMap u, ⋯⟩ + logMap x ∈ ZSpan.fundamentalDomain B
⊢ ∃ u, u • x ∈ fundamentalCone K

Tactic:
exact ⟨u, by rwa [Set.mem_preimage, logMap_unit_smul u hx], by simp [hx]⟩

Result:
no goals