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 : ℝ
a : Quotient (α := (↑(integerSet K) : Type u_1)) (MulAction.orbitRel ↥(Units.torsion K) (↑(integerSet K) : Type u_1))
⊢ HasQuotient.Quotient ↥(Units.torsion K) (B := Subgroup ↥(Units.torsion K)) ⊥ ≃ ↥(Units.torsion K)

Tactic:
exact QuotientGroup.quotientBot.toEquiv

Premises used: MulEquiv.toEquiv, QuotientGroup.quotientBot
-- 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 (α := Ideal (𝓞 K))
    (↑(↑((integerSetEquiv K :
                  (a : (↑(integerSet K) : Type u_1)) →
                    { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                a).1 :
          ↥(Ideal (𝓞 K))⁰) :
      Ideal (𝓞 K))
    (Ideal.span {(↑(preimageOfMemIntegerSet a) : 𝓞 K)})

Tactic:
rfl

Premises used: Set.Mem, setOf, Submodule.span, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
n : ℕ
x_1 : (↑(integerSet K) : Type u_1)
simp_rw :
  Eq (α := ℝ) (↑(intNorm x_1) : ℝ) (↑n : ℝ) ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n
simp_rw₁ :
  Eq (α := ℝ) (↑(Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet x_1) : 𝓞 K))) : ℝ) (↑n : ℝ) ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n
simp_rw₂ :
  Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet x_1) : 𝓞 K)) = n ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n
simp_rw₃ :
  Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet x_1) : 𝓞 K)) = n ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ) (Ideal.span {(↑(preimageOfMemIntegerSet x_1) : 𝓞 K)}) = n
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑x_1 : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ) ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n

Tactic:
simp_rw [← intNorm_coe, intNorm,
        Nat.cast_inj, integerSetEquiv_apply_fst, absNorm_span_singleton]

Premises used: NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, Nat.cast_inj, NumberField.mixedEmbedding.fundamentalCone.intNorm, NumberField.mixedEmbedding.fundamentalCone.intNorm_coe, Ideal.absNorm_span_singleton
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
rw :
  Nat.card.{u_1}
      ((↑{I : ↥(Ideal (𝓞 K))⁰ |
              IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) = n} :
          Type u_1) ×
        ↥(Units.torsion K)) =
    Nat.card.{u_1}
      (↑{a : (↑(integerSet K) : Type u_1) |
            Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ)} :
        Type u_1)
⊢ Nat.card.{u_1}
        (↑{I : ↥(Ideal (𝓞 K))⁰ |
              IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) = n} :
          Type u_1) *
      torsionOrder K =
    Nat.card.{u_1}
      (↑{a : (↑(integerSet K) : Type u_1) |
            Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ)} :
        Type u_1)

Tactic:
rw [torsionOrder, ← Nat.card_eq_fintype_card, ← Nat.card_prod]

Premises used: NumberField.Units.torsionOrder, Nat.card_prod, Nat.card_eq_fintype_card
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
⊢ Nat.card.{u_1}
      ((↑{I : ↥(Ideal (𝓞 K))⁰ |
              IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) = n} :
          Type u_1) ×
        ↥(Units.torsion K)) =
    Nat.card.{u_1}
      (↑{a : (↑(integerSet K) : Type u_1) |
            Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ)} :
        Type u_1)

Tactic:
Nat.card_congr (integerSetEquivNorm K n).symm

Premises used: Nat.card_congr, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm, Equiv.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
⊢ Nat.card.{u_1}
      ((↑{I : ↥(Ideal (𝓞 K))⁰ |
              IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) = n} :
          Type u_1) ×
        ↥(Units.torsion K)) =
    Nat.card.{u_1}
      (↑{a : (↑(integerSet K) : Type u_1) |
            Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ)} :
        Type u_1)

Tactic:
exact Nat.card_congr (integerSetEquivNorm K n).symm

Premises used: Nat.card_congr, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm, Equiv.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : (↑(idealSet K J) : Type u_1)
⊢ (↑(idealSetMap K J a) : mixedSpace K) = (↑a : mixedSpace K)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, RingHom.IsIntegralElem, IsIntegral, Set.image, Set.range, NumberField.RingOfIntegers, NumberField.mixedEmbedding.fundamentalCone.idealSet, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : (↑(idealSet K J) : Type u_1)
obtain :
  Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (↑a : mixedSpace K) →
    ∀ (x : 𝓞 K) (hx₁ : x ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K)))
      (hx₂ : (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)),
      (↑(preimageOfMemIntegerSet (idealSetMap K J a)) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
⊢ (↑(preimageOfMemIntegerSet (idealSetMap K J a)) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))

