awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
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)
simp_rw₁ :
  ((↑x_1 : (𝓞 K)ˣ) * (↑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)

Tactic:
simp_rw [integerSetTorsionSMul_smul_coe, Subgroup.coe_mul, mul_smul]

Premises used: NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe, Subgroup.coe_mul, SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
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)
rw₃ rw₄ : (↑x_1 : mixedSpace K) = (↑x_1 : mixedSpace K)
⊢ HSMul.hSMul (α := ↥(torsion K)) 1 x_1 = x_1

Tactic:
rw [Subtype.mk_eq_mk, integerSetTorsionSMul_smul_coe, OneMemClass.coe_one, one_smul]

Premises used: OneMemClass.coe_one, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe, one_smul, Subtype.mk_eq_mk
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
rw :
  Eq (α := ℝ) ((↑(Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K))) : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₁ :
  Eq (α := ℝ) ((↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)| : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₂ :
  Eq (α := ℝ) ((↑(↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)| : ℚ) : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₃ :
  Eq (α := ℝ) ((↑|(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)) : ℚ)| : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₄ :
  Eq (α := ℝ) ((↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑(↑(preimageOfMemIntegerSet a) : 𝓞 K) : K)| : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₅ :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑(preimageOfMemIntegerSet a) : 𝓞 K) : K) : mixedSpace K) :
      ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₆ rw₇ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
⊢ Eq (α := ℝ) ((↑(intNorm a) : ℝ) : ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)

Tactic:
rw [intNorm, Nat.cast_natAbs, ← Rat.cast_intCast, Int.cast_abs, Algebra.coe_norm_int,
    ← norm_eq_norm, mixedEmbedding_preimageOfMemIntegerSet]

Premises used: Int.cast_abs, Rat.cast_intCast, NumberField.mixedEmbedding.norm_eq_norm, Algebra.coe_norm_int, Nat.cast_natAbs, NumberField.mixedEmbedding.fundamentalCone.intNorm, NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
a b : (↑(integerSet K) : Type u_1)
h : a ≈ b
u : ↥(torsion K)
hu : (fun (m : ↥(torsion K)) ↦ m • b) u = a
rw :
  Eq (α := ℝ) (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a) : ℝ)
    (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b) : ℝ)
rw₁ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
    ((↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b) : ℝ) : ℝ)
rw₂ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
rw₃ :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑((fun (m : ↥(torsion K)) ↦ m • b) u) : mixedSpace K) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
rw₄ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((↑u : (𝓞 K)ˣ) • (↑b : mixedSpace K)) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
rw₅ rw₆ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
⊢ Eq (α := ℕ) ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a)
    ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b)

Tactic:
rw [← Nat.cast_inj (R := ℝ), intNorm_coe, intNorm_coe, ← hu, integerSetTorsionSMul_smul_coe,
      norm_unit_smul]

Premises used: NumberField.mixedEmbedding.norm_unit_smul, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe, Nat.cast_inj, NumberField.mixedEmbedding.fundamentalCone.intNorm_coe
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
⊢ quotIntNorm ⟦a⟧ = intNorm a

Tactic:
rfl

Premises used: NumberField.mixedEmbedding.fundamentalCone.quotIntNorm, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
⊢ integerSetToAssociates K a = ⟦preimageOfMemIntegerSet a⟧

Tactic:
rfl

Premises used: NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ ∃ (u : (𝓞 K)ˣ),
    Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
      (HSMul.hSMul (β := mixedSpace K) u ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))

Tactic:
exists_unitSMul_mem_integerSet ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩

Premises used: Set.mem_range_self, NumberField.RingOfIntegers.val, NumberField.mixedEmbedding.fundamentalCone.exists_unitSMul_mem_integerSet, And.intro, Exists.intro, Subtype.val, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
refine :
  Ne (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K)
    (0 : mixedSpace K)
⊢ ∃ (u : (𝓞 K)ˣ),
    Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
      (HSMul.hSMul (β := mixedSpace K) u ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))

