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 : 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)
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) u
have 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)ˣ))
          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: 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
a : mixedSpace K
ha : Membership.mem (γ := Set (mixedSpace K)) (integerSet K) a
⊢ ∃! x : 𝓞 K, (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = a
have obtain : ∀ (x : 𝓞 K)
  (ha :
    Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)),
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K) →
    ∃! x_1 : 𝓞 K,
      Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x_1 : K) : mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
Tactic: obtain ⟨_, ⟨x, rfl⟩⟩ := mem_integerSet.mp ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
ha :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
left :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
⊢ ∃! x_1 : 𝓞 K,
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x_1 : K) : mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
have refine : Function.Injective (β := mixedSpace K) fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K)
Tactic: refine Function.Injective.existsUnique_of_mem_range ?_ (Set.mem_range_self 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 y : mixedSpace K
c : ℝ
a : (↑(integerSet K) : Type u_1)
⊢ ⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) ≠ 0
have simp_rw : ¬sorry.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) = 0
Tactic: simp_rw [ne_eq, ← RingOfIntegers.coe_injective.eq_iff, ← (mixedEmbedding_injective K).eq_iff,
    map_zero, (mem_integerSet.mp a.prop).2.choose_spec, ne_zero_of_mem_integerSet,
    not_false_eq_true]
-- 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
c : ℝ
a : (↑(integerSet K) : Type u_1)
simp_rw :
  ¬⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) = 0
⊢ ⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) ≠ 0
have simp_rw₁ : ¬Eq (α := K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
        (sorry.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K))) :
      K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0 : K)
Tactic: simp_rw [ne_eq, ← RingOfIntegers.coe_injective.eq_iff, ← (mixedEmbedding_injective K).eq_iff,
    map_zero, (mem_integerSet.mp a.prop).2.choose_spec, ne_zero_of_mem_integerSet,
    not_false_eq_true]
-- 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
c : ℝ
a : (↑(integerSet K) : Type u_1)
simp_rw :
  ¬⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) = 0
simp_rw₁ :
  ¬Eq (α := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K))) :
        K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0 : K)
⊢ ⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) ≠ 0
have simp_rw₂ : ¬Eq (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (sorry.choose (p := fun (x : 𝓞 K) ↦
            (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)))) :
      mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0) : mixedSpace K)
Tactic: simp_rw [ne_eq, ← RingOfIntegers.coe_injective.eq_iff, ← (mixedEmbedding_injective K).eq_iff,
    map_zero, (mem_integerSet.mp a.prop).2.choose_spec, ne_zero_of_mem_integerSet,
    not_false_eq_true]
-- 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
c : ℝ
a : (↑(integerSet K) : Type u_1)
simp_rw :
  ¬⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) = 0
simp_rw₁ :
  ¬Eq (α := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K))) :
        K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0 : K)
simp_rw₂ :
  ¬Eq (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (⋯.choose (p := fun (x : 𝓞 K) ↦
              (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)))) :
        mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0) : mixedSpace K)
⊢ ⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) ≠ 0
have simp_rw₃ : ¬Eq (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (sorry.choose (p := fun (x : 𝓞 K) ↦
            (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)))) :
      mixedSpace K)
    (0 : mixedSpace K)
Tactic: simp_rw [ne_eq, ← RingOfIntegers.coe_injective.eq_iff, ← (mixedEmbedding_injective K).eq_iff,
    map_zero, (mem_integerSet.mp a.prop).2.choose_spec, ne_zero_of_mem_integerSet,
    not_false_eq_true]
-- 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
c : ℝ
a : (↑(integerSet K) : Type u_1)
simp_rw :
  ¬⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) = 0
simp_rw₁ :
  ¬Eq (α := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K))) :
        K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0 : K)
simp_rw₂ :
  ¬Eq (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (⋯.choose (p := fun (x : 𝓞 K) ↦
              (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)))) :
        mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0) : mixedSpace K)
