awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞)).toReal ^ HDiv.hDiv (α := ℝ) 1 (↑(finrank ℚ K) : ℝ)
h_le : minkowskiBound K I ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
x : K
⊢ (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            HPow.hPow (α := ℝ) 4 (nrComplexPlaces K) *
          √|(↑(discr K) : ℝ)| *
        (↑(finrank ℚ K).factorial : ℝ) *
      (1 / π ^ nrComplexPlaces K) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
          (HPow.hPow (α := ℝ) 4 (nrComplexPlaces K) / π ^ nrComplexPlaces K) *
        (↑(finrank ℚ K).factorial : ℝ) *
      √|(↑(discr K) : ℝ)|

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
obtain :
  ∀ (w : K) (h_mem : Membership.mem (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K) w)
    (h_nz : w ≠ 0)
    (h_nm :
      (↑|(Algebra.norm ℚ : (a : K) → ℚ) w| : ℝ) ≤
        (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑1 : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
                (4 / π) ^ nrComplexPlaces K *
              (↑(finrank ℚ K).factorial : ℝ) /
            HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
          √|(↑(discr K) : ℝ)|),
    ∃ (a : 𝓞 K),
      a ≠ 0 ∧
        (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤
          (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
              HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
            √|(↑(discr K) : ℝ)|
⊢ ∃ (a : 𝓞 K),
    a ≠ 0 ∧
      (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
            HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
          √|(↑(discr K) : ℝ)|

Tactic:
obtain ⟨_, h_mem, h_nz, h_nm⟩ := exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr K ↑1

Premises used: NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : K
h_mem : Membership.mem (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K) w
h_nz : w ≠ 0
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) w| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑1 : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
obtain :
  ∀ (a : 𝓞 K)
    (h_mem :
      Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))
    (h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K))
    (h_nm :
      (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
        (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑1 : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
                (4 / π) ^ nrComplexPlaces K *
              (↑(finrank ℚ K).factorial : ℝ) /
            HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
          √|(↑(discr K) : ℝ)|),
    ∃ (a : 𝓞 K),
      a ≠ 0 ∧
        (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤
          (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
              HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
            √|(↑(discr K) : ℝ)|
⊢ ∃ (a : 𝓞 K),
    a ≠ 0 ∧
      (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
            HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
          √|(↑(discr K) : ℝ)|

Tactic:
obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem

Premises used: FractionalIdeal.mem_one_iff, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : 𝓞 K
h_mem :
  Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑1 : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ ∃ (a : 𝓞 K),
    a ≠ 0 ∧
      (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
            HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
          √|(↑(discr K) : ℝ)|

Tactic:
⟨a, ne_zero_of_map h_nz, ?_⟩

Premises used: ne_zero_of_map, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : 𝓞 K
h_mem :
  Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑1 : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
refine :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ ∃ (a : 𝓞 K),
    a ≠ 0 ∧
      (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
            HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
          √|(↑(discr K) : ℝ)|

Tactic:
refine ⟨a, ne_zero_of_map h_nz, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : 𝓞 K
h_mem :
  Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑1 : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|

Tactic:
simp_rw [Units.val_one, FractionalIdeal.absNorm_one, Rat.cast_one, one_mul] at h_nm

Premises used: Units.val_one, one_mul, Rat.cast_one, FractionalIdeal.absNorm_one
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : 𝓞 K
h_mem :
  Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|

Tactic:
h_nm
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : 𝓞 K
h_mem :
  Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|

Tactic:
exact h_nm
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
obtain :
  ∀ (x : 𝓞 K) (h_nz : x ≠ 0)
    (h_bd :
      (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
            HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
          √|(↑(discr K) : ℝ)|),
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
        ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
      (↑|discr K| : ℝ)
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)

Tactic:
obtain ⟨x, h_nz, h_bd⟩ := exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr K

Premises used: NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_bd :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
rw : LE.le (α := ℤ) (1 : ℤ) (|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x| : ℤ)
⊢ LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ)

Tactic:
rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le]

Premises used: Int.cast_abs, Rat.cast_intCast, Int.cast_le, Algebra.coe_norm_int, Int.cast_one
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_bd :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ LE.le (α := ℤ) (1 : ℤ) (|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x| : ℤ)

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

Premises used: Iff.mpr, Int.one_le_abs, Algebra.norm_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_bd :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ LE.le (α := ℤ) (1 : ℤ) (|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x| : ℤ)

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

Premises used: Iff.mpr, Int.one_le_abs, Algebra.norm_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_bd :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : 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)
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_bd :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
h_nm : LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ)
⊢ 1 ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|

Tactic:
replace h_bd := le_trans h_nm h_bd
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ)
h_bd :
  HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) /
      ((4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ)) ≤
    √|(↑(discr K) : ℝ)|
⊢ 0 ≤
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) /
      ((4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ))

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ)
h_bd :
  HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) /
      ((4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ)) ≤
    √|(↑(discr K) : ℝ)|
