awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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_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₀ ⋯;
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
      (4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
⊢ (↑((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

Premises used: FractionalIdeal.coeIdeal_span_singleton, Rat.cast_mul, mul_assoc, mul_div_assoc, Algebra.linearMap_apply, FractionalIdeal.absNorm_span_singleton, map_mul, Ideal.absNorm_apply, Nat.cast_mul, Rat.cast_natCast, NumberField.RingOfIntegers, FractionalIdeal.coeIdeal_absNorm, FractionalIdeal.coe_mk0
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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) : ℝ)|)

Tactic:
le_of_mul_le_mul_of_pos_left h_nm ?_

Premises used: le_of_mul_le_mul_of_pos_left
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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₀ ⋯
refine_2 : LT.lt (α := ℝ) 0 (↑(Submodule.cardQuot (↑J : Ideal (𝓞 K))) : ℝ)
⊢ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)

Tactic:
refine le_of_mul_le_mul_of_pos_left h_nm ?_

Premises used: le_of_mul_le_mul_of_pos_left
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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₀ ⋯
⊢ LT.lt (α := ℝ) 0 (↑(Submodule.cardQuot (↑J : Ideal (𝓞 K))) : ℝ)

Tactic:
cast_pos.mpr <| pos_of_ne_zero <| absNorm_ne_zero_of_nonZeroDivisors J

Premises used: Iff.mpr, Nat.cast_pos, pos_of_ne_zero, Ideal.absNorm_ne_zero_of_nonZeroDivisors
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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₀ ⋯
⊢ LT.lt (α := ℝ) 0 (↑(Submodule.cardQuot (↑J : Ideal (𝓞 K))) : ℝ)

Tactic:
exact cast_pos.mpr <| pos_of_ne_zero <| absNorm_ne_zero_of_nonZeroDivisors J

Premises used: Iff.mpr, Nat.cast_pos, pos_of_ne_zero, Ideal.absNorm_ne_zero_of_nonZeroDivisors
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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))
rw : ∃ (x : ClassGroup (𝓞 K)), ∀ (y : ClassGroup (𝓞 K)), y = x
⊢ IsPrincipalIdealRing.{u_1} (𝓞 K)

Tactic:
rw [← classNumber_eq_one_iff, classNumber, Fintype.card_eq_one_iff]

Premises used: NumberField.classNumber_eq_one_iff, NumberField.classNumber, Fintype.card_eq_one_iff
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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

Tactic:
⟨1, fun C ↦ ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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))
refine : ∀ (C : ClassGroup (𝓞 K)), C = 1
⊢ ∃ (x : ClassGroup (𝓞 K)), ∀ (y : ClassGroup (𝓞 K)), y = x

Tactic:
refine ⟨1, fun C ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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)
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))
⊢ C = 1

Tactic:
obtain ⟨I, rfl, hI⟩ := exists_ideal_in_class_of_norm_le C

Premises used: NumberField.exists_ideal_in_class_of_norm_le, rfl
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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))
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:
simpa [← ClassGroup.mk0_eq_one_iff] using h hI

Premises used: ClassGroup.mk0_eq_one_iff
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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)

Tactic:
isPrincipalIdealRing_of_isPrincipal_of_norm_le (fun I hI ↦ ?_)

Premises used: RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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))
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))
⊢ IsPrincipalIdealRing.{u_1} (𝓞 K)

Tactic:
refine isPrincipalIdealRing_of_isPrincipal_of_norm_le (fun I hI ↦ ?_)

Premises used: RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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) : ℝ)|)
rw :
  Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K))
    (UniqueFactorizationMonoid.normalizedFactors (↑I : Ideal (𝓞 K))).prod
⊢ Submodule.IsPrincipal (↑I : Ideal (𝓞 K))

Tactic:
rw [← mem_isPrincipalSubmonoid_iff,
    ← Ideal.prod_normalizedFactors_eq_self (nonZeroDivisors.coe_ne_zero I)]

Premises used: nonZeroDivisors.coe_ne_zero, Ideal.prod_normalizedFactors_eq_self, Ideal.mem_isPrincipalSubmonoid_iff
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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

Tactic:
Submonoid.multiset_prod_mem _ _ (fun J hJ ↦ mem_isPrincipalSubmonoid_iff.mp ?_)

Premises used: Set.Mem, Submonoid.multiset_prod_mem, Iff.mp, Ideal.mem_isPrincipalSubmonoid_iff
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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) : ℝ)|)
refine :
  ∀ (J : Ideal (𝓞 K)) (hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors (↑I : Ideal (𝓞 K))),
    Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K)) J
⊢ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K))
    (UniqueFactorizationMonoid.normalizedFactors (↑I : Ideal (𝓞 K))).prod

Tactic:
refine Submonoid.multiset_prod_mem _ _ (fun J hJ ↦ mem_isPrincipalSubmonoid_iff.mp ?_)

Premises used: Submonoid.multiset_prod_mem
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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
neg : ∀ (hJ0 : ¬J = 0), Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K)) J
⊢ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K)) J

Tactic:
by_cases hJ0 : J = 0
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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

Tactic:
simpa [hJ0] using bot_isPrincipal

Premises used: bot_isPrincipal
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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
neg :
  Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K))
    (↑(Subtype.mk (p := Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰) J ⋯) : Ideal (𝓞 K))
⊢ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K)) J

Tactic:
rw [← Subtype.coe_mk J (mem_nonZeroDivisors_of_ne_zero hJ0)]

Premises used: Subtype.coe_mk, mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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))
    (↑(Subtype.mk (p := Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰) J ⋯) : Ideal (𝓞 K))

Tactic:
h (((mem_normalizedFactors_iff (nonZeroDivisors.coe_ne_zero I)).mp hJ).1) ?_

Premises used: Set.Mem, setOf, Ideal.mem_normalizedFactors_iff, And.left, nonZeroDivisors.coe_ne_zero, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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
neg :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
          (↑(Subtype.mk (p := Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰) J ⋯) : Ideal (𝓞 K))) :
      ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
⊢ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K))
    (↑(Subtype.mk (p := Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰) J ⋯) : Ideal (𝓞 K))

Tactic:
refine h (((mem_normalizedFactors_iff (nonZeroDivisors.coe_ne_zero I)).mp hJ).1) ?_
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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
⊢ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
          (↑(Subtype.mk (p := Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰) J ⋯) : Ideal (𝓞 K))) :
      ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)

Tactic:
(cast_le.mpr <| le_of_dvd (absNorm_pos_of_nonZeroDivisors I) <|
    absNorm_dvd_absNorm_of_le <| le_of_dvd <|
      UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors hJ).trans hI

Premises used: Iff.mpr, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, Ideal.le_of_dvd, Ideal.absNorm_dvd_absNorm_of_le, Ideal.absNorm_pos_of_nonZeroDivisors, Nat.cast_le, LE.le.trans, Nat.le_of_dvd