awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
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))⁰
⊢ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ∧
      (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C ↔
    Eq (α := ClassGroup (𝓞 K))
        ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K))
            (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x)
              (↑(↑((Equiv.dvd J : (a : ↥(Ideal (𝓞 K))⁰) → { a : ↥(Ideal (𝓞 K))⁰ // J ∣ a }) I) : ↥(Ideal (𝓞 K))⁰) :
                Ideal (𝓞 K))
              ⋯) :
          ClassGroup (𝓞 K))
        (1 : ClassGroup (𝓞 K)) ∧
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
              (↑(↑((Equiv.dvd J : (a : ↥(Ideal (𝓞 K))⁰) → { a : ↥(Ideal (𝓞 K))⁰ // J ∣ a }) I) : ↥(Ideal (𝓞 K))⁰) :
                Ideal (𝓞 K))) :
          ℝ) ≤
        s * (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ)
have simp_rw : 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: simp_rw [Equiv.dvd_apply, Submonoid.coe_mul, ← Submonoid.mul_def, _root_.map_mul, hJ,
    inv_mul_eq_one, Nat.cast_mul, mul_comm s, eq_comm, and_comm, and_congr_left_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
⊢ (↑({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 }
have refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine (((toMixed K).toEquiv.image _).trans (Equiv.subtypeEquivProp ?_)).trans
    (Equiv.subtypeSubtypeEquivSubtypeInter _ (mixedEmbedding.norm · ≤ s)).symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x : mixedSpace K
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have 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
Tactic: simp_rw [mem_idealSet, Set.mem_image, Set.mem_inter_iff, Set.mem_preimage, SetLike.mem_coe,
    mem_idealLattice, FractionalIdeal.coe_mk0]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x : 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)) ∧
        (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 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) : ℝ)|)))
have 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})
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (hypothesis)
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})
⊢ 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) : ℝ)|)))
have 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)
Tactic: have h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K := by ext; simp
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
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)
⊢ 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) : ℝ)|)))
have 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) : ℝ)|)))
Tactic: obtain ⟨J, hJ⟩ := ClassGroup.mk0_surjective C⁻¹
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (hypothesis)
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⁻¹
⊢ 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) : ℝ)|)))
have h₃ : 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))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
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
⊢ 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) : ℝ)⁻¹
have 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)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
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
⊢ π ^ 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)
have 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)
Tactic: rw [mul_inv_cancel_right₀ h₃]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
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
x : euclidean.mixedSpace K
x_1 : ℝ
h_1 :
  Membership.mem (γ := Set (euclidean.mixedSpace K))
    (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K) (fundamentalCone K))
    x
h : 0 < x_1
⊢ Membership.mem (γ := Set (euclidean.mixedSpace K))
    (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K) (fundamentalCone K))
    (x_1 • x)
have convert_1 : Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
  ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) (x_1 • x) : mixedSpace K)
Tactic: rwa [Set.mem_preimage, map_smul, smul_mem_iff_mem h.ne']