Tactic:
refine exists_unitSMul_mem_integerSet ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ Ne (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K)
    (0 : mixedSpace K)

Tactic:
(map_ne_zero _).mpr <| RingOfIntegers.coe_ne_zero_iff.mpr (nonZeroDivisors.coe_ne_zero _)

Premises used: Iff.mpr, nonZeroDivisors.coe_ne_zero, map_ne_zero, NumberField.RingOfIntegers.coe_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ Ne (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K)
    (0 : mixedSpace K)

Tactic:
exact (map_ne_zero _).mpr <| RingOfIntegers.coe_ne_zero_iff.mpr (nonZeroDivisors.coe_ne_zero _)

Premises used: Iff.mpr, nonZeroDivisors.coe_ne_zero, map_ne_zero, NumberField.RingOfIntegers.coe_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
mk :
  ∀ (u : (𝓞 K)ˣ)
    (hu :
      Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
        (HSMul.hSMul (β := mixedSpace K) u
          ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))),
    ∃ (a : (↑(integerSet K) : Type u_1)),
      integerSetToAssociates K a = Quot.mk (⇑(Associated.setoid ↥(𝓞 K)⁰) : ↥(𝓞 K)⁰ → ↥(𝓞 K)⁰ → Prop) x
⊢ ∃ (a : (↑(integerSet K) : Type u_1)),
    integerSetToAssociates K a = Quot.mk (⇑(Associated.setoid ↥(𝓞 K)⁰) : ↥(𝓞 K)⁰ → ↥(𝓞 K)⁰ → Prop) x

Tactic:
obtain ⟨u, hu⟩ : ∃ u : (𝓞 K)ˣ, u • mixedEmbedding K (x : 𝓞 K) ∈ integerSet K := by
    refine exists_unitSMul_mem_integerSet ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩
    exact (map_ne_zero _).mpr <| RingOfIntegers.coe_ne_zero_iff.mpr (nonZeroDivisors.coe_ne_zero _)

