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)
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
convert_1 :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
    ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) (x_1 • x) : mixedSpace K)
⊢ 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 (γ := Set (mixedSpace K)) (fundamentalCone K)
  (HSMul.hSMul (β := mixedSpace K) x_1 ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K))
Tactic: rwa [Set.mem_preimage, map_smul, smul_mem_iff_mem h.ne']
-- 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
convert_1 :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone K)
    ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) (x_1 • x) : mixedSpace K)
convert_1₁ :
  Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K)
    (HSMul.hSMul (β := mixedSpace K) x_1 ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K))
⊢ 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 : mixedSpace K)
Tactic: rwa [Set.mem_preimage, map_smul, smul_mem_iff_mem h.ne']
-- 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 : 0 ≤ x_1
⊢ (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) (x_1 • x) : mixedSpace K) =
    HMul.hMul (β := ℝ) (x_1 ^ Module.finrank.{0, u_1} ℝ (euclidean.mixedSpace K))
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
        ℝ)
have convert_2 : (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
    (HSMul.hSMul (β := mixedSpace K) x_1 ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K)) =
  HMul.hMul (β := ℝ) (x_1 ^ Module.finrank.{0, u_1} ℝ (euclidean.mixedSpace K))
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
      ℝ)
Tactic: rw [map_smul, mixedEmbedding.norm_smul, euclidean.finrank, abs_of_nonneg 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 : 0 ≤ x_1
convert_2 :
  (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      (HSMul.hSMul (β := mixedSpace K) x_1
        ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K)) =
    HMul.hMul (β := ℝ) (x_1 ^ Module.finrank.{0, u_1} ℝ (euclidean.mixedSpace K))
      ((mixedEmbedding.norm : (a : mixedSpace 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_1 • x) : mixedSpace K) =
    HMul.hMul (β := ℝ) (x_1 ^ Module.finrank.{0, u_1} ℝ (euclidean.mixedSpace K))
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
        ℝ)
have convert_2₁ : HMul.hMul (β := ℝ) (|x_1| ^ Module.finrank ℚ K)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
      ℝ) =
  HMul.hMul (β := ℝ) (x_1 ^ Module.finrank.{0, u_1} ℝ (euclidean.mixedSpace K))
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
      ℝ)
Tactic: rw [map_smul, mixedEmbedding.norm_smul, euclidean.finrank, abs_of_nonneg 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 : 0 ≤ x_1
convert_2 :
  (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      (HSMul.hSMul (β := mixedSpace K) x_1
        ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K)) =
    HMul.hMul (β := ℝ) (x_1 ^ Module.finrank.{0, u_1} ℝ (euclidean.mixedSpace K))
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
        ℝ)
convert_2₁ :
  HMul.hMul (β := ℝ) (|x_1| ^ Module.finrank ℚ K)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
        ℝ) =
    HMul.hMul (β := ℝ) (x_1 ^ Module.finrank.{0, u_1} ℝ (euclidean.mixedSpace K))
      ((mixedEmbedding.norm : (a : mixedSpace 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_1 • x) : mixedSpace K) =
    HMul.hMul (β := ℝ) (x_1 ^ Module.finrank.{0, u_1} ℝ (euclidean.mixedSpace K))
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
        ℝ)
have convert_2₂ : HMul.hMul (β := ℝ) (|x_1| ^ Module.finrank ℚ K)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
      ℝ) =
  HMul.hMul (β := ℝ) (x_1 ^ Module.finrank ℚ K)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
      ℝ)
