-- Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
theorem abs_discr_ge (h : 1 < finrank ℚ K) :
    (4 / 9 : ℝ) * (3 * π / 4) ^ finrank ℚ K ≤ |discr K|

Proof state:
case h.h.hmn
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
a : ℕ → ℝ := fun n => ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
this : ∀ (n : ℕ), 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n
⊢ 2 * nrComplexPlaces K ≤ nrRealPlaces K + 2 * nrComplexPlaces K

Tactic:
exact Nat.le_add_left _ _

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤
    ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2)

Tactic:
let a : ℕ → ℝ := fun n => (n : ℝ) ^ (n * 2) / ((4 / π) ^ n * (n.factorial : ℝ) ^ 2)

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
a : ℕ → ℝ := fun n => ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤
    ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
a : ℕ → ℝ := fun n => ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n : ℕ
⊢ 4 * (3 * π) ^ 2 * (4 ^ 2 * 4) = 16 * π ^ 2 * (9 * 4 ^ 2)

Tactic:
ring

Result:
no goals

Proof state:
case h.h.ha
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
a : ℕ → ℝ := fun n => ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
this : ∀ (n : ℕ), 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n
⊢ 1 ≤ 4 / π

Tactic:
exact (one_le_div Real.pi_pos).2 Real.pi_le_four

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
a : ℕ → ℝ := fun n => ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
⊢ 3 = 1 + 2

Tactic:
norm_num

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
a : ℕ → ℝ := fun n => ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n : ℕ
⊢ 4 / 9 * (3 * π / 4) ^ 2 = a 2

Tactic:
norm_num [a, Nat.factorial_two]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
a : ℕ → ℝ := fun n => ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n : ℕ
⊢ 4 / 9 * (3 * π / 4) ^ 2 = 16 / ((4 / π) ^ 2 * 4)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd : 1 ≤ (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
⊢ 0 < (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd : 1 ≤ (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑|discr K|

Tactic:
rw [← inv_mul_le_iff₀ (by positivity), inv_div, mul_one, Real.le_sqrt (by positivity)
  (by positivity), ← Int.cast_abs, div_pow, mul_pow, ← pow_mul, ← pow_mul] at h_bd

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑|discr K|

Proof state:
case intro.intro.succ
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
a : ℕ → ℝ := fun n => ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
⊢ -2 ≤ 1 / ↑m

Tactic:
exact le_trans (by norm_num : (-2 : ℝ) ≤ 0) (by positivity)

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
a : ℕ → ℝ := fun n => ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ 0 ≤ a m

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑|discr K|

Tactic:
refine le_trans ?_ h_bd

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤
    ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2)

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_bd :
  ↑|(Algebra.norm ℚ) ↑x| ≤
    (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑|discr K|

Tactic:
replace h_bd := le_trans h_nm h_bd

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd : 1 ≤ (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑|discr K|