⊢ LE.le (α := ℝ) 0 |(↑(discr K) : ℝ)|

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ)
h_bd :
  1 ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
rwa :
  0 <
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K)
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)

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

Premises used: Int.cast_abs, Real.le_sqrt, pow_mul, inv_mul_le_iff₀, div_pow, mul_comm, inv_div, mul_one, OfNat.ofNat, mul_pow
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ)
h_bd :
  1 ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ 0 < (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ)
h_bd :
  1 ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ 0 <
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K)

Tactic:
exact div_pos (by positivity) <| pow_pos (Nat.cast_pos.mpr finrank_pos) (finrank ℚ K)

Premises used: pow_pos, Rat, div_pos, Module.finrank
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)

Tactic:
have := abs_discr_ge' K
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
this :
  HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
          ((4 / π) ^ finrank ℚ K * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
        (↑|discr K| : ℝ)),
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
        ((4 / π) ^ finrank ℚ K * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
      (↑|discr K| : ℝ)
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ finrank ℚ K * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)

Tactic:
rwa [← IsTotallyComplex.finrank] at this

Premises used: NumberField.IsTotallyComplex.finrank
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
⊢ LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)

Tactic:
have h : 0 < (finrank ℚ K : ℝ) := Nat.cast_pos.mpr finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
h : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)
⊢ 0 ≤
    HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K) : ℝ) 2 /
      (4 / π * HPow.hPow (α := ℝ) (↑(finrank ℚ K).factorial : ℝ) (HMul.hMul (α := ℝ) 2 (↑(finrank ℚ K) : ℝ)⁻¹))

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
h : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)
⊢ 0 ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑|discr K| : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
h : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)
⊢ 0 ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K) : ℝ) 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
h : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)
⊢ 0 ≤ 4 / π * HPow.hPow (α := ℝ) (↑(finrank ℚ K).factorial : ℝ) (HMul.hMul (α := ℝ) 2 (↑(finrank ℚ K) : ℝ)⁻¹)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
h : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)
⊢ LE.le (α := ℝ) 0 (↑|discr K| : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
h : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)
⊢ 0 ≤ 4 / π

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
h : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑(finrank ℚ K).factorial : ℝ) (HMul.hMul (α := ℝ) 2 (↑(finrank ℚ K) : ℝ)⁻¹)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
h : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)
⊢ LE.le (α := ℝ) 0 (↑(finrank ℚ K).factorial : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
h : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)
rw :
  HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ finrank ℚ K * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K) : ℝ) 2 /
      (4 / π * HPow.hPow (α := ℝ) (↑(finrank ℚ K).factorial : ℝ) (HMul.hMul (α := ℝ) 2 (↑(finrank ℚ K) : ℝ)⁻¹)) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑|discr K| : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹

Tactic:
rw [← Real.rpow_le_rpow_iff (z := finrank ℚ K) (by positivity) (by positivity) h, Real.div_rpow
    (by positivity) (by positivity), ← Real.rpow_mul (by positivity), inv_mul_cancel₀ h.ne',
    Real.rpow_one, Real.mul_rpow (by positivity) (by positivity), Real.rpow_natCast,
    Real.rpow_natCast, ← pow_mul, ← Real.rpow_mul (by positivity),
    inv_mul_cancel_right₀ h.ne', Real.rpow_two]

Premises used: Real.mul_rpow, Real.div_rpow, pow_mul, Real.rpow_one, LT.lt.ne', Real.rpow_two, Real.rpow_le_rpow_iff, Real.rpow_mul, inv_mul_cancel₀, Real.rpow_natCast, inv_mul_cancel_right₀
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
h : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ finrank ℚ K * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)

Tactic:
abs_discr_ge_of_isTotallyComplex K

Premises used: NumberField.abs_discr_ge_of_isTotallyComplex
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
h : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ finrank ℚ K * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)

Tactic:
exact abs_discr_ge_of_isTotallyComplex K

Premises used: NumberField.abs_discr_ge_of_isTotallyComplex
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ (↑|discr K| : ℝ)

Tactic:
le_trans ?_ (abs_discr_ge' K)

Premises used: NumberField.abs_discr_ge', le_trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
refine :
  4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2)
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ (↑|discr K| : ℝ)

Tactic:
refine le_trans ?_ (abs_discr_ge' K)

Premises used: NumberField.abs_discr_ge', le_trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
rw :
  4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K * 2) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2)
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2)

Tactic:
rw [mul_comm 2 _]

Premises used: mul_comm, OfNat.ofNat