Tactic: rw [map_smul, mixedEmbedding.norm_smul, euclidean.finrank, abs_of_nonneg h]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Tendsto
    (fun (s : ℝ) ↦
      (↑(Nat.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) :
          ℝ) /
        s)
    atTop
    (𝓝
      (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K * (↑(classNumber K) : ℝ) /
        ((↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|)))
have h : HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K * (↑(classNumber K) : ℝ) /
    ((↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|) =
  ∑ c : ClassGroup (𝓞 K),
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K /
      ((↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|)
Tactic: convert!
    Filter.Tendsto.congr' ?_
      (tendsto_finsetSum Finset.univ (fun C _ ↦ tendsto_norm_le_and_mk_eq_div_atTop K C))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K * (↑(classNumber K) : ℝ) /
      ((↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|) =
    ∑ c : ClassGroup (𝓞 K),
      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 }) :
          ℝ) /
        s)
    atTop
    (𝓝
      (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K * (↑(classNumber K) : ℝ) /
        ((↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|)))
have convert_2 : EventuallyEq (β := ℝ) atTop
  (fun (b : ℝ) ↦
    ∑ c : ClassGroup (𝓞 K),
      (↑(Nat.card.{u_1}
              { I : ↥(Ideal (𝓞 K))⁰ //
                (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ b ∧
                  (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = c }) :
          ℝ) /
        b)
  fun (s : ℝ) ↦
  (↑(Nat.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) : ℝ) /
    s
Tactic: convert!
    Filter.Tendsto.congr' ?_
      (tendsto_finsetSum Finset.univ (fun C _ ↦ tendsto_norm_le_and_mk_eq_div_atTop K C))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K * (↑(classNumber K) : ℝ) /
      ((↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|) =
    ∑ c : ClassGroup (𝓞 K),
      HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K /
        ((↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|)
have h : HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K *
      (↑(Fintype.card.{u_1} (ClassGroup (𝓞 K))) : ℝ) /
    ((↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|) =
  (↑(Fintype.card.{u_1} (ClassGroup (𝓞 K))) : ℝ) *
    (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K /
      ((↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|))
Tactic: rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, classNumber]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ EventuallyEq (β := ℝ) atTop
    (fun (b : ℝ) ↦
      ∑ c : ClassGroup (𝓞 K),
        (↑(Nat.card.{u_1}
                { I : ↥(Ideal (𝓞 K))⁰ //
                  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ b ∧
                    (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = c }) :
            ℝ) /
          b)
    fun (s : ℝ) ↦
    (↑(Nat.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) :
        ℝ) /
      s
have h : ∀ (s : ℝ) (hs : 0 ≤ s),
  ∑ c : ClassGroup (𝓞 K),
      (↑(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 =
    (↑(Nat.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) :
        ℝ) /
      s
Tactic: filter_upwards [eventually_ge_atTop 0] with s hs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : ℝ
hs : 0 ≤ s
⊢ Fintype { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }
have simp_rw : Fintype { I : ↥(Ideal (𝓞 K))⁰ // (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) ≤ ⌊s⌋₊ }
Tactic: simp_rw [← Nat.le_floor_iff hs]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : ℝ
hs : 0 ≤ s
⊢ ∑ c : ClassGroup (𝓞 K),
      (↑(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 =
    (↑(Nat.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) :
        ℝ) /
      s
have h : ∀ (this : Fintype { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }),
  ∑ c : ClassGroup (𝓞 K),
      (↑(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 =
    (↑(Nat.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) :
        ℝ) /
      s
Tactic: have : Fintype {I : (Ideal (𝓞 K))⁰ // absNorm (I : Ideal (𝓞 K)) ≤ s} := by
      simp_rw [← Nat.le_floor_iff hs]
      refine @Fintype.ofFinite _ (finite_setOf_absNorm_le₀ ⌊s⌋₊)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : ℝ
hs : 0 ≤ s
this : Fintype { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }
e : (C : ClassGroup (𝓞 K)) →
  { x : { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } //
      (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) (↑x : ↥(Ideal (𝓞 K))⁰) = C } ≃
    { x : ↥(Ideal (𝓞 K))⁰ //
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑x : Ideal (𝓞 K))) : ℝ) ≤ s ∧
        (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) x = C } :=
  fun (C : ClassGroup (𝓞 K)) ↦
    Equiv.subtypeSubtypeEquivSubtypeInter
      (fun (I : ↥(Ideal (𝓞 K))⁰) ↦ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s)
      fun (I : ↥(Ideal (𝓞 K))⁰) ↦ (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C
⊢ ∑ c : ClassGroup (𝓞 K),
      (↑(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 =
    (↑(Nat.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) :
        ℝ) /
      s
have h : ∑ x : ClassGroup (𝓞 K),
    (↑(Finset.card.{u_1} (α :=
            { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s })
            {x_1 : { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } |
              (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) (↑x_1 : ↥(Ideal (𝓞 K))⁰) = x}) :
        ℝ) /
      s =
  (↑(Fintype.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) :
      ℝ) /
    s
Tactic: simp_rw [← Nat.card_congr (e _), Nat.card_eq_fintype_card, Fintype.subtype_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : ℝ
hs : 0 ≤ s
this : Fintype { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }
e : (C : ClassGroup (𝓞 K)) →
  { x : { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } //
      (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) (↑x : ↥(Ideal (𝓞 K))⁰) = C } ≃
    { x : ↥(Ideal (𝓞 K))⁰ //
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑x : Ideal (𝓞 K))) : ℝ) ≤ s ∧
        (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) x = C } :=
  fun (C : ClassGroup (𝓞 K)) ↦
    Equiv.subtypeSubtypeEquivSubtypeInter
      (fun (I : ↥(Ideal (𝓞 K))⁰) ↦ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s)
      fun (I : ↥(Ideal (𝓞 K))⁰) ↦ (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C
⊢ ∑ x : ClassGroup (𝓞 K),
      (↑(Finset.card.{u_1} (α :=
              { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s })
              {x_1 : { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } |
                (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) (↑x_1 : ↥(Ideal (𝓞 K))⁰) = x}) :
          ℝ) /
        s =
    (↑(Fintype.card.{u_1}
            { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) :
        ℝ) /
      s
have h : ∑ x : ClassGroup (𝓞 K),
    (↑(Finset.card.{u_1} (α :=
            { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s })
            {x_1 : { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } |
              (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) (↑x_1 : ↥(Ideal (𝓞 K))⁰) = x}) :
        ℝ) /
      s =
  (↑(Finset.card.{u_1} (α :=
          { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) Finset.univ) :
      ℝ) /
    s
Tactic: rw [Fintype.card, Finset.card_eq_sum_card_fiberwise (f := fun I ↦ ClassGroup.mk0 I.1)
      (t := Finset.univ) (fun _ _ ↦ Finset.mem_univ _), Nat.cast_sum, Finset.sum_div]