awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
I : ↥(Ideal (𝓞 K))⁰
⊢ C = (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I →
    ((↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ↔
      HMul.hMul (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ)
          (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) * s)

Tactic:
exact fun _ ↦
    (mul_le_mul_iff_of_pos_left (Nat.cast_pos.mpr (absNorm_pos_of_nonZeroDivisors J))).symm

Premises used: Iff.mpr, Nat.cast_pos, mul_le_mul_iff_of_pos_left, Ideal.absNorm_pos_of_nonZeroDivisors, Iff.symm
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (↑({x : euclidean.mixedSpace K |
            Membership.mem (γ := Set (euclidean.mixedSpace K))
                (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
                  (fundamentalCone K))
                x ∧
              (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
                  ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ≤
                s} ∩
          (⇑(↑(↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) : euclidean.mixedSpace K →ₗ[ℝ] mixedSpace K) :
              (a : euclidean.mixedSpace K) → mixedSpace K) ⁻¹'
            (↑(idealLattice K ((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J)) :
              Set (mixedSpace K))) :
      Type u_1) ≃
    { a : (↑(idealSet K J) : Type u_1) // (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) ≤ s }

Tactic:
refine (((toMixed K).toEquiv.image _).trans (Equiv.subtypeEquivProp ?_)).trans
    (Equiv.subtypeSubtypeEquivSubtypeInter _ (mixedEmbedding.norm · ≤ s)).symm

Premises used: ContinuousLinearEquiv.toLinearEquiv, Equiv.trans, LE.le, Equiv.subtypeEquivProp, Equiv.image, LinearEquiv.toEquiv, NumberField.mixedEmbedding.norm, NumberField.mixedEmbedding.euclidean.toMixed, Equiv.subtypeSubtypeEquivSubtypeInter, Equiv.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x : mixedSpace K
h :
  (∃ (x_1 : euclidean.mixedSpace K),
      (Membership.mem (γ := Set (euclidean.mixedSpace K))
            {x : euclidean.mixedSpace K |
              Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
                  ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ∧
                (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
                    ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ≤
                  s}
            x_1 ∧
          ∃ y ∈ (↑(↑(↑J : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K) : Set K),
            Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) y : mixedSpace K)
              (((↑(↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
                      euclidean.mixedSpace K →ₗ[ℝ] mixedSpace K) :
                    (a : euclidean.mixedSpace K) → mixedSpace K)
                  x_1 :
                mixedSpace K)) ∧
        (LinearEquiv.toEquiv (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
              (a : euclidean.mixedSpace K) → mixedSpace K)
            x_1 =
          x) ↔
    (Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
        ∃ a ∈ (↑J : Ideal (𝓞 K)), (mixedEmbedding K : (a : K) → mixedSpace K) (↑a : K) = x) ∧
      (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x ≤ s
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp_rw [mem_idealSet, Set.mem_image, Set.mem_inter_iff, Set.mem_preimage, SetLike.mem_coe,
    mem_idealLattice, FractionalIdeal.coe_mk0]

Premises used: NumberField.mixedEmbedding.mem_idealLattice, Set.mem_inter_iff, Set.mem_image, SetLike.mem_coe, NumberField.mixedEmbedding.fundamentalCone.mem_idealSet, FractionalIdeal.coe_mk0, Set.mem_preimage
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
w : euclidean.mixedSpace K
hx₁ :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
    ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) w : mixedSpace K)
hx₂ :
  (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) w : mixedSpace K) ≤
    s
x : 𝓞 K
hx₃ : x ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h :
  Eq (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) x) : mixedSpace K)
    (((↑(↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) : euclidean.mixedSpace K →ₗ[ℝ] mixedSpace K) :
          (a : euclidean.mixedSpace K) → mixedSpace K)
        w :
      mixedSpace K)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
⟨⟨hx₁, x, hx₃, h⟩, hx₂⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
w : euclidean.mixedSpace K
hx₁ :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
    ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) w : mixedSpace K)
hx₂ :
  (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) w : mixedSpace K) ≤
    s
x : 𝓞 K
hx₃ : x ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h :
  Eq (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) x) : mixedSpace K)
    (((↑(↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) : euclidean.mixedSpace K →ₗ[ℝ] mixedSpace K) :
          (a : euclidean.mixedSpace K) → mixedSpace K)
        w :
      mixedSpace K)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact ⟨⟨hx₁, x, hx₃, h⟩, hx₂⟩
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x : 𝓞 K
hx₂ : x ∈ (↑J : Ideal (𝓞 K))
hx₃ :
  (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K) ≤
    s