simp_rw₃ :
  ¬Eq (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (⋯.choose (p := fun (x : 𝓞 K) ↦
              (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)))) :
        mixedSpace K)
      (0 : mixedSpace K)
⊢ ⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) ≠ 0
have simp_rw₄ : ¬(↑a : mixedSpace K) = 0
Tactic: simp_rw [ne_eq, ← RingOfIntegers.coe_injective.eq_iff, ← (mixedEmbedding_injective K).eq_iff,
    map_zero, (mem_integerSet.mp a.prop).2.choose_spec, ne_zero_of_mem_integerSet,
    not_false_eq_true]
-- 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
c : ℝ
a : (↑(integerSet K) : Type u_1)
simp_rw :
  ¬⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) = 0
simp_rw₁ :
  ¬Eq (α := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K))) :
        K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0 : K)
simp_rw₂ :
  ¬Eq (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (⋯.choose (p := fun (x : 𝓞 K) ↦
              (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)))) :
        mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0) : mixedSpace K)
simp_rw₃ :
  ¬Eq (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (⋯.choose (p := fun (x : 𝓞 K) ↦
              (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)))) :
        mixedSpace K)
      (0 : mixedSpace K)
simp_rw₄ : ¬(↑a : mixedSpace K) = 0
⊢ ⋯.choose (p := fun (x : 𝓞 K) ↦ (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)) ≠ 0
have simp_rw₅ : ¬False
Tactic: simp_rw [ne_eq, ← RingOfIntegers.coe_injective.eq_iff, ← (mixedEmbedding_injective K).eq_iff,
    map_zero, (mem_integerSet.mp a.prop).2.choose_spec, ne_zero_of_mem_integerSet,
    not_false_eq_true]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
⊢ (mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑(preimageOfMemIntegerSet a) : 𝓞 K) : K) = (↑a : mixedSpace K)
have rw : (mixedEmbedding K : (a : K) → mixedSpace K)
    (↑(↑(Subtype.mk (p := fun (x : 𝓞 K) ↦ Membership.mem (γ := Submonoid (𝓞 K)) (𝓞 K)⁰ x)
              (sorry.choose (p := fun (x : 𝓞 K) ↦
                (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)))
              sorry) :
          𝓞 K) :
      K) =
  (↑a : mixedSpace K)
Tactic: rw [preimageOfMemIntegerSet, (mem_integerSet.mp a.prop).2.choose_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
rw :
  (mixedEmbedding K : (a : K) → mixedSpace K)
      (↑(↑(Subtype.mk (p := fun (x : 𝓞 K) ↦ Membership.mem (γ := Submonoid (𝓞 K)) (𝓞 K)⁰ x)
                (⋯.choose (p := fun (x : 𝓞 K) ↦
                  (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)))
                ⋯) :
            𝓞 K) :
        K) =
    (↑a : mixedSpace K)
⊢ (mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑(preimageOfMemIntegerSet a) : 𝓞 K) : K) = (↑a : mixedSpace K)
have rw₁ : (↑a : mixedSpace K) = (↑a : mixedSpace K)
Tactic: rw [preimageOfMemIntegerSet, (mem_integerSet.mp a.prop).2.choose_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
hx :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
⊢ (↑(preimageOfMemIntegerSet
          (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
            ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K)) hx)) :
      𝓞 K) =
    x
have simp_rw : (↑(↑(preimageOfMemIntegerSet
            (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
              ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K)) hx)) :
        𝓞 K) :
    K) =
  (↑x : K)
Tactic: simp_rw [RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff,
    mixedEmbedding_preimageOfMemIntegerSet]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
hx :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
simp_rw :
  (↑(↑(preimageOfMemIntegerSet
              (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
                ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K)) hx)) :
          𝓞 K) :
      K) =
    (↑x : K)
⊢ (↑(preimageOfMemIntegerSet
          (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
            ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K)) hx)) :
      𝓞 K) =
    x
have simp_rw₁ : Eq (α := mixedSpace K)
  ((mixedEmbedding K : (a : K) → mixedSpace K)
      (↑(↑(preimageOfMemIntegerSet
                (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
                  ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K)) hx)) :
            𝓞 K) :
        K) :
    mixedSpace K)
  ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
