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

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)
this : ∀ (n : ℕ), 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤
    ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2)

Tactic:
refine le_trans (this (finrank ℚ K) h) ?_

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)
this : ∀ (n : ℕ), 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n
⊢ a (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 m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a (m + 1)

Tactic:
convert_to _ ≤ (a m) * (1 + 1 / m : ℝ) ^ (2 * m) / (4 / π)

Result:
case h.e'_4
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)
⊢ a (m + 1) = a m * (1 + 1 / ↑m) ^ (2 * m) / (4 / π)

case convert_2
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)
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a m * (1 + 1 / ↑m) ^ (2 * m) / (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 : ↑(finrank ℚ K) ^ finrank ℚ K / ((4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial) ≤ √|↑(discr K)|
⊢ 0 ≤ ↑(finrank ℚ K) ^ finrank ℚ K / ((4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial)

Tactic:
positivity

Result:
no goals

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
⊢ nrComplexPlaces K * 2 ≤ finrank ℚ K

Tactic:
rw [← card_add_two_mul_card_eq_rank, mul_comm]

Result:
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

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|
a : ℕ → ℝ := fun n => ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
⊢ ∀ (n : ℕ), 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n

Tactic:
intro n hn

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)
n : ℕ
hn : 2 ≤ n
⊢ 4 / 9 * (3 * π / 4) ^ n ≤ a n

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 ≤ 3

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_bd :
  ↑|(Algebra.norm ℚ) ↑x| ≤
    (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑|discr K|

Tactic:
have h_nm : (1 : ℝ) ≤ |Algebra.norm ℚ (x : K)| := by
  rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le]
  exact Int.one_le_abs (Algebra.norm_ne_zero_iff.mpr h_nz)

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_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|

Proof state:
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)|
⊢ 1 ≤ |(Algebra.norm ℤ) x|

Tactic:
exact Int.one_le_abs (Algebra.norm_ne_zero_iff.mpr h_nz)

Result:
no goals