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
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)
⊢ (↑((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)
have rw₁ : (↑(↑a : (↑(integerSet K) : Type u_1)) : mixedSpace K) = (↑(↑a : (↑(integerSet K) : Type u_1)) : mixedSpace K)
Tactic: rw [← (idealSetEquiv_apply ((idealSetEquiv K J).symm a)), Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : (↑(idealSet K J) : Type u_1)
⊢ 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) : ℝ)
have 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) : ℝ)
Tactic: rw [intNorm_coe, idealSetEquiv_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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) : ℝ)
⊢ 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) : ℝ)
have rw₁ : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
Tactic: rw [intNorm_coe, idealSetEquiv_apply]
-- 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 : ℝ
J : ↥(Ideal (𝓞 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 : ℝ) : ℝ) }
have 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 : ℝ) : ℝ)
Tactic: convert! (Equiv.subtypeEquivOfSubtype (idealSetEquiv K J).symm).symm using 3
-- 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 : ℝ
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)) }
⊢ 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 : ℝ) : ℝ)
have 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 : ℝ) : ℝ)
Tactic: rw [idealSetEquiv_symm_apply]
-- 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 : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
⊢ { 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)) }
have 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))
Tactic: convert! Equiv.subtypeEquivOfSubtype (p := fun I ↦ J.1 ∣ I.1) (integerSetEquivNorm K n)
-- 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 : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
x_1 :
  { a : (↑(integerSet K) : Type u_1) //
    Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ) }
⊢ (↑(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))
have 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)}
Tactic: rw [integerSetEquivNorm_apply_fst, dvd_span_singleton]
-- 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 : ℝ
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)}
⊢ (↑(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))
have 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))
Tactic: rw [integerSetEquivNorm_apply_fst, dvd_span_singleton]
-- 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 : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
x_1 : ↥(Units.torsion 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)) ↔
    (↑J : Ideal (𝓞 K)) ∣ (↑x_2 : Ideal (𝓞 K)) ∧
      IsPrincipal (↑x_2 : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑x_2 : Ideal (𝓞 K)) = n
have 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
Tactic: rw [and_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
⊢ Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ //
          (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
            IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } *
      torsionOrder K =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
have inl : ∀ (hs : 0 ≤ s),
  Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ //
          (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
            IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } *
      torsionOrder K =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
Tactic: obtain hs | hs := le_or_gt 0 s
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
inl :
  ∀ (hs : 0 ≤ s),
    Nat.card.{u_1}
          { I : ↥(Ideal (𝓞 K))⁰ //
            (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
              IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } *
        torsionOrder K =
      Nat.card.{u_1}
        { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
⊢ Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ //
          (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
            IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } *
      torsionOrder K =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
have inr : ∀ (hs : s < 0),
  Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ //
          (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
            IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } *
      torsionOrder K =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
Tactic: obtain hs | hs := le_or_gt 0 s
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ //
          (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
            IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } *
      torsionOrder K =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
have inl : Nat.card.{u_1}
      { I : ↥(Ideal (𝓞 K))⁰ //
        (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
          IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) ≤ ⌊s⌋₊ } *
    torsionOrder K =
  Nat.card.{u_1}
    { a : (↑(idealSet K J) : Type u_1) //
      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)) ≤
        ⌊s⌋₊ }
Tactic: simp_rw [← intNorm_idealSetEquiv_apply, ← Nat.le_floor_iff hs]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ //
          (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
            IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) ≤ ⌊s⌋₊ } *
      torsionOrder K =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) //
        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)) ≤
          ⌊s⌋₊ }
have inl : Nat.card.{u_1}
    ({ I : ↥(Ideal (𝓞 K))⁰ //
        (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
          IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) ≤ ⌊s⌋₊ } ×
      ↥(Units.torsion K)) =
  Nat.card.{u_1}
    { a : (↑(idealSet K J) : Type u_1) //
      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)) ≤
        ⌊s⌋₊ }
Tactic: rw [torsionOrder, ← Nat.card_eq_fintype_card, ← Nat.card_prod]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a : (↑(idealSet K J) : Type u_1) //
      Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑i : ℝ) : ℝ) } ≃
    { a : (↑(idealSet K J) : Type u_1) //
      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)) =
        i }
have simp_rw : { a : (↑(idealSet K J) : Type u_1) //
    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)) =
      i } ≃
  { a : (↑(idealSet K J) : Type u_1) //
    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)) =
      i }
Tactic: simp_rw [← intNorm_idealSetEquiv_apply, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a :
      { I : ↥(Ideal (𝓞 K))⁰ //
          (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
            IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) ≤ ⌊s⌋₊ } ×
        ↥(Units.torsion K) //
      (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑(↑a.1 : ↥(Ideal (𝓞 K))⁰) : Ideal (𝓞 K)) = i } ≃
    { b :
      { a : (↑(idealSet K J) : Type u_1) //
        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)) ≤
          ⌊s⌋₊ } //
      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))
                (↑b : (↑(idealSet K J) : Type u_1))) :
            (↑(integerSet K) : Type u_1)) =
        i }
have calc : { a : (↑(idealSet K J) : Type u_1) //
    Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑i : ℝ) : ℝ) } ≃
  { a : (↑(idealSet K J) : Type u_1) //
    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)) =
      i }
Tactic: calc _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // _ ∧ _ ∧ _} // absNorm I.1.1 = i} × torsion K :=
        Equiv.prodSubtypeFstEquivSubtypeProd
      _ ≃ {I : (Ideal (𝓞 K))⁰ // (_ ∧ _ ∧ absNorm I.1 ≤ ⌊s⌋₊) ∧ absNorm I.1 = i}
            × torsion K := Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeSubtypeEquivSubtypeInter
        (p := fun I : (Ideal (𝓞 K))⁰ ↦ J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 ≤ ⌊s⌋₊)
        (q := fun I ↦ absNorm I.1 = i))
      _ ≃ {I : (Ideal (𝓞 K))⁰ // J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 = i}
            × torsion K := Equiv.prodCongrLeft fun _ ↦ Equiv.subtypeEquivRight fun _ ↦ by grind
      _ ≃ {a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) = i} :=
            (idealSetEquivNorm K J i).symm
      _ ≃ {a : idealSet K J // intNorm (idealSetEquiv K J a).1 = i} := by
        simp_rw [← intNorm_idealSetEquiv_apply, Nat.cast_inj]
        rfl
      _ ≃ {b : {a : idealSet K J // intNorm (idealSetEquiv K J a).1 ≤ ⌊s⌋₊} //
            intNorm (idealSetEquiv K J b).1 = i} :=
        (Equiv.subtypeSubtypeEquivSubtype fun h ↦ Finset.mem_Iic.mp (h ▸ hi)).symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : s < 0
⊢ Nat.card.{u_1}
        { I : ↥(Ideal (𝓞 K))⁰ //
          (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
            IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } *
      torsionOrder K =
    Nat.card.{u_1}
      { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
have inr : Nat.card.{u_1}
      { I : ↥(Ideal (𝓞 K))⁰ // (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧ IsPrincipal (↑I : Ideal (𝓞 K)) ∧ False } *
    torsionOrder K =
  Nat.card.{u_1}
    { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }
Tactic: simp_rw [lt_iff_not_ge.mp (lt_of_lt_of_le hs (Nat.cast_nonneg _)), lt_iff_not_ge.mp
      (lt_of_lt_of_le hs (mixedEmbedding.norm_nonneg _)), and_false, Nat.card_of_isEmpty,
      zero_mul]