awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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)
⊢ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) e
have rwa₂ : Type
Tactic: rwa [← Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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)
⊢ ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
have 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) sorry) :
            logSpace K) :
          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₂⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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)
⊢ ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
have 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
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₂⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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 (mixedSpace K)) (fundamentalCone K) (ζ • x)
have left : Membership.mem (γ := Set (mixedSpace K))
  (Set.preimage (β := logSpace K) logMap
    (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
  (ζ • x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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)
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (ζ • x)
have right : ζ • x ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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 (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    (ζ • x)
have left : Membership.mem (γ := Set (logSpace K))
  (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
  (logMap x)
Tactic: rw [Set.mem_preimage, logMap_torsion_smul _ hζ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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) ζ
⊢ ζ • x ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
have right : ¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
Tactic: rw [Set.mem_setOf_eq, unitSMul_smul, map_mul, norm_unit, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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
have refine : ∀ (h : 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⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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)
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) u
have 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)
Tactic: rw [← logEmbedding_eq_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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)
have 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)
Tactic: refine (Subtype.mk_eq_mk (h := ?_) (h' := Submodule.zero_mem _)).mp <|
    (ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)).unique ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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)
⊢ Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
      logSpace K)
    (0 : logSpace K)
have 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)ˣ))
        sorry :
      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: refine (Subtype.mk_eq_mk (h := ?_) (h' := Submodule.zero_mem _)).mp <|
    (ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)).unique ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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
⊢ Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
      logSpace K)
    (0 : logSpace K)
have 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 sorry)
    (logMap x) ∈
  ZSpan.fundamentalDomain B
Tactic: refine (Subtype.mk_eq_mk (h := ?_) (h' := Submodule.zero_mem _)).mp <|
    (ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)).unique ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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))
    (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)
have 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)
Tactic: rw [Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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)
⊢ 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
have refine_2 : logMap (u • x) ∈ ZSpan.fundamentalDomain B
Tactic: rw [AddSubmonoid.mk_vadd, vadd_eq_add, ← logMap_unit_smul _ hx.2]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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)
⊢ 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
have refine_3 : logMap x ∈ ZSpan.fundamentalDomain B
Tactic: rw [AddSubmonoid.mk_vadd, vadd_eq_add, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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
have refine : ∀ (h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)),
  Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) u
Tactic: classical
  refine ⟨fun h ↦ ?_, fun h ↦ torsion_smul_mem_of_mem hx h⟩
  rw [← logEmbedding_eq_zero_iff]
  let B := (basisUnitLattice K).ofZLatticeBasis ℝ
  refine (Subtype.mk_eq_mk (h := ?_) (h' := Submodule.zero_mem _)).mp <|
    (ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)).unique ?_ ?_
  · rw [Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]
    exact ⟨u, trivial, rfl⟩
  · rw [AddSubmonoid.mk_vadd, vadd_eq_add, ← logMap_unit_smul _ hx.2]
    exact h.1
  · rw [AddSubmonoid.mk_vadd, vadd_eq_add, zero_add]
    exact hx.1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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
have refine₁ : ∀ (h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)),
  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: classical
  refine ⟨fun h ↦ ?_, fun h ↦ torsion_smul_mem_of_mem hx h⟩
  rw [← logEmbedding_eq_zero_iff]
  let B := (basisUnitLattice K).ofZLatticeBasis ℝ
  refine (Subtype.mk_eq_mk (h := ?_) (h' := Submodule.zero_mem _)).mp <|
    (ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)).unique ?_ ?_
  · rw [Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]
    exact ⟨u, trivial, rfl⟩
  · rw [AddSubmonoid.mk_vadd, vadd_eq_add, ← logMap_unit_smul _ hx.2]
    exact h.1
  · rw [AddSubmonoid.mk_vadd, vadd_eq_add, zero_add]
    exact hx.1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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
refine₁ :
  ∀ (h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)),
    Eq (α := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) u : Additive (𝓞 K)ˣ) :
        logSpace K)
      (0 : logSpace K)
refine₂ :
  ∀ (h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)),
    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 (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) u
have refine_1 : ∀ (h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)),
  let B : Module.Basis (Fin (rank K)) ℝ (logSpace K) :=
    Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice 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: classical
  refine ⟨fun h ↦ ?_, fun h ↦ torsion_smul_mem_of_mem hx h⟩
  rw [← logEmbedding_eq_zero_iff]
  let B := (basisUnitLattice K).ofZLatticeBasis ℝ
  refine (Subtype.mk_eq_mk (h := ?_) (h' := Submodule.zero_mem _)).mp <|
    (ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)).unique ?_ ?_
  · rw [Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]
    exact ⟨u, trivial, rfl⟩
  · rw [AddSubmonoid.mk_vadd, vadd_eq_add, ← logMap_unit_smul _ hx.2]
    exact h.1
  · rw [AddSubmonoid.mk_vadd, vadd_eq_add, zero_add]
    exact hx.1