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
rw :
  Measure.real.{u_1} (α := mixedSpace K) (m := Prod.instMeasurableSpace) (volume : Measure (mixedSpace K))
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₁ :
  ENNReal.toReal
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K))) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₂ :
  (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞)).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₃ :
  (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K)).toReal * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₄ :
  ENNReal.toReal 2⁻¹ ^ nrComplexPlaces K * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₅ :
  (ENNReal.toReal 2)⁻¹ ^ nrComplexPlaces K * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₆ :
  HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₇ :
  HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
⊢ ZLattice.covolume.{u_1} (E := mixedSpace K) (mixedEmbedding.integerLattice K) (volume : Measure (mixedSpace K)) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
have rw₈ : HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √(↑‖discr K‖₊ : ℝ) =
  HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
Tactic: rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_integerLattice K),
    measureReal_def,
    volume_fundamentalDomain_latticeBasis, ENNReal.toReal_mul, ENNReal.toReal_pow,
    ENNReal.toReal_inv, toReal_ofNat, ENNReal.coe_toReal, Real.coe_sqrt, coe_nnnorm,
    Int.norm_eq_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Measure.real.{u_1} (α := mixedSpace K) (m := Prod.instMeasurableSpace) (volume : Measure (mixedSpace K))
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₁ :
  ENNReal.toReal
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K))) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₂ :
  (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞)).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₃ :
  (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K)).toReal * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₄ :
  ENNReal.toReal 2⁻¹ ^ nrComplexPlaces K * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₅ :
  (ENNReal.toReal 2)⁻¹ ^ nrComplexPlaces K * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₆ :
  HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₇ :
  HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₈ :
  HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √(↑‖discr K‖₊ : ℝ) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
⊢ ZLattice.covolume.{u_1} (E := mixedSpace K) (mixedEmbedding.integerLattice K) (volume : Measure (mixedSpace K)) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
have rw₉ : HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √‖discr K‖ =
  HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
Tactic: rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_integerLattice K),
    measureReal_def,
    volume_fundamentalDomain_latticeBasis, ENNReal.toReal_mul, ENNReal.toReal_pow,
    ENNReal.toReal_inv, toReal_ofNat, ENNReal.coe_toReal, Real.coe_sqrt, coe_nnnorm,
    Int.norm_eq_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Measure.real.{u_1} (α := mixedSpace K) (m := Prod.instMeasurableSpace) (volume : Measure (mixedSpace K))
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₁ :
  ENNReal.toReal
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K))) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₂ :
  (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞)).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₃ :
  (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K)).toReal * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₄ :
  ENNReal.toReal 2⁻¹ ^ nrComplexPlaces K * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₅ :
  (ENNReal.toReal 2)⁻¹ ^ nrComplexPlaces K * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₆ :
  HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₇ :
  HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₈ :
  HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √(↑‖discr K‖₊ : ℝ) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
rw₉ :
  HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √‖discr K‖ =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
⊢ ZLattice.covolume.{u_1} (E := mixedSpace K) (mixedEmbedding.integerLattice K) (volume : Measure (mixedSpace K)) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
have rw₁₀ : HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)| =
  HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
Tactic: rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_integerLattice K),
    measureReal_def,
    volume_fundamentalDomain_latticeBasis, ENNReal.toReal_mul, ENNReal.toReal_pow,
    ENNReal.toReal_inv, toReal_ofNat, ENNReal.coe_toReal, Real.coe_sqrt, coe_nnnorm,
    Int.norm_eq_abs]
-- 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)ˣ
⊢ ZLattice.covolume.{u_1} (E := mixedSpace K) (idealLattice K I) (volume : Measure (mixedSpace K)) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
have rw : Measure.real.{u_1} (α := mixedSpace K) (m := Prod.instMeasurableSpace) (volume : Measure (mixedSpace K))
    (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
      (fractionalIdealLatticeBasis K I)) =
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
    √|(↑(discr K) : ℝ)|
Tactic: rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_idealLattice K I),
    measureReal_def,
    volume_fundamentalDomain_fractionalIdealLatticeBasis, volume_fundamentalDomain_latticeBasis,
    ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_pow, ENNReal.toReal_inv, toReal_ofNat,
    ENNReal.coe_toReal, Real.coe_sqrt, coe_nnnorm, Int.norm_eq_abs,
    ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.val)), 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)ˣ
