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) : ℝ)
rw : minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞) ≠ ∞
h : Ne (α := ℝ) (↑(finrank ℚ K) : ℝ) 0
⊢ minkowskiBound K I = ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)

Tactic:
rw [convexBodySum_volume, ← ENNReal.ofReal_pow (by positivity), ← Real.rpow_natCast,
      ← Real.rpow_mul toReal_nonneg, div_mul_cancel₀, Real.rpow_one, ofReal_toReal, mul_comm,
      mul_assoc, ← coe_mul, inv_mul_cancel₀ (convexBodySumFactor_ne_zero K), ENNReal.coe_one,
      mul_one]

Premises used: div_mul_cancel₀, mul_assoc, ENNReal.ofReal_toReal, ENNReal.toReal_nonneg, ENNReal.coe_one, Real.rpow_one, NumberField.mixedEmbedding.convexBodySumFactor_ne_zero, ENNReal.coe_mul, mul_comm, mul_one, Real.rpow_mul, NumberField.mixedEmbedding.convexBodySum_volume, inv_mul_cancel₀, ENNReal.ofReal_pow, Real.rpow_natCast
-- 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) : ℝ)
⊢ minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞) ≠ ∞

Tactic:
mul_ne_top (ne_of_lt (minkowskiBound_lt_top K I)) coe_ne_top

Premises used: ENNReal.mul_ne_top, NumberField.mixedEmbedding.minkowskiBound_lt_top, ne_of_lt, ENNReal.coe_ne_top
-- 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) : ℝ)
⊢ minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞) ≠ ∞

Tactic:
exact mul_ne_top (ne_of_lt (minkowskiBound_lt_top K I)) coe_ne_top

Premises used: ENNReal.mul_ne_top, NumberField.mixedEmbedding.minkowskiBound_lt_top, ne_of_lt, ENNReal.coe_ne_top
-- 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) : ℝ)
⊢ Ne (α := ℝ) (↑(finrank ℚ K) : ℝ) 0

Tactic:
(Nat.cast_ne_zero.mpr (ne_of_gt finrank_pos))

Premises used: Iff.mpr, ne_of_gt, Module.finrank_pos, Nat.cast_ne_zero
-- 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) : ℝ)
⊢ Ne (α := ℝ) (↑(finrank ℚ K) : ℝ) 0

Tactic:
exact (Nat.cast_ne_zero.mpr (ne_of_gt finrank_pos))

Premises used: Iff.mpr, ne_of_gt, Module.finrank_pos, Nat.cast_ne_zero
-- 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) : ℝ)
⊢ minkowskiBound K I ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)

Tactic:
have h_le : (minkowskiBound K I) ≤ volume (convexBodySum K B) := by
    refine le_of_eq ?_
    rw [convexBodySum_volume, ← ENNReal.ofReal_pow (by positivity), ← Real.rpow_natCast,
      ← Real.rpow_mul toReal_nonneg, div_mul_cancel₀, Real.rpow_one, ofReal_toReal, mul_comm,
      mul_assoc, ← coe_mul, inv_mul_cancel₀ (convexBodySumFactor_ne_zero K), ENNReal.coe_one,
      mul_one]
    · exact mul_ne_top (ne_of_lt (minkowskiBound_lt_top K I)) coe_ne_top
    · exact (Nat.cast_ne_zero.mpr (ne_of_gt finrank_pos))
-- 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)
⊢ ∃ a ∈ (↑I : FractionalIdeal (𝓞 K)⁰ K),
    a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K

Tactic:
exists_ne_zero_mem_ideal_of_norm_le K I h_le

Premises used: NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le
-- 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)
h :
  ∀ (x : K),
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
              (4 / π) ^ nrComplexPlaces K *
            (↑(finrank ℚ K).factorial : ℝ) /
          HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
        √|(↑(discr K) : ℝ)| =
      (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
⊢ ∃ a ∈ (↑I : FractionalIdeal (𝓞 K)⁰ K),
    a ≠ 0 ∧
      (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) ≤
        (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
                (4 / π) ^ nrComplexPlaces K *
              (↑(finrank ℚ K).factorial : ℝ) /
            HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
          √|(↑(discr K) : ℝ)|

Tactic:
convert! exists_ne_zero_mem_ideal_of_norm_le K I h_le

Premises used: NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le
-- 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
⊢ 0 ≤ (minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞)).toReal

Tactic:
positivity
-- 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
h :
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K).factorial : ℝ) *
        √|(↑(discr K) : ℝ)| /
      HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) =
    (minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞)).toReal /
      HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K)