Tactic:
obtain ⟨_, ⟨x, hx₁, hx₂⟩⟩ := mem_idealSet.mp a.prop

Premises used: Subtype.prop, Iff.mp, NumberField.mixedEmbedding.fundamentalCone.mem_idealSet
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : (↑(idealSet K J) : Type u_1)
left : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (↑a : mixedSpace K)
x : 𝓞 K
hx₁ : x ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
hx₂ : (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)
simp_rw : x ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
⊢ (↑(preimageOfMemIntegerSet (idealSetMap K J a)) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))

Tactic:
simp_rw [idealSetMap, ← hx₂, preimageOfMemIntegerSet_mixedEmbedding]

Premises used: NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet_mixedEmbedding, NumberField.mixedEmbedding.fundamentalCone.idealSetMap
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : (↑(idealSet K J) : Type u_1)
left : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (↑a : mixedSpace K)
x : 𝓞 K
hx₁ : x ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
hx₂ : (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)
⊢ x ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))

Tactic:
hx₁
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : (↑(idealSet K J) : Type u_1)
left : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (↑a : mixedSpace K)
x : 𝓞 K
hx₁ : x ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
hx₂ : (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)
⊢ x ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))

Tactic:
exact hx₁
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
x_1 x_2 : (↑(idealSet K J) : Type u_1)
h :
  Eq.{u_1 + 1} (α :=
    (↑{a : (↑(integerSet K) : Type u_1) | (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
      Type u_1))
    ((fun (a : (↑(idealSet K J) : Type u_1)) ↦
        (Subtype.mk (p := fun (x : (↑(integerSet K) : Type u_1)) ↦
            Membership.mem (γ := Set (↑(integerSet K) : Type u_1))
              {a : (↑(integerSet K) : Type u_1) |
                (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))}
              x)
            (idealSetMap K J a) ⋯ :
          { x : (↑(integerSet K) : Type u_1) //
            Membership.mem (γ := Set (↑(integerSet K) : Type u_1))
              {a : (↑(integerSet K) : Type u_1) |
                (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))}
              x }))
      x_1)
    ((fun (a : (↑(idealSet K J) : Type u_1)) ↦
        (Subtype.mk (p := fun (x : (↑(integerSet K) : Type u_1)) ↦
            Membership.mem (γ := Set (↑(integerSet K) : Type u_1))
              {a : (↑(integerSet K) : Type u_1) |
                (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))}
              x)
            (idealSetMap K J a) ⋯ :
          { x : (↑(integerSet K) : Type u_1) //
            Membership.mem (γ := Set (↑(integerSet K) : Type u_1))
              {a : (↑(integerSet K) : Type u_1) |
                (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))}
              x }))
      x_2)
⊢ (↑x_1 : mixedSpace K) = (↑x_2 : mixedSpace K)

Tactic:
simp_rw [Subtype.ext_iff, idealSetMap_apply] at h

Premises used: NumberField.mixedEmbedding.fundamentalCone.idealSetMap_apply, Subtype.ext_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
x_1 x_2 : (↑(idealSet K J) : Type u_1)
h rwa rwa₁ rwa₂ rwa₃ : (↑x_1 : mixedSpace K) = (↑x_2 : mixedSpace K)
⊢ x_1 = x_2

