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 : ℝ)
c : ℝ
hc : c ≠ 0
⊢ Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1) : ℝ) (0 : ℝ)
have rw : |c| ^ finrank ℚ K ≠ 0
Tactic: rw [norm_smul, map_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
c : ℝ
hc : c ≠ 0
⊢ Eq (α := logSpace K) (logMap (c • x)) (logMap x)
have this : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1) : ℝ) (0 : ℝ)
Tactic: have : mixedEmbedding.norm (c • (1 : mixedSpace K)) ≠ 0 := by
    rw [norm_smul, map_one, mul_one]
    exact pow_ne_zero _ (abs_ne_zero.mpr hc)
-- 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 : ℝ)
c : ℝ
hc : c ≠ 0
this : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1) : ℝ) (0 : ℝ)
⊢ Eq (α := logSpace K) (logMap (c • x)) (logMap x)
have rw : Eq (α := logSpace K) (logMap (HSMul.hSMul (β := mixedSpace K) c 1 * x)) (logMap x)
Tactic: rw [← smul_one_mul, logMap_mul this hx, logMap_real, 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 : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
c : ℝ
hc : c ≠ 0
this : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1) : ℝ) (0 : ℝ)
rw : Eq (α := logSpace K) (logMap (HSMul.hSMul (β := mixedSpace K) c 1 * x)) (logMap x)
⊢ Eq (α := logSpace K) (logMap (c • x)) (logMap x)
have rw₁ : HAdd.hAdd (α := logSpace K) (logMap (HSMul.hSMul (β := mixedSpace K) c 1)) (logMap x) = logMap x
Tactic: rw [← smul_one_mul, logMap_mul this hx, logMap_real, 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 : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
c : ℝ
hc : c ≠ 0
this : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1) : ℝ) (0 : ℝ)
rw : Eq (α := logSpace K) (logMap (HSMul.hSMul (β := mixedSpace K) c 1 * x)) (logMap x)
rw₁ : HAdd.hAdd (α := logSpace K) (logMap (HSMul.hSMul (β := mixedSpace K) c 1)) (logMap x) = logMap x
⊢ Eq (α := logSpace K) (logMap (c • x)) (logMap x)
have rw₂ : HAdd.hAdd (α := logSpace K) 0 (logMap x) = logMap x
Tactic: rw [← smul_one_mul, logMap_mul this hx, logMap_real, 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 : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
c : ℝ
hc : c ≠ 0
this : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1) : ℝ) (0 : ℝ)
rw : Eq (α := logSpace K) (logMap (HSMul.hSMul (β := mixedSpace K) c 1 * x)) (logMap x)
rw₁ : HAdd.hAdd (α := logSpace K) (logMap (HSMul.hSMul (β := mixedSpace K) c 1)) (logMap x) = logMap x
rw₂ : HAdd.hAdd (α := logSpace K) 0 (logMap x) = logMap x
⊢ Eq (α := logSpace K) (logMap (c • x)) (logMap x)
have rw₃ : Eq (α := logSpace K) (logMap x) (logMap x)
Tactic: rw [← smul_one_mul, logMap_mul this hx, logMap_real, 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 y : mixedSpace K
h :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) y : ℝ)
⊢ Eq (α := logSpace K) (logMap x) (logMap y)
have h₁ : ∀ (x_1 : { w : InfinitePlace K // w ≠ w₀ }), logMap x x_1 = logMap y x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
h :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) y : ℝ)
x_1 : { w : InfinitePlace K // w ≠ w₀ }
⊢ logMap x x_1 = logMap y x_1
have h₁ : (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
    (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) =
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
    (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)
Tactic: simp_rw [logMap_apply, h, norm_eq_of_normAtPlace_eq 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 y : mixedSpace K
h :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) y : ℝ)
x_1 : { w : InfinitePlace K // w ≠ w₀ }
h₁ :
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)
⊢ logMap x x_1 = logMap y x_1
have h₂ : (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
    (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) =
  (↑(↑x_1 : InfinitePlace K).mult : ℝ) *
    (Real.log ((normAtPlace (↑x_1 : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)
Tactic: simp_rw [logMap_apply, h, norm_eq_of_normAtPlace_eq h]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurableSet (α := mixedSpace K) (fundamentalCone K)
have refine_1 : MeasurableSet.{u_1} (α := mixedSpace K)
  (Set.preimage (β := logSpace K) logMap
    (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
Tactic: refine MeasurableSet.diff ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_1 :
  MeasurableSet.{u_1} (α := mixedSpace K)
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
⊢ MeasurableSet (α := mixedSpace K) (fundamentalCone K)
have refine_2 : MeasurableSet.{u_1} (α := mixedSpace K)
  {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
Tactic: refine MeasurableSet.diff ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurableSet.{u_1} (α := mixedSpace K)
    (Set.preimage (β := logSpace K)
      (fun (x : mixedSpace K) (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        (↑(↑w : InfinitePlace K).mult : ℝ) *
          (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
            Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(Module.finrank ℚ K) : ℝ)⁻¹))
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
have refine_1 : ∀ (w : { w : InfinitePlace K // w ≠ w₀ }),
  Measurable (β := ℝ) fun (x : mixedSpace K) ↦
    Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(Module.finrank ℚ K) : ℝ)⁻¹
Tactic: refine MeasurableSet.preimage (ZSpan.fundamentalDomain_measurableSet _) <|
      measurable_pi_iff.mpr fun w ↦ measurable_const.mul ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurableSet (α := mixedSpace K) (fundamentalCone K)
have refine_1 : MeasurableSet.{u_1} (α := mixedSpace K)
  (Set.preimage (β := logSpace K) logMap
    (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
Tactic: classical
  refine MeasurableSet.diff ?_ ?_
  · unfold logMap
    refine MeasurableSet.preimage (ZSpan.fundamentalDomain_measurableSet _) <|
      measurable_pi_iff.mpr fun w ↦ measurable_const.mul ?_
    exact (continuous_normAtPlace _).measurable.log.sub <|
      (mixedEmbedding.continuous_norm _).measurable.log.mul measurable_const
  · exact measurableSet_eq_fun (mixedEmbedding.continuous_norm K).measurable measurable_const
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_1 :
  MeasurableSet.{u_1} (α := mixedSpace K)
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
⊢ MeasurableSet (α := mixedSpace K) (fundamentalCone K)
have refine_2 : MeasurableSet.{u_1} (α := mixedSpace K)
  {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
Tactic: classical
  refine MeasurableSet.diff ?_ ?_
  · unfold logMap
    refine MeasurableSet.preimage (ZSpan.fundamentalDomain_measurableSet _) <|
      measurable_pi_iff.mpr fun w ↦ measurable_const.mul ?_
    exact (continuous_normAtPlace _).measurable.log.sub <|
      (mixedEmbedding.continuous_norm _).measurable.log.mul measurable_const
  · exact measurableSet_eq_fun (mixedEmbedding.continuous_norm K).measurable measurable_const
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hy :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) y : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) y
have refine : Membership.mem (γ := Set (mixedSpace K))
  (Set.preimage (β := logSpace K) logMap
    (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
  y
Tactic: refine ⟨?_, by simpa [norm_eq_of_normAtPlace_eq hy] using 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 y : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hy :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) y : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
⊢ Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    y
have rw : 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_eq_of_normAtPlace_eq hy]
-- 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
c : ℝ
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hc : c ≠ 0
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c • x)
have refine_1 : Membership.mem (γ := Set (mixedSpace K))
  (Set.preimage (β := logSpace K) logMap
    (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
  (c • x)
Tactic: refine ⟨?_, ?_⟩
-- 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
c : ℝ
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hc : c ≠ 0
refine_1 :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    (c • x)
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c • x)
have refine_2 : c • x ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
Tactic: refine ⟨?_, ?_⟩
-- 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
c : ℝ
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hc : c ≠ 0
⊢ Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    (c • x)
have refine_1 : 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_real_smul hx.2 hc]
-- 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
c : ℝ
hx : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
hc : c ≠ 0
⊢ c • x ∉ {x : mixedSpace K | Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)}
have refine_2 : ¬|c| ^ Module.finrank ℚ K = 0 ∧ ¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
Tactic: rw [Set.mem_setOf_eq, mixedEmbedding.norm_smul, mul_eq_zero, not_or]
-- 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
c : ℝ
hc : c ≠ 0
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c • x) ↔
    Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
have refine : ∀ (h : 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⟩
-- 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
c : ℝ
hc : c ≠ 0
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c • x)
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x
have h₁ : x = c⁻¹ • c • x
Tactic: convert! smul_mem_of_mem h (inv_ne_zero hc)
-- 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
c : ℝ
hc : c ≠ 0
h : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (c • x)
⊢ x = c⁻¹ • c • x
have h₁ : c • x = c • x
Tactic: rw [eq_inv_smul_iff₀ hc]
-- 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)
⊢ ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
have 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) sorry) :
            logSpace K) :
          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
-- 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)
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)
⊢ ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
have rsuffices₁ : ∃ (e : ↥(unitLattice K)), (↑e : logSpace K) + logMap x ∈ ZSpan.fundamentalDomain B
Tactic: rsuffices ⟨⟨_, ⟨u, _, rfl⟩⟩, hu⟩ : ∃ e : unitLattice K, e + logMap x ∈ ZSpan.fundamentalDomain B
-- 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)
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
⊢ Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    (u • x)
have rwa : Membership.mem (γ := Set (logSpace K))
  (ZSpan.fundamentalDomain (ι := Fin (rank K)) (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))
  (logMap (u • x))
Tactic: rwa [Set.mem_preimage, logMap_unit_smul u hx]
-- 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)
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))
⊢ Membership.mem (γ := Set (mixedSpace K))
    (Set.preimage (β := logSpace K) logMap
      (ZSpan.fundamentalDomain (ι := Fin (rank K))
        (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))))
    (u • x)
have 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))
Tactic: rwa [Set.mem_preimage, logMap_unit_smul u hx]
-- 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 : ↥(unitLattice K)), (↑e : logSpace K) + logMap x ∈ ZSpan.fundamentalDomain B
have 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
Tactic: obtain ⟨⟨e, h₁⟩, h₂, -⟩ := ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)
-- 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
⊢ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) e
have rwa₁ : Module.Basis (Fin (rank K)) ℤ ↥(unitLattice K)
Tactic: rwa [← Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]