-- Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
theorem minkowskiBound_lt_boundOfDiscBdd : minkowskiBound K ↑1 < boundOfDiscBdd N

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K ≤ 1 * ↑(sqrt ↑N) * 2 ^ rankOfDiscrBdd N

Tactic:
gcongr

Result:
case h₁.h₁
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 2⁻¹ ^ nrComplexPlaces K ≤ 1

case h₁.h₂.a.hab
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ ‖discr K‖₊ ≤ ↑N

case h₂.ha
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 1 ≤ 2

case h₂.hmn
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 2⁻¹ ≤ 1

Tactic:
norm_num

Result:
no goals

Proof state:
case h₁.h₁
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 2⁻¹ ^ nrComplexPlaces K ≤ 1

Tactic:
exact pow_le_one₀ (by positivity) (by norm_num)

Result:
no goals

Proof state:
case h₂.ha
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 1 ≤ 2

Tactic:
exact one_le_two

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
⊢ minkowskiBound K 1 < ↑(boundOfDiscBdd N)

Tactic:
have : boundOfDiscBdd N - 1 < boundOfDiscBdd N := by
  simp_rw [boundOfDiscBdd, add_tsub_cancel_right, lt_add_iff_pos_right, zero_lt_one]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ minkowskiBound K 1 < ↑(boundOfDiscBdd N)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 0 ≤ 2⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ minkowskiBound K 1 < ↑(boundOfDiscBdd N)

Tactic:
refine lt_of_le_of_lt ?_ (coe_lt_coe.mpr this)

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ minkowskiBound K 1 ≤ ↑(boundOfDiscBdd N - 1)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ minkowskiBound K 1 ≤ ↑(boundOfDiscBdd N - 1)

Tactic:
rw [minkowskiBound, volume_fundamentalDomain_fractionalIdealLatticeBasis, boundOfDiscBdd,
  add_tsub_cancel_right, Units.val_one, FractionalIdeal.absNorm_one, Rat.cast_one,
  ENNReal.ofReal_one, one_mul, mixedEmbedding.finrank, volume_fundamentalDomain_latticeBasis,
  coe_mul, ENNReal.coe_pow, coe_ofNat, show sqrt N = (1 : ℝ≥0∞) * sqrt N by rw [one_mul]]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K ≤ 1 * ↑(sqrt ↑N) * 2 ^ rankOfDiscrBdd N

Proof state:
case h₁.h₂.a.hab
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ ‖discr K‖₊ ≤ ↑N

Tactic:
rwa [← NNReal.coe_le_coe, coe_nnnorm, Int.norm_eq_abs, ← Int.cast_abs,
  NNReal.coe_natCast, ← Int.cast_natCast, Int.cast_le]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
⊢ boundOfDiscBdd N - 1 < boundOfDiscBdd N

Tactic:
simp_rw [boundOfDiscBdd, add_tsub_cancel_right, lt_add_iff_pos_right, zero_lt_one]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ ↑(sqrt ↑N) = 1 * ↑(sqrt ↑N)

Tactic:
rw [one_mul]

Result:
no goals

Proof state:
case h₂.hmn
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
exact rank_le_rankOfDiscrBdd hK

Result:
no goals