Premises used: NumberField.mixedEmbedding, NumberField.RingOfIntegers.val, NumberField.mixedEmbedding.fundamentalCone.integerSet, NumberField.RingOfIntegers, Subtype.val, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu :
  Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
    (HSMul.hSMul (β := mixedSpace K) u ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
⊢ ∃ (a : (↑(integerSet K) : Type u_1)),
    integerSetToAssociates K a = Quot.mk (⇑(Associated.setoid ↥(𝓞 K)⁰) : ↥(𝓞 K)⁰ → ↥(𝓞 K)⁰ → Prop) x

Tactic:
⟨⟨u • mixedEmbedding K (x : 𝓞 K), hu⟩,
    Quotient.sound ⟨unitsNonZeroDivisorsEquiv.symm u⁻¹, ?_⟩⟩

Premises used: NumberField.mixedEmbedding, NumberField.RingOfIntegers.val, Subtype.mk, Inv.inv, Exists.intro, HSMul.hSMul, unitsNonZeroDivisorsEquiv, Quotient.sound, MulEquiv.symm, Subtype.val, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu :
  Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
    (HSMul.hSMul (β := mixedSpace K) u ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
mk :
  preimageOfMemIntegerSet
        (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
          (HSMul.hSMul (β := mixedSpace K) u
            ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
          hu) *
      (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰) =
    x
⊢ ∃ (a : (↑(integerSet K) : Type u_1)),
    integerSetToAssociates K a = Quot.mk (⇑(Associated.setoid ↥(𝓞 K)⁰) : ↥(𝓞 K)⁰ → ↥(𝓞 K)⁰ → Prop) x

Tactic:
refine ⟨⟨u • mixedEmbedding K (x : 𝓞 K), hu⟩,
    Quotient.sound ⟨unitsNonZeroDivisorsEquiv.symm u⁻¹, ?_⟩⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : (↑(integerSet K) : Type u_1)
simp_rw :
  (∃ (u : (↥(𝓞 K)⁰)ˣ),
      HMul.hMul (α := mixedSpace K)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
            mixedSpace K)
          (↑a : mixedSpace K) =
        (↑b : mixedSpace K)) ↔
    ∃ (ζ : ↥(torsion K)), (↑ζ : (𝓞 K)ˣ) • (↑a : mixedSpace K) = (↑b : mixedSpace K)
⊢ integerSetToAssociates K a = integerSetToAssociates K b ↔ ∃ (ζ : ↥(torsion K)), ζ • a = b

Tactic:
simp_rw [integerSetToAssociates_apply, Associates.quotient_mk_eq_mk,
    Associates.mk_eq_mk_iff_associated, Associated, mul_comm, Subtype.ext_iff,
    RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff, Submonoid.coe_mul, map_mul,
    mixedEmbedding_preimageOfMemIntegerSet, integerSetTorsionSMul_smul_coe]

Premises used: Associates.mk_eq_mk_iff_associated, Function.Injective.eq_iff, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe, Associates.quotient_mk_eq_mk, NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_apply, Subtype.ext_iff, map_mul, NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, Associated, NumberField.mixedEmbedding_injective, mul_comm, NumberField.RingOfIntegers.ext_iff, Submonoid.coe_mul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : (↑(integerSet K) : Type u_1)
h_1 :
  ∃ (u : (↥(𝓞 K)⁰)ˣ),
    HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
          mixedSpace K)
        (↑a : mixedSpace K) =
      (↑b : mixedSpace K)
u : (↥(𝓞 K)⁰)ˣ
h :
  HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
        mixedSpace K)
      (↑a : mixedSpace K) =
    (↑b : mixedSpace K)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simpa using h
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : (↑(integerSet K) : Type u_1)
h_1 : ∃ (ζ : ↥(torsion K)), (↑ζ : (𝓞 K)ˣ) • (↑a : mixedSpace K) = (↑b : mixedSpace K)
u : (𝓞 K)ˣ
property : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) u
h :
  (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) u property) : (𝓞 K)ˣ) •
      (↑a : mixedSpace K) =
    (↑b : mixedSpace K)
⊢ HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u) : ↥(𝓞 K)⁰) : 𝓞 K)) :
        mixedSpace K)
      (↑a : mixedSpace K) =
    (↑b : mixedSpace K)

Tactic:
simpa using h
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : (↑(integerSet K) : Type u_1)
refine :
  (∃ (u : (↥(𝓞 K)⁰)ˣ),
      HMul.hMul (α := mixedSpace K)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
            mixedSpace K)
          (↑a : mixedSpace K) =
        (↑b : mixedSpace K)) →
    ∀ (u : (↥(𝓞 K)⁰)ˣ)
      (h :
        HMul.hMul (α := mixedSpace K)
            ((mixedEmbedding K : (a : K) → mixedSpace K)
                ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
              mixedSpace K)
            (↑a : mixedSpace K) =
          (↑b : mixedSpace K)),
      Membership.mem (α := (𝓞 K)ˣ) (γ := Subgroup (𝓞 K)ˣ) (torsion K)
        ((unitsNonZeroDivisorsEquiv : (a : (↥(𝓞 K)⁰)ˣ) → (𝓞 K)ˣ) u : (𝓞 K)ˣ)
⊢ (∃ (u : (↥(𝓞 K)⁰)ˣ),
      HMul.hMul (α := mixedSpace K)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
            mixedSpace K)
          (↑a : mixedSpace K) =
        (↑b : mixedSpace K)) ↔
    ∃ (ζ : ↥(torsion K)), (↑ζ : (𝓞 K)ˣ) • (↑a : mixedSpace K) = (↑b : mixedSpace K)

Tactic:
refine ⟨fun ⟨u, h⟩ ↦  ⟨⟨unitsNonZeroDivisorsEquiv u, ?_⟩, by simpa using h⟩,
    fun ⟨⟨u, _⟩, h⟩ ↦ ⟨unitsNonZeroDivisorsEquiv.symm u, by simpa using h⟩⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : (↑(integerSet K) : Type u_1)