rw :
  Measure.real.{u_1} (α := mixedSpace K) (m := Prod.instMeasurableSpace) (volume : Measure (mixedSpace K))
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
        (fractionalIdealLatticeBasis K I)) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
⊢ ZLattice.covolume.{u_1} (E := mixedSpace K) (idealLattice K I) (volume : Measure (mixedSpace K)) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
have rw₁ : ENNReal.toReal
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
        (fractionalIdealLatticeBasis K I))) =
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
    √|(↑(discr K) : ℝ)|
Tactic: rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_idealLattice K I),
    measureReal_def,
    volume_fundamentalDomain_fractionalIdealLatticeBasis, volume_fundamentalDomain_latticeBasis,
    ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_pow, ENNReal.toReal_inv, toReal_ofNat,
    ENNReal.coe_toReal, Real.coe_sqrt, coe_nnnorm, Int.norm_eq_abs,
    ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.val)), 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)ˣ
rw :
  Measure.real.{u_1} (α := mixedSpace K) (m := Prod.instMeasurableSpace) (volume : Measure (mixedSpace K))
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
        (fractionalIdealLatticeBasis K I)) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
rw₁ :
  ENNReal.toReal
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K :=
          ℝ) (fractionalIdealLatticeBasis K I))) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
⊢ ZLattice.covolume.{u_1} (E := mixedSpace K) (idealLattice K I) (volume : Measure (mixedSpace K)) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
have rw₂ : (HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal
        (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ))
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
          (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
        ℝ≥0∞)).toReal =
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
    √|(↑(discr K) : ℝ)|
Tactic: rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_idealLattice K I),
    measureReal_def,
    volume_fundamentalDomain_fractionalIdealLatticeBasis, volume_fundamentalDomain_latticeBasis,
    ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_pow, ENNReal.toReal_inv, toReal_ofNat,
    ENNReal.coe_toReal, Real.coe_sqrt, coe_nnnorm, Int.norm_eq_abs,
    ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.val)), 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)ˣ
rw :
  Measure.real.{u_1} (α := mixedSpace K) (m := Prod.instMeasurableSpace) (volume : Measure (mixedSpace K))
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
        (fractionalIdealLatticeBasis K I)) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
rw₁ :
  ENNReal.toReal
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K :=
          ℝ) (fractionalIdealLatticeBasis K I))) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
rw₂ :
  (HMul.hMul (β := ℝ≥0∞)
        (ENNReal.ofReal
          (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ))
        (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
            (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) :
          ℝ≥0∞)).toReal =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
⊢ ZLattice.covolume.{u_1} (E := mixedSpace K) (idealLattice K I) (volume : Measure (mixedSpace K)) =
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
        HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
      √|(↑(discr K) : ℝ)|
have rw₃ : (ENNReal.ofReal
        (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞))).toReal =
  (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
      HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) *
    √|(↑(discr K) : ℝ)|
Tactic: rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_idealLattice K I),
    measureReal_def,
    volume_fundamentalDomain_fractionalIdealLatticeBasis, volume_fundamentalDomain_latticeBasis,
    ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_pow, ENNReal.toReal_inv, toReal_ofNat,
    ENNReal.coe_toReal, Real.coe_sqrt, coe_nnnorm, Int.norm_eq_abs,
    ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.val)), 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) : ℝ)
⊢ minkowskiBound K I ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
have refine : minkowskiBound K I = ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
Tactic: refine le_of_eq ?_
-- 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) : ℝ)
⊢ minkowskiBound K I = ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
have rw : minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞) ≠ ∞
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]
-- 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) : ℝ)
rw : minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞) ≠ ∞
⊢ minkowskiBound K I = ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
have h : Ne (α := ℝ) (↑(finrank ℚ K) : ℝ) 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (hypothesis)
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) : ℝ)
⊢ ∃ 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) : ℝ)|
have h_le : 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))
-- 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)
⊢ ∃ 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) : ℝ)|
have 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
Tactic: convert! exists_ne_zero_mem_ideal_of_norm_le K I h_le
-- 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 : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)| =
    (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
have 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)
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']
-- 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) : ℝ)| /
      HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) =
    (minkowskiBound K I * (↑(convexBodySumFactor K)⁻¹ : ℝ≥0∞)).toReal /
      HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K)
have 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
Tactic: congr 1