Tactic: simp_rw [RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff,
    mixedEmbedding_preimageOfMemIntegerSet]
-- 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 : x ≠ 0
hx' :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.image (α := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
      (Set.range (ι := 𝓞 K) (⇑(algebraMap (𝓞 K) K) : (a : 𝓞 K) → K)))
    x
⊢ ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (integerSet K) (u • x)
have hx₁ : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
Tactic: replace hx : mixedEmbedding.norm x ≠ 0 :=
      (norm_eq_zero_iff' (Set.mem_range_of_mem_image (mixedEmbedding K) _ hx')).not.mpr hx
Cleared hypotheses: 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' :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.image (α := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
      (Set.range (ι := 𝓞 K) (⇑(algebraMap (𝓞 K) K) : (a : 𝓞 K) → K)))
    x
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (integerSet K) (u • x)
have obtain : ∀ (u : (𝓞 K)ˣ) (hu : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)),
  ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (integerSet K) (u • x)
Tactic: obtain ⟨u, hu⟩ := exists_unit_smul_mem 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' :
  Membership.mem (γ := Set (mixedSpace K))
    (Set.image (α := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
      (Set.range (ι := 𝓞 K) (⇑(algebraMap (𝓞 K) K) : (a : 𝓞 K) → K)))
    x
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
u : (𝓞 K)ˣ
hu : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (u • x)
⊢ ∃ (u : (𝓞 K)ˣ), Membership.mem (γ := Set (mixedSpace K)) (integerSet K) (u • x)
have obtain : ∀ (x : 𝓞 K)
  (hx :
    Ne (α := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : mixedSpace K) :
        ℝ)
      (0 : ℝ))
  (hu :
    Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K)
      (HSMul.hSMul (β := mixedSpace K) u
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : mixedSpace K))),
  ∃ (u : (𝓞 K)ˣ),
    Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
      (HSMul.hSMul (β := mixedSpace K) u
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : mixedSpace K))
Tactic: obtain ⟨_, ⟨x, rfl⟩, _, rfl⟩ := hx'
Cleared hypotheses: x, hx', hx, hu
-- 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
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
hx : Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x
⊢ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) (ζ • x)
have obtain : ∀ (a : 𝓞 K)
  (hx :
    Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (integerSet K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) (↑a : K) : mixedSpace K)),
  Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
    (HSMul.hSMul (β := mixedSpace K) ζ ((mixedEmbedding K : (a : K) → mixedSpace K) (↑a : K) : mixedSpace K))
