awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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)) : ℝ) *
          (4 / π) ^ nrComplexPlaces K *
        (↑(finrank ℚ K).factorial : ℝ) *
      √|(↑(discr K) : ℝ)| =
    (minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞)).toReal
have 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) : ℝ)|
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ (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 : ℝ))⁻¹
have 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 : ℝ))⁻¹)))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ (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 : ℝ))⁻¹)))
have 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 : ℝ))⁻¹)))
Tactic: rw [ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.1))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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) *
        ((↑((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 : ℝ))⁻¹)))
have simp_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 : ℝ))⁻¹)))
Tactic: simp_rw [NNReal.coe_inv, NNReal.coe_div, NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_div,
        coe_real_pi, NNReal.coe_ofNat, NNReal.coe_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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) *
        ((↑((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 : ℝ))⁻¹)))
⊢ (↑((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 : ℝ))⁻¹)))
have simp_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 : ℝ))⁻¹)))
Tactic: simp_rw [NNReal.coe_inv, NNReal.coe_div, NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_div,
        coe_real_pi, NNReal.coe_ofNat, NNReal.coe_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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) *
          (↑((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
have 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) : ℤ))
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
              (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
have e_a : HSub.hSub (α := ℤ) (↑(finrank ℚ K) : ℤ) (↑(nrComplexPlaces K) : ℤ) - (↑(nrRealPlaces K) : ℤ) +
    (↑(nrComplexPlaces K) : ℤ) =
  HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ HSub.hSub (α := ℤ) (↑(finrank ℚ K) : ℤ) (↑(nrComplexPlaces K) : ℤ) - (↑(nrRealPlaces K) : ℤ) +
      (↑(nrComplexPlaces K) : ℤ) =
    HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces K) : ℤ)
have e_a : (↑(nrRealPlaces K) : ℤ) + HMul.hMul (α := ℤ) 2 (↑(nrComplexPlaces 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ HPow.hPow (α := ℝ) (β := ℤ) 2 2 = 4
have norm_cast : HPow.hPow (α := ℕ) (β := ℕ) 2 2 = 4
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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 (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) : ℝ)|
have 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) : ℝ)|
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ (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) : ℝ)|
have _ : (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: calc
    _ = FractionalIdeal.absNorm I.1 * (2 : ℝ)⁻¹ ^ nrComplexPlaces K * sqrt ‖discr K‖₊ *
          (2 : ℝ) ^ finrank ℚ K * ((2 : ℝ) ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K /
            (Nat.factorial (finrank ℚ K)))⁻¹ := by
      simp_rw [minkowskiBound, convexBodySumFactor,
        volume_fundamentalDomain_fractionalIdealLatticeBasis,
        volume_fundamentalDomain_latticeBasis, toReal_mul, toReal_pow, toReal_inv, coe_toReal,
        toReal_ofNat, mixedEmbedding.finrank, mul_assoc]
      rw [ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.1))]
      simp_rw [NNReal.coe_inv, NNReal.coe_div, NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_div,
        coe_real_pi, NNReal.coe_ofNat, NNReal.coe_natCast]
    _ = FractionalIdeal.absNorm I.1 * (2 : ℝ) ^ (finrank ℚ K - nrComplexPlaces K - nrRealPlaces K +
          nrComplexPlaces K : ℤ) * Real.sqrt ‖discr K‖ * Nat.factorial (finrank ℚ K) *
            π⁻¹ ^ (nrComplexPlaces K) := by
      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)]
      ring
    _ = FractionalIdeal.absNorm I.1 * (2 : ℝ) ^ (2 * nrComplexPlaces K : ℤ) * Real.sqrt ‖discr K‖ *
          Nat.factorial (finrank ℚ K) * π⁻¹ ^ (nrComplexPlaces K) := by
      congr
      rw [← card_add_two_mul_card_eq_rank, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat]
      ring
    _ = FractionalIdeal.absNorm I.1 * (4 / π) ^ nrComplexPlaces K * (finrank ℚ K).factorial *
          Real.sqrt |discr K| := by
      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]
      ring
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField 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) : ℝ)|
have 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) : ℝ)|
Tactic: obtain ⟨_, h_mem, h_nz, h_nm⟩ := exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr K ↑1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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) : ℝ)|
⊢ ∃ (a : 𝓞 K),
    a ≠ 0 ∧
      (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
            HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
          √|(↑(discr K) : ℝ)|
have 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) : ℝ)|
Tactic: obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem
Cleared hypotheses: w, h_mem, h_nz, h_nm