-- Mathlib/NumberTheory/Cyclotomic/PID.lean
theorem five_pid [IsCyclotomicExtension {5} ℚ K] : IsPrincipalIdealRing (𝓞 K)

Proof state:
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ 0 < ↑5

Tactic:
norm_num

Result:
no goals

Proof state:
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ 0 < 125

Tactic:
norm_num

Result:
no goals

Proof state:
case h
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ ↑|discr K| <
    (2 * (π / 4) ^ nrComplexPlaces K * (↑(Module.finrank ℚ K) ^ Module.finrank ℚ K / ↑(Module.finrank ℚ K)!)) ^ 2

Tactic:
rw [absdiscr_prime 5 K, IsCyclotomicExtension.finrank (n := 5) K
  (irreducible_rat (by norm_num)), nrComplexPlaces_eq_totient_div_two 5, totient_prime
    PNat.prime_five]

Result:
case h
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ ↑|(-1) ^ ((↑5 - 1) / 2) * ↑↑5 ^ (↑5 - 2)| < (2 * (π / 4) ^ ((↑5 - 1) / 2) * (↑(↑5 - 1) ^ (↑5 - 1) / ↑(↑5 - 1)!)) ^ 2

Proof state:
case h
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ ↑|(-1) ^ ((↑5 - 1) / 2) * ↑↑5 ^ (↑5 - 2)| < (2 * (π / 4) ^ ((↑5 - 1) / 2) * (↑(↑5 - 1) ^ (↑5 - 1) / ↑(↑5 - 1)!)) ^ 2

Tactic:
simp only [Int.reduceNeg, PNat.val_ofNat, succ_sub_succ_eq_sub, tsub_zero, reduceDiv, even_two,
  Even.neg_pow, one_pow, cast_ofNat, Int.reducePow, one_mul, Int.cast_abs, Int.cast_ofNat,
  div_pow, gt_iff_lt, show 4! = 24 by rfl, abs_of_pos (show (0 : ℝ) < 125 by norm_num)]

Result:
case h
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ 125 < (2 * (π ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2

Proof state:
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ 4! = 24

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ IsPrincipalIdealRing (𝓞 K)

Tactic:
apply RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt

Result:
case h
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ ↑|discr K| <
    (2 * (π / 4) ^ nrComplexPlaces K * (↑(Module.finrank ℚ K) ^ Module.finrank ℚ K / ↑(Module.finrank ℚ K)!)) ^ 2

Proof state:
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
this : (2 * (3 ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 < (2 * (π ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2
⊢ 125 < (2 * (3 ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2

Tactic:
norm_num

Result:
no goals

Proof state:
case h
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ (2 * (3 ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 < (2 * (π ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2

Tactic:
gcongr

Result:
case h.hab.bc.bc.h.hab
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ 3 < π

Proof state:
case h.hab.bc.bc.h.hab
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ 3 < π

Tactic:
exact pi_gt_three

Result:
no goals

Proof state:
case h
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ 125 < (2 * (π ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2

Tactic:
suffices (2 * (3 ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 < (2 * (π ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 from
  lt_trans (by norm_num) this

Result:
case h
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
⊢ (2 * (3 ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 < (2 * (π ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2