-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem unit_smul_mem_iff_mem_torsion (hx : x ∈ fundamentalCone K) (u : (𝓞 K)ˣ) :
    u • x ∈ fundamentalCone K ↔ u ∈ torsion K

Proof state:
case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
exact hx.1

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
⊢ u • x ∈ fundamentalCone K ↔ u ∈ torsion K

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

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
⊢ u ∈ torsion K

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ logMap (u • x) ∈ ZSpan.fundamentalDomain B

Tactic:
exact h.1

Result:
no goals

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ (logEmbedding K) (Additive.ofMul u) ∈ unitLattice K

Tactic:
exact ⟨u, trivial, rfl⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
⊢ u ∈ torsion K

Tactic:
rw [← logEmbedding_eq_zero_iff]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
⊢ (logEmbedding K) (Additive.ofMul u) = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
⊢ (logEmbedding K) (Additive.ofMul u) = 0

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

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ (logEmbedding K) (Additive.ofMul u) = 0

Proof state:
case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ⟨0, ⋯⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B

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

Result:
case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ logMap x ∈ ZSpan.fundamentalDomain B

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ⟨(logEmbedding K) (Additive.ofMul u), ⋯⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B

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

Result:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ logMap (u • x) ∈ ZSpan.fundamentalDomain B

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ (logEmbedding K) (Additive.ofMul u) ∈ Submodule.span ℤ (Set.range ⇑B)

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

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ (logEmbedding K) (Additive.ofMul u) ∈ unitLattice K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ (logEmbedding K) (Additive.ofMul u) = 0

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

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ (logEmbedding K) (Additive.ofMul u) ∈ Submodule.span ℤ (Set.range ⇑B)

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ⟨(logEmbedding K) (Additive.ofMul u), ?refine_1⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B

case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Basis (Fin (rank K)) ℝ ({ w // w ≠ w₀ } → ℝ) := Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ⟨0, ⋯⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B