-- Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
theorem rank_le_rankOfDiscrBdd :
    finrank ℚ K ≤ rankOfDiscrBdd N

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
obtain h | h := lt_or_le 1 (finrank ℚ K)

Result:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : finrank ℚ K ≤ 1
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Proof state:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * ↑N) < ↑(finrank ℚ K)
⊢ ↑↑N ≤ 4 / 9 * (3 * π / 4) ^ Real.logb (3 * π / 4) (9 / 4 * ↑N)

Tactic:
rw [Real.rpow_logb (lt_trans zero_lt_one h₂) (ne_of_gt h₂) (by positivity), ← mul_assoc,
      ← inv_div, inv_mul_cancel₀ (by norm_num), one_mul, Int.cast_natCast]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 0 < 4

Tactic:
positivity

Result:
no goals

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : finrank ℚ K ≤ 1
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
exact le_max_of_le_left h

Result:
no goals

Proof state:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * ↑N) < ↑(finrank ℚ K)
⊢ ↑↑N < 4 / 9 * (3 * π / 4) ^ ↑(finrank ℚ K)

Tactic:
refine lt_of_le_of_lt ?_ (mul_lt_mul_of_pos_left
  (Real.rpow_lt_rpow_of_exponent_lt h₂ h) (by positivity : (0 : ℝ) < 4 / 9))

Result:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * ↑N) < ↑(finrank ℚ K)
⊢ ↑↑N ≤ 4 / 9 * (3 * π / 4) ^ Real.logb (3 * π / 4) (9 / 4 * ↑N)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
⊢ 4 / 3 < π

Tactic:
linarith [Real.pi_gt_three]

Result:
no goals

Proof state:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4) < ↑(finrank ℚ K)
⊢ ↑↑N < 4 / 9 * (3 * π / 4) ^ ↑(finrank ℚ K)

Tactic:
rw [Real.log_div_log] at h

Result:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * ↑N) < ↑(finrank ℚ K)
⊢ ↑↑N < 4 / 9 * (3 * π / 4) ^ ↑(finrank ℚ K)

Proof state:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ ↑(finrank ℚ K) ≤ Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4)

Tactic:
have h := le_trans (abs_discr_ge h) (Int.cast_le.mpr hK)

Result:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑↑N
⊢ ↑(finrank ℚ K) ≤ Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
have h_nz : N ≠ 0 := by
  refine fun h ↦ discr_ne_zero K ?_
  rwa [h, Nat.cast_zero, abs_nonpos_iff] at hK

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Proof state:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 1 ≤ 9 / 4 * ↑N

Tactic:
rw [mul_comm, ← mul_div_assoc, _root_.le_div_iff₀ (by positivity), one_mul,
  ← _root_.div_le_iff₀ (by positivity)]

Result:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 4 / 9 ≤ ↑N

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
have h₂ : 1 < 3 * π / 4 := by
  rw [_root_.lt_div_iff₀ (by positivity), ← _root_.div_lt_iff₀' (by positivity), one_mul]
  linarith [Real.pi_gt_three]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * ↑N) < ↑(finrank ℚ K)
⊢ 0 < 4 / 9

Tactic:
positivity

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 4 / 9 ≤ 1

Tactic:
norm_num

Result:
no goals

Proof state:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 0 ≤ Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4)

Tactic:
refine div_nonneg (Real.log_nonneg ?_) (Real.log_nonneg (le_of_lt h₂))

Result:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 1 ≤ 9 / 4 * ↑N

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 0 < 9

Tactic:
positivity

Result:
no goals

Proof state:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4) < ↑(finrank ℚ K)
⊢ ↑↑N < 4 / 9 * (3 * π / 4) ^ finrank ℚ K

Tactic:
rw [← Real.rpow_natCast]

Result:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4) < ↑(finrank ℚ K)
⊢ ↑↑N < 4 / 9 * (3 * π / 4) ^ ↑(finrank ℚ K)

Proof state:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 4 / 9 ≤ ↑N

Tactic:
exact le_trans (by norm_num) (Nat.one_le_cast.mpr (Nat.one_le_iff_ne_zero.mpr h_nz))

Result:
no goals

Proof state:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
apply le_max_of_le_right

Result:
case inl.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ finrank ℚ K ≤ ⌊Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4)⌋₊

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
⊢ 0 < 3

Tactic:
positivity

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * ↑N) < ↑(finrank ℚ K)
⊢ 9 / 4 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
⊢ 0 < 4

Tactic:
positivity

Result:
no goals