Tactic: obtain ⟨a, ⟨_, rfl⟩, rfl⟩ := (mem_integerSet.mp hx).2
Cleared hypotheses: x, 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 y : mixedSpace K
c : ℝ
x_1 x_2 : ↥(torsion K)
x_3 : (↑(integerSet K) : Type u_1)
⊢ (x_1 * x_2) • x_3 = x_1 • x_2 • x_3
have rw : (↑((x_1 * x_2) • x_3) : mixedSpace K) = (↑(x_1 • x_2 • x_3) : mixedSpace K)
Tactic: rw [Subtype.mk_eq_mk]
-- 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
c : ℝ
x_1 x_2 : ↥(torsion K)
x_3 : (↑(integerSet K) : Type u_1)
⊢ (↑((x_1 * x_2) • x_3) : mixedSpace K) = (↑(x_1 • x_2 • x_3) : mixedSpace K)
have simp_rw : (↑(x_1 * x_2) : (𝓞 K)ˣ) • (↑x_3 : mixedSpace K) = (↑x_1 : (𝓞 K)ˣ) • (↑x_2 : (𝓞 K)ˣ) • (↑x_3 : mixedSpace K)
Tactic: simp_rw [integerSetTorsionSMul_smul_coe, Subgroup.coe_mul, mul_smul]
-- 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
c : ℝ
x_1 x_2 : ↥(torsion K)
x_3 : (↑(integerSet K) : Type u_1)
simp_rw : (↑(x_1 * x_2) : (𝓞 K)ˣ) • (↑x_3 : mixedSpace K) = (↑x_1 : (𝓞 K)ˣ) • (↑x_2 : (𝓞 K)ˣ) • (↑x_3 : mixedSpace K)
⊢ (↑((x_1 * x_2) • x_3) : mixedSpace K) = (↑(x_1 • x_2 • x_3) : mixedSpace K)
have simp_rw₁ : ((↑x_1 : (𝓞 K)ˣ) * (↑x_2 : (𝓞 K)ˣ)) • (↑x_3 : mixedSpace K) = (↑x_1 : (𝓞 K)ˣ) • (↑x_2 : (𝓞 K)ˣ) • (↑x_3 : mixedSpace K)
Tactic: simp_rw [integerSetTorsionSMul_smul_coe, Subgroup.coe_mul, mul_smul]
-- 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
c : ℝ
x_1 : (↑(integerSet K) : Type u_1)
⊢ HSMul.hSMul (α := ↥(torsion K)) 1 x_1 = x_1
have rw : (↑(HSMul.hSMul (α := ↥(torsion K)) 1 x_1) : mixedSpace K) = (↑x_1 : mixedSpace K)
Tactic: rw [Subtype.mk_eq_mk, integerSetTorsionSMul_smul_coe, OneMemClass.coe_one, one_smul]
-- 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
c : ℝ
x_1 : (↑(integerSet K) : Type u_1)
rw : (↑(HSMul.hSMul (α := ↥(torsion K)) 1 x_1) : mixedSpace K) = (↑x_1 : mixedSpace K)
⊢ HSMul.hSMul (α := ↥(torsion K)) 1 x_1 = x_1
have rw₁ : HSMul.hSMul (α := (𝓞 K)ˣ) (↑1 : (𝓞 K)ˣ) (↑x_1 : mixedSpace K) = (↑x_1 : mixedSpace K)
Tactic: rw [Subtype.mk_eq_mk, integerSetTorsionSMul_smul_coe, OneMemClass.coe_one, one_smul]
-- 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
c : ℝ
x_1 : (↑(integerSet K) : Type u_1)
rw : (↑(HSMul.hSMul (α := ↥(torsion K)) 1 x_1) : mixedSpace K) = (↑x_1 : mixedSpace K)
rw₁ : HSMul.hSMul (α := (𝓞 K)ˣ) (↑1 : (𝓞 K)ˣ) (↑x_1 : mixedSpace K) = (↑x_1 : mixedSpace K)
⊢ HSMul.hSMul (α := ↥(torsion K)) 1 x_1 = x_1
have rw₂ : HSMul.hSMul (α := (𝓞 K)ˣ) 1 (↑x_1 : mixedSpace K) = (↑x_1 : mixedSpace K)
Tactic: rw [Subtype.mk_eq_mk, integerSetTorsionSMul_smul_coe, OneMemClass.coe_one, one_smul]
-- 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
c : ℝ
x_1 : (↑(integerSet K) : Type u_1)
rw : (↑(HSMul.hSMul (α := ↥(torsion K)) 1 x_1) : mixedSpace K) = (↑x_1 : mixedSpace K)
rw₁ : HSMul.hSMul (α := (𝓞 K)ˣ) (↑1 : (𝓞 K)ˣ) (↑x_1 : mixedSpace K) = (↑x_1 : mixedSpace K)
rw₂ : HSMul.hSMul (α := (𝓞 K)ˣ) 1 (↑x_1 : mixedSpace K) = (↑x_1 : mixedSpace K)
⊢ HSMul.hSMul (α := ↥(torsion K)) 1 x_1 = x_1
have rw₃ : (↑x_1 : mixedSpace K) = (↑x_1 : mixedSpace K)
Tactic: rw [Subtype.mk_eq_mk, integerSetTorsionSMul_smul_coe, OneMemClass.coe_one, one_smul]