Tactic:
rwa [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : (↑(idealSet K J) : Type u_1)
⊢ (↑(↑((idealSetEquiv K J :
                (a : (↑(idealSet K J) : Type u_1)) →
                  (↑{a : (↑(integerSet K) : Type u_1) |
                        (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                    Type u_1))
              a) :
          (↑(integerSet K) : Type u_1)) :
      mixedSpace K) =
    (↑a : mixedSpace K)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, RingHom.IsIntegralElem, IsIntegral, Set.image, Set.range, NumberField.RingOfIntegers, NumberField.mixedEmbedding.fundamentalCone.idealSet, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : { a : (↑(integerSet K) : Type u_1) // (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K)) }
rw :
  (↑(↑((idealSetEquiv K J :
                (a : (↑(idealSet K J) : Type u_1)) →
                  (↑{a : (↑(integerSet K) : Type u_1) |
                        (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                    Type u_1))
              ((Equiv.symm (idealSetEquiv K J) :
                  (a :
                      (↑{a : (↑(integerSet K) : Type u_1) |
                            (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                        Type u_1)) →
                    (↑(idealSet K J) : Type u_1))
                a)) :
          (↑(integerSet K) : Type u_1)) :
      mixedSpace K) =
    (↑(↑a : (↑(integerSet K) : Type u_1)) : mixedSpace K)
rw₁ rw₂ : (↑(↑a : (↑(integerSet K) : Type u_1)) : mixedSpace K) = (↑(↑a : (↑(integerSet K) : Type u_1)) : mixedSpace K)
⊢ (↑((Equiv.symm (idealSetEquiv K J) :
            (a :
                (↑{a : (↑(integerSet K) : Type u_1) |
                      (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                  Type u_1)) →
              (↑(idealSet K J) : Type u_1))
          a) :
      mixedSpace K) =
    (↑(↑a : (↑(integerSet K) : Type u_1)) : mixedSpace K)

Tactic:
rw [← (idealSetEquiv_apply ((idealSetEquiv K J).symm a)), Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv, Equiv.symm, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_apply, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : (↑(idealSet K J) : Type u_1)
rw :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        (↑(↑((idealSetEquiv K J :
                    (a : (↑(idealSet K J) : Type u_1)) →
                      (↑{a : (↑(integerSet K) : Type u_1) |
                            (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                        Type u_1))
                  a) :
              (↑(integerSet K) : Type u_1)) :
          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.{u_1} (K := K)
            (↑((idealSetEquiv K J :
                    (a : (↑(idealSet K J) : Type u_1)) →
                      (↑{a : (↑(integerSet K) : Type u_1) |
                            (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                        Type u_1))
                  a) :
              (↑(integerSet K) : Type u_1))) :
        ℝ) :
      ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)

Tactic:
rw [intNorm_coe, idealSetEquiv_apply]

Premises used: NumberField.mixedEmbedding.fundamentalCone.intNorm_coe, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
h :
  { a : (↑(integerSet K) : Type u_1) // (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑J : Ideal (𝓞 K)) } =
      (↑{a : (↑(integerSet K) : Type u_1) | (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
        Type u_1) →
    ∀ (x : { a : (↑(integerSet K) : Type u_1) // (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑J : Ideal (𝓞 K)) }),
      Eq (α := ℝ)
          ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑(↑x : (↑(integerSet K) : Type u_1)) : mixedSpace K) : ℝ)
          ((↑n : ℝ) : ℝ) ↔
        Eq (α := ℝ)
          ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              (↑((Equiv.symm (idealSetEquiv K J) :
                      (a :
                          (↑{a : (↑(integerSet K) : Type u_1) |
                                (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                            Type u_1)) →
                        (↑(idealSet K J) : Type u_1))
                    x) :
                mixedSpace K) :
            ℝ)
          ((↑n : ℝ) : ℝ)
⊢ { a : (↑(idealSet K J) : Type u_1) //
      Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ) } ≃
    { a : { a : (↑(integerSet K) : Type u_1) // (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑J : Ideal (𝓞 K)) } //
      Eq (α := ℝ)
        ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑(↑a : (↑(integerSet K) : Type u_1)) : mixedSpace K) : ℝ)
        ((↑n : ℝ) : ℝ) }

Tactic:
convert! (Equiv.subtypeEquivOfSubtype (idealSetEquiv K J).symm).symm using 3

Premises used: NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv, Equiv.symm, Equiv.subtypeEquivOfSubtype
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
e_1 :
  { a : (↑(integerSet K) : Type u_1) // (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑J : Ideal (𝓞 K)) } =
    (↑{a : (↑(integerSet K) : Type u_1) | (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
      Type u_1)
x_1 : { a : (↑(integerSet K) : Type u_1) // (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑J : Ideal (𝓞 K)) }
h h₁ :
  Eq (α := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑(↑x_1 : (↑(integerSet K) : Type u_1)) : mixedSpace K) : ℝ)
      ((↑n : ℝ) : ℝ) ↔
    Eq (α := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑(↑x_1 : (↑(integerSet K) : Type u_1)) : mixedSpace K) : ℝ)
      ((↑n : ℝ) : ℝ)
⊢ Eq (α := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑(↑x_1 : (↑(integerSet K) : Type u_1)) : mixedSpace K) : ℝ)
      ((↑n : ℝ) : ℝ) ↔
    Eq (α := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          (↑((Equiv.symm (idealSetEquiv K J) :
                  (a :
                      (↑{a : (↑(integerSet K) : Type u_1) |
                            (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                        Type u_1)) →
                    (↑(idealSet K J) : Type u_1))
                x_1) :
            mixedSpace K) :
        ℝ)
      ((↑n : ℝ) : ℝ)

Tactic:
rw [idealSetEquiv_symm_apply]

Premises used: NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_symm_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
x_1 : (↑(integerSet K) : Type u_1)
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑x_1 : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ) ∧
      (↑(preimageOfMemIntegerSet x_1) : 𝓞 K) ∈ (↑J : Ideal (𝓞 K)) ↔
    (↑(preimageOfMemIntegerSet x_1) : 𝓞 K) ∈ (↑J : Ideal (𝓞 K)) ∧
      Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑x_1 : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ)

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
h :
  ∀
    (x :
      { a : (↑(integerSet K) : Type u_1) //
        Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ) }),
    (↑(preimageOfMemIntegerSet (↑x : (↑(integerSet K) : Type u_1))) : 𝓞 K) ∈ (↑J : Ideal (𝓞 K)) ↔
      (↑J : Ideal (𝓞 K)) ∣
        (↑(↑((integerSetEquivNorm K n :
                      (a :
                          { a : (↑(integerSet K) : Type u_1) //
                            (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) = (↑n : ℝ) }) →
                        { I : ↥(Ideal (𝓞 K))⁰ //
                            IsPrincipal (↑I : Ideal (𝓞 K)) ∧
                              (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) = n } ×
                          ↥(Units.torsion K))
                    x).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K))
⊢ { a :
      { a : (↑(integerSet K) : Type u_1) //
        Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ) } //
      (↑(preimageOfMemIntegerSet (↑a : (↑(integerSet K) : Type u_1))) : 𝓞 K) ∈ (↑J : Ideal (𝓞 K)) } ≃
    { I :
      { I : ↥(Ideal (𝓞 K))⁰ //
          IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) = n } ×
        ↥(Units.torsion K) //
      (↑J : Ideal (𝓞 K)) ∣ (↑(↑I.1 : ↥(Ideal (𝓞 K))⁰) : Ideal (𝓞 K)) }

Tactic:
convert! Equiv.subtypeEquivOfSubtype (p := fun I ↦ J.1 ∣ I.1) (integerSetEquivNorm K n)

Premises used: NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm, Equiv.subtypeEquivOfSubtype
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
x_1 :
  { a : (↑(integerSet K) : Type u_1) //
    Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ) }
h :
  (↑(preimageOfMemIntegerSet (↑x_1 : (↑(integerSet K) : Type u_1))) : 𝓞 K) ∈ (↑J : Ideal (𝓞 K)) ↔
    (↑J : Ideal (𝓞 K)) ∣ Ideal.span {(↑(preimageOfMemIntegerSet (↑x_1 : (↑(integerSet K) : Type u_1))) : 𝓞 K)}
h₁ h₂ :
  (↑(preimageOfMemIntegerSet (↑x_1 : (↑(integerSet K) : Type u_1))) : 𝓞 K) ∈ (↑J : Ideal (𝓞 K)) ↔
    (↑(preimageOfMemIntegerSet (↑x_1 : (↑(integerSet K) : Type u_1))) : 𝓞 K) ∈ (↑J : Ideal (𝓞 K))
⊢ (↑(preimageOfMemIntegerSet (↑x_1 : (↑(integerSet K) : Type u_1))) : 𝓞 K) ∈ (↑J : Ideal (𝓞 K)) ↔
    (↑J : Ideal (𝓞 K)) ∣
      (↑(↑((integerSetEquivNorm K n :
                    (a :
                        { a : (↑(integerSet K) : Type u_1) //
                          (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) = (↑n : ℝ) }) →
                      { I : ↥(Ideal (𝓞 K))⁰ //
                          IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) = n } ×
                        ↥(Units.torsion K))
                  x_1).1 :
            ↥(Ideal (𝓞 K))⁰) :
        Ideal (𝓞 K))

Tactic:
rw [integerSetEquivNorm_apply_fst, dvd_span_singleton]

Premises used: NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, Ideal.dvd_span_singleton
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
x_1 : ↥(Units.torsion K)
x_2 : ↥(Ideal (𝓞 K))⁰
rw rw₁ :
  (↑J : Ideal (𝓞 K)) ∣ (↑x_2 : Ideal (𝓞 K)) ∧
      IsPrincipal (↑x_2 : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑x_2 : Ideal (𝓞 K)) = n ↔
    (↑J : Ideal (𝓞 K)) ∣ (↑x_2 : Ideal (𝓞 K)) ∧
      IsPrincipal (↑x_2 : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑x_2 : Ideal (𝓞 K)) = n
⊢ (IsPrincipal (↑x_2 : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑x_2 : Ideal (𝓞 K)) = n) ∧
      (↑J : Ideal (𝓞 K)) ∣ (↑x_2 : Ideal (𝓞 K)) ↔
    (↑J : Ideal (𝓞 K)) ∣ (↑x_2 : Ideal (𝓞 K)) ∧
      IsPrincipal (↑x_2 : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑x_2 : Ideal (𝓞 K)) = n

Tactic:
rw [and_comm]

Premises used: and_comm