h_1 :
  ∃ (u : (↥(𝓞 K)⁰)ˣ),
    HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
          mixedSpace K)
        (↑a : mixedSpace K) =
      (↑b : mixedSpace K)
u : (↥(𝓞 K)⁰)ˣ
h :
  HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
        mixedSpace K)
      (↑a : mixedSpace K) =
    (↑b : mixedSpace K)
⊢ Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K)
    (HSMul.hSMul (α := (𝓞 K)ˣ) ((unitsNonZeroDivisorsEquiv : (a : (↥(𝓞 K)⁰)ˣ) → (𝓞 K)ˣ) u : (𝓞 K)ˣ) (↑a : mixedSpace K))

Tactic:
simpa [h] using b.prop.1

Premises used: And.left, Subtype.prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : (↑(integerSet K) : Type u_1)
h_1 :
  ∃ (u : (↥(𝓞 K)⁰)ˣ),
    HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
          mixedSpace K)
        (↑a : mixedSpace K) =
      (↑b : mixedSpace K)
u : (↥(𝓞 K)⁰)ˣ
h :
  HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
        mixedSpace K)
      (↑a : mixedSpace K) =
    (↑b : mixedSpace K)
⊢ Membership.mem (α := (𝓞 K)ˣ) (γ := Subgroup (𝓞 K)ˣ) (torsion K)
    ((unitsNonZeroDivisorsEquiv : (a : (↥(𝓞 K)⁰)ˣ) → (𝓞 K)ˣ) u : (𝓞 K)ˣ)

Tactic:
exact (unit_smul_mem_iff_mem_torsion a.prop.1 _).mp (by simpa [h] using b.prop.1)

