-- 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
⊢ ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ finrank ℚ K * ↑(finrank ℚ K).factorial ^ 2) ≤
    ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2)

Tactic:
gcongr

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

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

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
⊢ 3 ≤ (1 + 1 / ↑m) ^ (2 * m)

Tactic:
refine le_trans (le_of_eq (by field_simp; norm_num)) (one_add_mul_le_pow ?_ (2 * m))

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

Proof state:
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 / π)

Tactic:
rw [_root_.le_div_iff₀ (by positivity), pow_succ]

Result:
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 * (3 * π / 4)) * (4 / π) ≤ a m * (1 + 1 / ↑m) ^ (2 * m)

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
⊢ -2 ≤ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case h.e'_3
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 * (3 * π / 4)) * (4 / π) = 4 / 9 * (3 * π / 4) ^ m * 3

Tactic:
field_simp

Result:
case h.e'_3
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 * ((3 * π) ^ m * (3 * π)) * 4 * (9 * 4 ^ m) = 4 * (3 * π) ^ m * 3 * (9 * (4 ^ 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 * 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 * m) * (1 / ↑m)

Tactic:
field_simp

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

Proof state:
case h.e'_3
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 * ((3 * π) ^ m * (3 * π)) * 4 * (9 * 4 ^ m) = 4 * (3 * π) ^ m * 3 * (9 * (4 ^ m * 4) * π)

Tactic:
ring

Result:
no goals

Proof state:
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 / π)

Tactic:
simp_rw [a, add_mul, one_mul, pow_succ, Nat.factorial_succ]

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)
⊢ ↑(m + 1) ^ (m * 2) * ↑(m + 1) * ↑(m + 1) /
      ((4 / π) ^ m * (4 / π) * (↑((m + 1) * m.factorial) ^ 0 * ↑((m + 1) * m.factorial) * ↑((m + 1) * m.factorial))) =
    ↑m ^ (m * 2) / ((4 / π) ^ m * (↑m.factorial ^ 0 * ↑m.factorial * ↑m.factorial)) * (1 + 1 / ↑m) ^ (2 * m) / (4 / π)