-- Mathlib/NumberTheory/NumberField/ClassNumber.lean
theorem _root_.RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt
    (h : |discr K| < (2 * (π / 4) ^ nrComplexPlaces K *
      ((finrank ℚ K) ^ (finrank ℚ K) / (finrank ℚ K).factorial)) ^ 2) :
    IsPrincipalIdealRing (𝓞 K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
C : ClassGroup (𝓞 K)
⊢ C = 1

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

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI :
  ↑(Ideal.absNorm ↑I) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
⊢ ClassGroup.mk0 I = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI :
  ↑(Ideal.absNorm ↑I) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
⊢ Ideal.absNorm ↑I < Nat.succ 1

Tactic:
exact Nat.cast_lt.mp <| lt_of_le_of_lt hI h

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : √↑|discr K| < 2 * ((π / 4) ^ nrComplexPlaces K * (↑(finrank ℚ K) ^ finrank ℚ K / ↑(finrank ℚ K).factorial))
this : 0 < finrank ℚ K
⊢ 0 < (π / 4) ^ nrComplexPlaces K * (↑(finrank ℚ K) ^ finrank ℚ K / ↑(finrank ℚ K).factorial)

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this✝ : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI :
  ↑(Ideal.absNorm ↑I) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
this : Ideal.absNorm ↑I = 1
⊢ Submodule.IsPrincipal ⊤

Tactic:
exact top_isPrincipal

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this✝ : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI :
  ↑(Ideal.absNorm ↑I) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
this : Ideal.absNorm ↑I = 1
⊢ ClassGroup.mk0 I = 1

Tactic:
rw [ClassGroup.mk0_eq_one_iff, Ideal.absNorm_eq_one_iff.mp this]

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this✝ : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI :
  ↑(Ideal.absNorm ↑I) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
this : Ideal.absNorm ↑I = 1
⊢ Submodule.IsPrincipal ⊤

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
⊢ ∃ x, ∀ (y : ClassGroup (𝓞 K)), y = x

Tactic:
refine ⟨1, fun C ↦ ?_⟩

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
C : ClassGroup (𝓞 K)
⊢ C = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI :
  ↑(Ideal.absNorm ↑I) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
⊢ Ideal.absNorm ↑I = 1

Tactic:
refine le_antisymm (Nat.lt_succ.mp ?_) (Nat.one_le_iff_ne_zero.mpr
  (Ideal.absNorm_ne_zero_of_nonZeroDivisors I))

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI :
  ↑(Ideal.absNorm ↑I) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
⊢ Ideal.absNorm ↑I < Nat.succ 1

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI :
  ↑(Ideal.absNorm ↑I) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
⊢ ClassGroup.mk0 I = 1

Tactic:
have : Ideal.absNorm I.1 = 1 := by
  refine le_antisymm (Nat.lt_succ.mp ?_) (Nat.one_le_iff_ne_zero.mpr
    (Ideal.absNorm_ne_zero_of_nonZeroDivisors I))
  exact Nat.cast_lt.mp <| lt_of_le_of_lt hI h

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this✝ : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI :
  ↑(Ideal.absNorm ↑I) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
this : Ideal.absNorm ↑I = 1
⊢ ClassGroup.mk0 I = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : ↑|discr K| < (2 * (π / 4) ^ nrComplexPlaces K * (↑(finrank ℚ K) ^ finrank ℚ K / ↑(finrank ℚ K).factorial)) ^ 2
this : 0 < finrank ℚ K
⊢ 0 ≤ 2 * (π / 4) ^ nrComplexPlaces K * (↑(finrank ℚ K) ^ finrank ℚ K / ↑(finrank ℚ K).factorial)

Tactic:
positivity

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : ↑|discr K| < (2 * (π / 4) ^ nrComplexPlaces K * (↑(finrank ℚ K) ^ finrank ℚ K / ↑(finrank ℚ K).factorial)) ^ 2
this : 0 < finrank ℚ K
⊢ 0 ≤ ↑|discr K|

Tactic:
positivity

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
⊢ IsPrincipalIdealRing (𝓞 K)

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

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
⊢ ∃ x, ∀ (y : ClassGroup (𝓞 K)), y = x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : ↑|discr K| < (2 * (π / 4) ^ nrComplexPlaces K * (↑(finrank ℚ K) ^ finrank ℚ K / ↑(finrank ℚ K).factorial)) ^ 2
⊢ IsPrincipalIdealRing (𝓞 K)

Tactic:
have : 0 < finrank ℚ K := finrank_pos

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : ↑|discr K| < (2 * (π / 4) ^ nrComplexPlaces K * (↑(finrank ℚ K) ^ finrank ℚ K / ↑(finrank ℚ K).factorial)) ^ 2
this : 0 < finrank ℚ K
⊢ IsPrincipalIdealRing (𝓞 K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : ↑|discr K| < (2 * (π / 4) ^ nrComplexPlaces K * (↑(finrank ℚ K) ^ finrank ℚ K / ↑(finrank ℚ K).factorial)) ^ 2
this : 0 < finrank ℚ K
⊢ IsPrincipalIdealRing (𝓞 K)

Tactic:
rw [← Real.sqrt_lt (by positivity) (by positivity), mul_assoc, ← inv_mul_lt_iff₀' (by positivity),
  mul_inv, ← inv_pow, inv_div, inv_div, mul_assoc, Int.cast_abs] at h

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
⊢ IsPrincipalIdealRing (𝓞 K)