⊢ (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)| =
    (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K

Tactic:
rw [div_pow B, ← Real.rpow_natCast B, ← Real.rpow_mul (by positivity), div_mul_cancel₀ _
    (Nat.cast_ne_zero.mpr <| ne_of_gt finrank_pos), Real.rpow_one, mul_comm_div, mul_div_assoc']

Premises used: div_mul_cancel₀, mul_div_assoc', Real.rpow_one, mul_comm_div, div_pow, Real.rpow_mul, Real.rpow_natCast
-- 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
h :
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
          (4 / π) ^ nrComplexPlaces K *
        (↑(finrank ℚ K).factorial : ℝ) *
      √|(↑(discr K) : ℝ)| =
    (minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞)).toReal
⊢ (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K).factorial : ℝ) *
        √|(↑(discr K) : ℝ)| /
      HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) =
    (minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞)).toReal /
      HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K)

Tactic:
congr 1
-- 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
h :
  (minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞)).toReal =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
          (4 / π) ^ nrComplexPlaces K *
        (↑(finrank ℚ K).factorial : ℝ) *
      √|(↑(discr K) : ℝ)|
⊢ (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
          (4 / π) ^ nrComplexPlaces K *
        (↑(finrank ℚ K).factorial : ℝ) *
      √|(↑(discr K) : ℝ)| =
    (minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞)).toReal

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- 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
simp_rw :
  (ENNReal.ofReal
          (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) :
            ℝ)).toReal *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (pi / 2) ^ nrComplexPlaces K /
                    (↑(finrank ℚ K).factorial : ℝ≥0))⁻¹ :
              ℝ)))) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K / (↑(finrank ℚ K).factorial : ℝ))⁻¹)))
⊢ (minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞)).toReal =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
          (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
        HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
      (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K / (↑(finrank ℚ K).factorial : ℝ))⁻¹

Tactic:
simp_rw [minkowskiBound, convexBodySumFactor,
        volume_fundamentalDomain_fractionalIdealLatticeBasis,
        volume_fundamentalDomain_latticeBasis, toReal_mul, toReal_pow, toReal_inv, coe_toReal,
        toReal_ofNat, mixedEmbedding.finrank, mul_assoc]

Premises used: NumberField.mixedEmbedding.minkowskiBound, ENNReal.coe_toReal, mul_assoc, ENNReal.toReal_inv, ENNReal.toReal_pow, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, ENNReal.toReal_mul, ENNReal.toReal_ofNat, NumberField.mixedEmbedding.finrank, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, NumberField.mixedEmbedding.convexBodySumFactor
-- 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
rw :
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (pi / 2) ^ nrComplexPlaces K /
                    (↑(finrank ℚ K).factorial : ℝ≥0))⁻¹ :
              ℝ)))) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K / (↑(finrank ℚ K).factorial : ℝ))⁻¹)))
⊢ (ENNReal.ofReal
          (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) :
            ℝ)).toReal *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * (pi / 2) ^ nrComplexPlaces K /
                    (↑(finrank ℚ K).factorial : ℝ≥0))⁻¹ :
              ℝ)))) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
        ((↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
          (HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
            (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K / (↑(finrank ℚ K).factorial : ℝ))⁻¹)))

Tactic:
rw [ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.1))]

Premises used: Iff.mpr, Units.val, ENNReal.toReal_ofReal, Rat.cast_nonneg, FractionalIdeal.absNorm_nonneg
-- 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
simp_rw :
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑(nrComplexPlaces K) : ℤ)) *
          √‖discr K‖ *
        HPow.hPow (α := ℝ) (β := ℤ) 2 (↑(finrank ℚ K) : ℤ) *
      ((↑(finrank ℚ K).factorial : ℝ) *
        (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑(nrRealPlaces K) : ℤ)) *
          (HPow.hPow (β := ℤ) π (-(↑(nrComplexPlaces K) : ℤ)) *
            HPow.hPow (α := ℝ) (β := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)))) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (↑(finrank ℚ K) : ℤ) *
                  HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑(nrComplexPlaces K) : ℤ)) *
                HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑(nrRealPlaces K) : ℤ)) *
              HPow.hPow (α := ℝ) (β := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)) *
          √‖discr K‖ *
        (↑(finrank ℚ K).factorial : ℝ) *
      HPow.hPow (β := ℤ) π (-(↑(nrComplexPlaces K) : ℤ))
