-- 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)
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)
refine_2 :
  ∀ (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);
    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
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) u
have refine_3 : ∀ (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);
  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: 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