awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
⊢ ∃ (I : ↥(Ideal (𝓞 K))⁰),
    (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C ∧
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
have refine_1 : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C
Tactic: refine ⟨I, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
refine_1 : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C
⊢ ∃ (I : ↥(Ideal (𝓞 K))⁰),
    (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C ∧
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
have refine_2 : (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
  (4 / π) ^ nrComplexPlaces K *
    ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
Tactic: refine ⟨I, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀
this_1 : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
this :
  Eq (α := ClassGroup (𝓞 K)) ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I : ClassGroup (𝓞 K))
    (((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J)⁻¹ : ClassGroup (𝓞 K))
⊢ (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C
have rw : ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J)⁻¹ = C
Tactic: rw [this, hJ, inv_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀
this_1 : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
this :
  Eq (α := ClassGroup (𝓞 K)) ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I : ClassGroup (𝓞 K))
    (((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J)⁻¹ : ClassGroup (𝓞 K))
rw : ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J)⁻¹ = C
⊢ (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C
have rw₁ : C⁻¹⁻¹ = C
Tactic: rw [this, hJ, inv_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀
this_1 : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
this :
  Eq (α := ClassGroup (𝓞 K)) ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I : ClassGroup (𝓞 K))
    (((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J)⁻¹ : ClassGroup (𝓞 K))
rw : ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J)⁻¹ = C
rw₁ : C⁻¹⁻¹ = C
⊢ (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C
have rw₂ : C = C
Tactic: rw [this, hJ, inv_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
⊢ (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C
have refine_1 : Eq (α := ClassGroup (𝓞 K)) ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I : ClassGroup (𝓞 K))
  (((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J)⁻¹ : ClassGroup (𝓞 K))
Tactic: suffices ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ by rw [this, hJ, inv_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
⊢ (↑I : Ideal (𝓞 K)) * (↑J : Ideal (𝓞 K)) = span {a}
have rw : (↑J : Ideal (𝓞 K)) * (↑I : Ideal (𝓞 K)) = span {a}
Tactic: rw [mul_comm, hI]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
rw : (↑J : Ideal (𝓞 K)) * (↑I : Ideal (𝓞 K)) = span {a}
⊢ (↑I : Ideal (𝓞 K)) * (↑J : Ideal (𝓞 K)) = span {a}
have rw₁ : (↑J : Ideal (𝓞 K)) * (↑I : Ideal (𝓞 K)) = (↑J : Ideal (𝓞 K)) * I₀
Tactic: rw [mul_comm, hI]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
⊢ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
have refine_2 : ∀ (I₀ : Ideal (𝓞 K))
  (h_nm :
    HMul.hMul (α := ℝ) (↑(Submodule.cardQuot (↑J : Ideal (𝓞 K))) : ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) I₀) : ℝ) ≤
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) *
        ((4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)))
  (hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀) (this : I₀ ≠ 0),
  let I :=
    Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ sorry;
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
Tactic: rw [← FractionalIdeal.absNorm_span_singleton (𝓞 K), Algebra.linearMap_apply,
      ← FractionalIdeal.coeIdeal_span_singleton, FractionalIdeal.coeIdeal_absNorm, hI, map_mul,
      cast_mul, Rat.cast_mul, absNorm_apply, Rat.cast_natCast, Rat.cast_natCast,
      FractionalIdeal.coe_mk0, FractionalIdeal.coeIdeal_absNorm, Rat.cast_natCast, mul_div_assoc,
      mul_assoc, mul_assoc] at h_nm
Cleared hypotheses: h_nm, I₀, hI, this, I
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
I₀ : Ideal (𝓞 K)
h_nm :
  HMul.hMul (α := ℝ) (↑(Submodule.cardQuot (↑J : Ideal (𝓞 K))) : ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) I₀) : ℝ) ≤
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) *
      ((4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|))
hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
⊢ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
have refine_2 : LT.lt (α := ℝ) 0 (↑(Submodule.cardQuot (↑J : Ideal (𝓞 K))) : ℝ)
Tactic: refine le_of_mul_le_mul_of_pos_left h_nm ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) →
      Submodule.IsPrincipal (↑I : Ideal (𝓞 K))
⊢ IsPrincipalIdealRing.{u_1} (𝓞 K)
have rw : ∃ (x : ClassGroup (𝓞 K)), ∀ (y : ClassGroup (𝓞 K)), y = x
Tactic: rw [← classNumber_eq_one_iff, classNumber, Fintype.card_eq_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) →
      Submodule.IsPrincipal (↑I : Ideal (𝓞 K))
⊢ ∃ (x : ClassGroup (𝓞 K)), ∀ (y : ClassGroup (𝓞 K)), y = x
have refine : ∀ (C : ClassGroup (𝓞 K)), C = 1
Tactic: refine ⟨1, fun C ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) →
      Submodule.IsPrincipal (↑I : Ideal (𝓞 K))