⊢ (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
          (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) *
        HPow.hPow (α := ℝ) 2 (finrank ℚ K) *
      (HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (π / 2) ^ nrComplexPlaces K / (↑(finrank ℚ K).factorial : ℝ))⁻¹ =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            HPow.hPow (α := ℝ) 2
              (HSub.hSub (α := ℤ) (↑(finrank ℚ K) : ℤ) (↑(nrComplexPlaces K) : ℤ) - (↑(nrRealPlaces K) : ℤ) +
                (↑(nrComplexPlaces K) : ℤ)) *
          √‖discr K‖ *
        (↑(finrank ℚ K).factorial : ℝ) *
      π⁻¹ ^ nrComplexPlaces K

Tactic:
simp_rw [inv_div, div_eq_mul_inv, mul_inv, ← zpow_neg_one, ← zpow_natCast, mul_zpow,
        ← zpow_mul, neg_one_mul, mul_neg_one, neg_neg, Real.coe_sqrt, coe_nnnorm, sub_eq_add_neg,
        zpow_add₀ (two_ne_zero : (2 : ℝ) ≠ 0)]

Premises used: zpow_natCast, zpow_neg_one, mul_inv, zpow_mul, sub_eq_add_neg, neg_one_mul, neg_neg, mul_zpow, div_eq_mul_inv, two_ne_zero, zpow_add₀, coe_nnnorm, inv_div, mul_neg_one, Real.coe_sqrt
-- 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 (α := ℝ) (β := ℤ) 2 (-(↑(nrComplexPlaces K) : ℤ)) *
          √‖discr K‖ *
        HPow.hPow (α := ℝ) (β := ℤ) 2 (↑(finrank ℚ K) : ℤ) *
      ((↑(finrank ℚ K).factorial : ℝ) *
        (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑(nrRealPlaces K) : ℤ)) *
          (HPow.hPow (β := ℤ) π (-(↑(nrComplexPlaces K) : ℤ)) *
            HPow.hPow (α := ℝ) (β := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)))) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (↑(finrank ℚ K) : ℤ) *
                  HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑(nrComplexPlaces K) : ℤ)) *
                HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑(nrRealPlaces K) : ℤ)) *
              HPow.hPow (α := ℝ) (β := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)) *
          √‖discr K‖ *
        (↑(finrank ℚ K).factorial : ℝ) *
      HPow.hPow (β := ℤ) π (-(↑(nrComplexPlaces K) : ℤ))

Tactic:
ring
-- 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
e_a :
  HSub.hSub (α := ℤ) (↑(finrank ℚ K) : ℤ) (↑(nrComplexPlaces K) : ℤ) - (↑(nrRealPlaces K) : ℤ) +
      (↑(nrComplexPlaces K) : ℤ) =
    HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)
⊢ (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            HPow.hPow (α := ℝ) 2
              (HSub.hSub (α := ℤ) (↑(finrank ℚ K) : ℤ) (↑(nrComplexPlaces K) : ℤ) - (↑(nrRealPlaces K) : ℤ) +
                (↑(nrComplexPlaces K) : ℤ)) *
          √‖discr K‖ *
        (↑(finrank ℚ K).factorial : ℝ) *
      π⁻¹ ^ nrComplexPlaces K =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            HPow.hPow (α := ℝ) 2 (HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)) *
          √‖discr K‖ *
        (↑(finrank ℚ K).factorial : ℝ) *
      π⁻¹ ^ nrComplexPlaces K

Tactic:
congr
-- 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
e_a :
  (↑(nrRealPlaces K) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces K) : ℤ) - (↑(nrComplexPlaces K) : ℤ) -
        (↑(nrRealPlaces K) : ℤ) +
      (↑(nrComplexPlaces K) : ℤ) =
    HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(finrank ℚ K) : ℤ) (↑(nrComplexPlaces K) : ℤ) - (↑(nrRealPlaces K) : ℤ) +
      (↑(nrComplexPlaces K) : ℤ) =
    HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)

Tactic:
rw [← card_add_two_mul_card_eq_rank, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, Nat.cast_add, Nat.cast_mul, NumberField.InfinitePlace.card_add_two_mul_card_eq_rank
-- 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
⊢ (↑(nrRealPlaces K) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces K) : ℤ) - (↑(nrComplexPlaces K) : ℤ) -
        (↑(nrRealPlaces K) : ℤ) +
      (↑(nrComplexPlaces K) : ℤ) =
    HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)

Tactic:
ring
-- 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
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : HPow.hPow (α := ℕ) (β := ℕ) 2 2 = 4
⊢ HPow.hPow (α := ℝ) (β := ℤ) 2 2 = 4

Tactic:
norm_cast
-- 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
rw :
  (↑((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) : ℝ)|
⊢ (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            HPow.hPow (α := ℝ) 2 (HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)) *
          √‖discr K‖ *
        (↑(finrank ℚ K).factorial : ℝ) *
      π⁻¹ ^ nrComplexPlaces K =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
          (4 / π) ^ nrComplexPlaces K *
        (↑(finrank ℚ K).factorial : ℝ) *
      √|(↑(discr K) : ℝ)|

Tactic:
rw [Int.norm_eq_abs, zpow_mul, show (2 : ℝ) ^ (2 : ℤ) = 4 by norm_cast, div_pow,
        inv_eq_one_div, div_pow, one_pow, zpow_natCast]

Premises used: zpow_natCast, one_pow, zpow_mul, Int.norm_eq_abs, inv_eq_one_div, div_pow