Premises used: NumberField.mixedEmbedding.fundamentalCone.unit_smul_mem_iff_mem_torsion, And.left, Subtype.prop, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
a :
  ∀ (a b : (↑(integerSet K) : Type u_1)),
    (Setoid.ker (integerSetToAssociates K) : (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop) a b ↔
      (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
          (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
        a b
⊢ Eq (α := Setoid (↑(integerSet K) : Type u_1)) (Setoid.ker (integerSetToAssociates K))
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1))

Tactic:
ext a b
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
a b : (↑(integerSet K) : Type u_1)
a₁ :
  integerSetToAssociates K a = integerSetToAssociates K b ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
a₂ :
  integerSetToAssociates K b = integerSetToAssociates K a ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
a₃ :
  (∃ (ζ : ↥(torsion K)), ζ • b = a) ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
a₄ : (∃ (ζ : ↥(torsion K)), ζ • b = a) ↔ a ∈ MulAction.orbit (↥(torsion K)) b
a₅ a₆ : (∃ (ζ : ↥(torsion K)), ζ • b = a) ↔ ∃ (x : ↥(torsion K)), x • b = a
⊢ (Setoid.ker (integerSetToAssociates K) : (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop) a b ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b

Tactic:
rw [Setoid.ker_def, eq_comm, integerSetToAssociates_eq_iff b a,
          MulAction.orbitRel_apply, MulAction.mem_orbit_iff]

Premises used: MulAction.mem_orbit_iff, Setoid.ker_def, eq_comm, MulAction.orbitRel_apply, NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_eq_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
⊢ Eq (α := Associates ↥(𝓞 K)⁰)
    ((integerSetQuotEquivAssociates K :
          (a : Quotient (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1))) → Associates ↥(𝓞 K)⁰)
        ⟦a⟧ :
      Associates ↥(𝓞 K)⁰)
    (⟦preimageOfMemIntegerSet a⟧ : Quotient (α := ↥(𝓞 K)⁰) (Associated.setoid ↥(𝓞 K)⁰))

Tactic:
rfl

Premises used: NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
⊢ Eq (α := Subgroup ↥(torsion K)) (MulAction.stabilizer (↥(torsion K)) a) ⊥

Tactic:
(Subgroup.eq_bot_iff_forall _).mpr fun ζ hζ ↦ ?_

Premises used: Iff.mpr, Subgroup.eq_bot_iff_forall
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
refine :
  ∀ (ζ : ↥(torsion K)) (hζ : Membership.mem (γ := Subgroup ↥(torsion K)) (MulAction.stabilizer (↥(torsion K)) a) ζ),
    ζ = 1
⊢ Eq (α := Subgroup ↥(torsion K)) (MulAction.stabilizer (↥(torsion K)) a) ⊥

Tactic:
refine (Subgroup.eq_bot_iff_forall _).mpr fun ζ hζ ↦ ?_

Premises used: Iff.mpr, Subgroup.eq_bot_iff_forall
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
ζ : ↥(torsion K)
hζ : Membership.mem (γ := Subgroup ↥(torsion K)) (MulAction.stabilizer (↥(torsion K)) a) ζ
rwa :
  ∀ (hζ : (↑(↑ζ : (𝓞 K)ˣ) : 𝓞 K) * (↑(preimageOfMemIntegerSet a) : 𝓞 K) = (↑(preimageOfMemIntegerSet a) : 𝓞 K)),
    (↑(preimageOfMemIntegerSet a) : 𝓞 K) ≠ 0
⊢ ζ = 1

Tactic:
rwa [MulAction.mem_stabilizer_iff, Subtype.ext_iff, integerSetTorsionSMul_smul_coe,
    unitSMul_smul, ← mixedEmbedding_preimageOfMemIntegerSet, ← map_mul,
    (mixedEmbedding_injective K).eq_iff, ← map_mul, ← RingOfIntegers.ext_iff, mul_eq_right₀,
    Units.val_eq_one, OneMemClass.coe_eq_one] at hζ

Premises used: Function.Injective.eq_iff, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe, mul_eq_right₀, OneMemClass.coe_eq_one, Subtype.ext_iff, map_mul, NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, NumberField.mixedEmbedding.unitSMul_smul, NumberField.mixedEmbedding_injective, NumberField.RingOfIntegers.ext_iff, MulAction.mem_stabilizer_iff, Units.val_eq_one
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
ζ : ↥(torsion K)
hζ : (↑(↑ζ : (𝓞 K)ˣ) : 𝓞 K) * (↑(preimageOfMemIntegerSet a) : 𝓞 K) = (↑(preimageOfMemIntegerSet a) : 𝓞 K)
⊢ (↑(preimageOfMemIntegerSet a) : 𝓞 K) ≠ 0

Tactic:
nonZeroDivisors.coe_ne_zero _

Premises used: nonZeroDivisors.coe_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
ζ : ↥(torsion K)
hζ : (↑(↑ζ : (𝓞 K)ˣ) : 𝓞 K) * (↑(preimageOfMemIntegerSet a) : 𝓞 K) = (↑(preimageOfMemIntegerSet a) : 𝓞 K)
⊢ (↑(preimageOfMemIntegerSet a) : 𝓞 K) ≠ 0

Tactic:
exact nonZeroDivisors.coe_ne_zero _

Premises used: nonZeroDivisors.coe_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
a : Quotient (α := (↑(integerSet K) : Type u_1)) (MulAction.orbitRel ↥(Units.torsion K) (↑(integerSet K) : Type u_1))
simp_rw : HasQuotient.Quotient ↥(Units.torsion K) (B := Subgroup ↥(Units.torsion K)) ⊥ ≃ ↥(Units.torsion K)
⊢ HasQuotient.Quotient ↥(Units.torsion K) (B := Subgroup ↥(Units.torsion K))
      (MulAction.stabilizer (↥(Units.torsion K)) a.out) ≃
    ↥(Units.torsion K)

Tactic:
simp_rw [integerSetTorsionSMul_stabilizer]

Premises used: NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_stabilizer