hx₁ :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
⊢ (↑x : K) ∈ (↑(↑(↑J : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K) : Set K)

Tactic:
simp [hx₂]
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x : 𝓞 K
hx₂ : x ∈ (↑J : Ideal (𝓞 K))
hx₃ :
  (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K) ≤
    s
hx₁ :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)
⊢ ∃ (x_1 : euclidean.mixedSpace K),
    (Membership.mem (γ := Set (euclidean.mixedSpace K))
          {x : euclidean.mixedSpace K |
            Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
                ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ∧
              (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
                  ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ≤
                s}
          x_1 ∧
        ∃ y ∈ (↑(↑(↑J : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K) : Set K),
          Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) y : mixedSpace K)
            (((↑(↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
                    euclidean.mixedSpace K →ₗ[ℝ] mixedSpace K) :
                  (a : euclidean.mixedSpace K) → mixedSpace K)
                x_1 :
              mixedSpace K)) ∧
      Eq (α := mixedSpace K)
        ((LinearEquiv.toEquiv (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
              (a : euclidean.mixedSpace K) → mixedSpace K)
            x_1 :
          mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K)

Tactic:
exact ⟨(toMixed K).symm (mixedEmbedding K x), ⟨⟨hx₁, hx₃⟩, ⟨(x : K), by simp [hx₂], rfl⟩⟩, rfl⟩
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
⊢ ∀ (s : ℝ),
    Eq (α := Set (euclidean.mixedSpace K))
      {x : euclidean.mixedSpace K |
        Membership.mem (γ := Set (euclidean.mixedSpace K))
            (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
              (fundamentalCone K))
            x ∧
          (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ≤
            s}
      (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
        {x : mixedSpace K |
          Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
            (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x ≤ s})

Tactic:
have h₁ : ∀ s : ℝ,
    {x | x ∈ toMixed K ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm (toMixed K x) ≤ s} =
      toMixed K ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s} := fun _ ↦ rfl
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    Eq (α := Set (euclidean.mixedSpace K))
      {x : euclidean.mixedSpace K |
        Membership.mem (γ := Set (euclidean.mixedSpace K))
            (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
              (fundamentalCone K))
            x ∧
          (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ≤
            s}
      (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
        {x : mixedSpace K |
          Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
            (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x ≤ s})
h :
  ∀ (x : mixedSpace K),
    Membership.mem (γ := Set (mixedSpace K))
        {x : mixedSpace K |
          Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
            LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)}
        x ↔
      Membership.mem (γ := Set (mixedSpace K)) (normLeOne K) x
⊢ Eq (α := Set (mixedSpace K))
    {x : mixedSpace K |
      Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
        LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)}
    (normLeOne K)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    Eq (α := Set (euclidean.mixedSpace K))
      {x : euclidean.mixedSpace K |
        Membership.mem (γ := Set (euclidean.mixedSpace K))
            (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
              (fundamentalCone K))
            x ∧
          (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ≤
            s}
      (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
        {x : mixedSpace K |
          Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
            (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x ≤ s})
x : mixedSpace K
⊢ Membership.mem (γ := Set (mixedSpace K))
      {x : mixedSpace K |
        Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
          LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)}
      x ↔
    Membership.mem (γ := Set (mixedSpace K)) (normLeOne K) x

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    Eq (α := Set (euclidean.mixedSpace K))
      {x : euclidean.mixedSpace K |
        Membership.mem (γ := Set (euclidean.mixedSpace K))
            (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
              (fundamentalCone K))
            x ∧
          (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ≤
            s}
      (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
        {x : mixedSpace K |
          Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
            (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x ≤ s})
⊢ Eq (α := Set (mixedSpace K))
    {x : mixedSpace K |
      Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
        LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)}
    (normLeOne K)

Tactic:
have h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K := by ext; simp
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    Eq (α := Set (euclidean.mixedSpace K))
      {x : euclidean.mixedSpace K |
        Membership.mem (γ := Set (euclidean.mixedSpace K))
            (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
              (fundamentalCone K))
            x ∧
          (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ≤
            s}
      (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
        {x : mixedSpace K |
          Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
            (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x ≤ s})
h₂ :
  Eq (α := Set (mixedSpace K))
    {x : mixedSpace K |
      Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
        LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)}
    (normLeOne K)
obtain :
  ∀ (J : ↥(Ideal (𝓞 K))⁰) (hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹),
    Tendsto
      (fun (s : ℝ) ↦
        (↑(Nat.card.{u_1}
                { I : ↥(Ideal (𝓞 K))⁰ //
                  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ∧
                    (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C }) :
            ℝ) /
          s)
      atTop
      (𝓝
        (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K /
          ((↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|)))
⊢ Tendsto
    (fun (s : ℝ) ↦
      (↑(Nat.card.{u_1}
              { I : ↥(Ideal (𝓞 K))⁰ //
                (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ∧
                  (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C }) :
          ℝ) /
        s)
    atTop
    (𝓝
      (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K /
        ((↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|)))

Tactic:
obtain ⟨J, hJ⟩ := ClassGroup.mk0_surjective C⁻¹

Premises used: Inv.inv, ClassGroup.mk0_surjective
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    Eq (α := Set (euclidean.mixedSpace K))
      {x : euclidean.mixedSpace K |
        Membership.mem (γ := Set (euclidean.mixedSpace K))
            (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
              (fundamentalCone K))
            x ∧
          (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ≤
            s}
      (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
        {x : mixedSpace K |
          Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
            (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x ≤ s})
h₂ :
  Eq (α := Set (mixedSpace K))
    {x : mixedSpace K |
      Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
        LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)}
    (normLeOne K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
⊢ Ne (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) 0

Tactic:
have h₃ : (absNorm J.1 : ℝ) ≠ 0 := (Nat.cast_ne_zero.mpr (absNorm_ne_zero_of_nonZeroDivisors J))
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    Eq (α := Set (euclidean.mixedSpace K))
      {x : euclidean.mixedSpace K |
        Membership.mem (γ := Set (euclidean.mixedSpace K))
            (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
              (fundamentalCone K))
            x ∧
          (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ≤
            s}
      (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
        {x : mixedSpace K |
          Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
            (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x ≤ s})
h₂ :
  Eq (α := Set (mixedSpace K))
    {x : mixedSpace K |
      Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
        LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)}
    (normLeOne K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
h₃ : Ne (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) 0
h :
  π ^ nrComplexPlaces K * regulator K * (↑(torsionOrder K) : ℝ)⁻¹ * (√|(↑(discr K) : ℝ)|)⁻¹ *
        HPow.hPow (α := ℝ) 2 (nrRealPlaces K) *
      HPow.hPow (α := ℝ) 2 (nrComplexPlaces K) =
    π ^ nrComplexPlaces K * regulator K * (↑(torsionOrder K) : ℝ)⁻¹ * (√|(↑(discr K) : ℝ)|)⁻¹ *
            (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) *
          (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) 2 (nrRealPlaces K) *
      HPow.hPow (α := ℝ) 2 (nrComplexPlaces K)
⊢ HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K *
      ((↑(torsionOrder K) : ℝ)⁻¹ * (√|(↑(discr K) : ℝ)|)⁻¹) =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * π ^ nrComplexPlaces K * regulator K *
        ((↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ)⁻¹ * HPow.hPow (α := ℝ) 2 (nrComplexPlaces K) *
          (√|(↑(discr K) : ℝ)|)⁻¹) *
      HMul.hMul (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) (↑(torsionOrder K) : ℝ)⁻¹

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    Eq (α := Set (euclidean.mixedSpace K))
      {x : euclidean.mixedSpace K |
        Membership.mem (γ := Set (euclidean.mixedSpace K))
            (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
              (fundamentalCone K))
            x ∧
          (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ≤
            s}
      (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
        {x : mixedSpace K |
          Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
            (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x ≤ s})
h₂ :
  Eq (α := Set (mixedSpace K))
    {x : mixedSpace K |
      Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
        LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)}
    (normLeOne K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
h₃ : Ne (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) 0
h h₄ :
  π ^ nrComplexPlaces K * regulator K * (↑(torsionOrder K) : ℝ)⁻¹ * (√|(↑(discr K) : ℝ)|)⁻¹ *
        HPow.hPow (α := ℝ) 2 (nrRealPlaces K) *
      HPow.hPow (α := ℝ) 2 (nrComplexPlaces K) =
    π ^ nrComplexPlaces K * regulator K * (↑(torsionOrder K) : ℝ)⁻¹ * (√|(↑(discr K) : ℝ)|)⁻¹ *
        HPow.hPow (α := ℝ) 2 (nrRealPlaces K) *
      HPow.hPow (α := ℝ) 2 (nrComplexPlaces K)
⊢ π ^ nrComplexPlaces K * regulator K * (↑(torsionOrder K) : ℝ)⁻¹ * (√|(↑(discr K) : ℝ)|)⁻¹ *
        HPow.hPow (α := ℝ) 2 (nrRealPlaces K) *
      HPow.hPow (α := ℝ) 2 (nrComplexPlaces K) =
    π ^ nrComplexPlaces K * regulator K * (↑(torsionOrder K) : ℝ)⁻¹ * (√|(↑(discr K) : ℝ)|)⁻¹ *
            (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) *
          (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) 2 (nrRealPlaces K) *
      HPow.hPow (α := ℝ) 2 (nrComplexPlaces K)

Tactic:
rw [mul_inv_cancel_right₀ h₃]

Premises used: mul_inv_cancel_right₀