C : ClassGroup (𝓞 K)
⊢ C = 1
have obtain : ∀ (I : ↥(Ideal (𝓞 K))⁰)
  (hI :
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
      (4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)),
  Eq (α := ClassGroup (𝓞 K)) ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I : ClassGroup (𝓞 K))
    (1 : ClassGroup (𝓞 K))
Tactic: obtain ⟨I, rfl, hI⟩ := exists_ideal_in_class_of_norm_le C
Cleared hypotheses: C
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑I : Ideal (𝓞 K)).IsPrime →
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
          (4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) →
        Submodule.IsPrincipal (↑I : Ideal (𝓞 K))
⊢ IsPrincipalIdealRing.{u_1} (𝓞 K)
have refine : ∀ (I : ↥(Ideal (𝓞 K))⁰)
  (hI :
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
      (4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)),
  Submodule.IsPrincipal (↑I : Ideal (𝓞 K))
Tactic: refine isPrincipalIdealRing_of_isPrincipal_of_norm_le (fun I hI ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑I : Ideal (𝓞 K)).IsPrime →
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
          (4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) →
        Submodule.IsPrincipal (↑I : Ideal (𝓞 K))
I : ↥(Ideal (𝓞 K))⁰
hI :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
⊢ Submodule.IsPrincipal (↑I : Ideal (𝓞 K))
have rw : Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K))
  (UniqueFactorizationMonoid.normalizedFactors (↑I : Ideal (𝓞 K))).prod
Tactic: rw [← mem_isPrincipalSubmonoid_iff,
    ← Ideal.prod_normalizedFactors_eq_self (nonZeroDivisors.coe_ne_zero I)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑I : Ideal (𝓞 K)).IsPrime →
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
          (4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) →
        Submodule.IsPrincipal (↑I : Ideal (𝓞 K))
I : ↥(Ideal (𝓞 K))⁰
hI :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
⊢ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K))
    (UniqueFactorizationMonoid.normalizedFactors (↑I : Ideal (𝓞 K))).prod
have refine : ∀ (J : Ideal (𝓞 K)) (hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors (↑I : Ideal (𝓞 K))),
  Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K)) J
Tactic: refine Submonoid.multiset_prod_mem _ _ (fun J hJ ↦ mem_isPrincipalSubmonoid_iff.mp ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑I : Ideal (𝓞 K)).IsPrime →
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
          (4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) →
        Submodule.IsPrincipal (↑I : Ideal (𝓞 K))
I : ↥(Ideal (𝓞 K))⁰
hI :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
J : Ideal (𝓞 K)
hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors (↑I : Ideal (𝓞 K))
⊢ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K)) J
have pos : ∀ (hJ0 : J = 0), Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K)) J
Tactic: by_cases hJ0 : J = 0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑I : Ideal (𝓞 K)).IsPrime →
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
          (4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) →
        Submodule.IsPrincipal (↑I : Ideal (𝓞 K))
I : ↥(Ideal (𝓞 K))⁰
hI :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
J : Ideal (𝓞 K)
hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors (↑I : Ideal (𝓞 K))
pos : ∀ (hJ0 : J = 0), Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K)) J
⊢ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K)) J
have neg : ∀ (hJ0 : ¬J = 0), Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K)) J
Tactic: by_cases hJ0 : J = 0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑I : Ideal (𝓞 K)).IsPrime →
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
          (4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) →
        Submodule.IsPrincipal (↑I : Ideal (𝓞 K))
I : ↥(Ideal (𝓞 K))⁰
hI :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
J : Ideal (𝓞 K)
hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors (↑I : Ideal (𝓞 K))
hJ0 : ¬J = 0
⊢ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K)) J
have neg : Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K))
  (↑(Subtype.mk (p := Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰) J sorry) : Ideal (𝓞 K))
Tactic: rw [← Subtype.coe_mk J (mem_nonZeroDivisors_of_ne_zero hJ0)]