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

Proof state:
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ 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 {3} ℚ 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 {3} ℚ K
⊢ 0 < 3

Tactic:
norm_num

Result:
no goals

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

Tactic:
norm_num

Result:
no goals

Proof state:
case h.hab.bc.bc.h
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ 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 {3} ℚ K
⊢ ↑|(-1) ^ ((↑3 - 1) / 2) * ↑↑3 ^ (↑3 - 2)| < (2 * (π / 4) ^ ((↑3 - 1) / 2) * (↑(↑3 - 1) ^ (↑3 - 1) / ↑(↑3 - 1)!)) ^ 2

Tactic:
simp only [Int.reduceNeg, PNat.val_ofNat, succ_sub_succ_eq_sub, tsub_zero, zero_lt_two,
  Nat.div_self, pow_one, cast_ofNat, neg_mul, one_mul, abs_neg, Int.cast_abs, Int.cast_ofNat,
  factorial_two, gt_iff_lt, abs_of_pos (show (0 : ℝ) < 3 by norm_num)]

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

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

Tactic:
gcongr

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

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

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

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

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

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

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

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

Tactic:
norm_num

Result:
no goals