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
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  Basis.indexEquiv (canonicalEmbedding.latticeBasis K) (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Equiv.trans (indexEquiv K) f.symm
M : Matrix (index K) (index K) ℝ :=
  Basis.toMatrix (mixedEmbedding.stdBasis K) (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ
    (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
      (⇑f.symm : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))
    RingHom.equivRatAlgHom
this :
  M.map (⇑ofRealHom : (a : ℝ) → ℂ) =
    HMul.hMul (α := Matrix (index K) (index K) ℂ) (matrixToStdBasis K)
      ((reindex (Equiv.symm (indexEquiv K)) (Equiv.symm (indexEquiv K)) :
            (a : Matrix (K →+* ℂ) (K →+* ℂ) ℂ) → Matrix (index K) (index K) ℂ)
          N)ᵀ
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞)
have calc : ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
    (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) =
  (↑‖det (n := index K)
          (Basis.toMatrix (mixedEmbedding.stdBasis K)
            (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))‖₊ :
    ℝ≥0∞)
Tactic: calc volume (fundamentalDomain (latticeBasis K))
      _ = ‖((mixedEmbedding.stdBasis K).toMatrix ((latticeBasis K).reindex e.symm)).det‖₊ := by
        rw [← fundamentalDomain_reindex _ e.symm, ← norm_toNNReal, measure_fundamentalDomain
          ((latticeBasis K).reindex e.symm), volume_fundamentalDomain_stdBasis, mul_one]
        rfl
      _ = ‖(matrixToStdBasis K).det * N.det‖₊ := by
        rw [← nnnorm_real, ← ofRealHom_eq_coe, RingHom.map_det, RingHom.mapMatrix_apply, this,
          det_mul, det_transpose, det_reindex_self]
      _ = (2 : ℝ≥0∞)⁻¹ ^ Fintype.card {w : InfinitePlace K // IsComplex w} * sqrt ‖N.det ^ 2‖₊ := by
        have : ‖Complex.I‖₊ = 1 := by rw [← norm_toNNReal, norm_I, Real.toNNReal_one]
        rw [det_matrixToStdBasis, nnnorm_mul, nnnorm_pow, nnnorm_mul, this, mul_one, nnnorm_inv,
          coe_mul, ENNReal.coe_pow, ← norm_toNNReal, RCLike.norm_two, Real.toNNReal_ofNat,
          coe_inv two_ne_zero, coe_ofNat, nnnorm_pow, NNReal.sqrt_sq]
      _ = (2 : ℝ≥0∞)⁻¹ ^ Fintype.card { w // IsComplex w } * NNReal.sqrt ‖discr K‖₊ := by
        rw [← Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, Algebra.discr_reindex,
          ← coe_discr, map_intCast, ← Complex.nnnorm_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  Basis.indexEquiv (canonicalEmbedding.latticeBasis K) (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Equiv.trans (indexEquiv K) f.symm
M : Matrix (index K) (index K) ℝ :=
  Basis.toMatrix (mixedEmbedding.stdBasis K) (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ
    (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
      (⇑f.symm : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))
    RingHom.equivRatAlgHom
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞)
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (K := ℝ) (latticeBasis K)) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞)
have suffices : M.map (⇑ofRealHom : (a : ℝ) → ℂ) =
  HMul.hMul (α := Matrix (index K) (index K) ℂ) (matrixToStdBasis K)
    ((reindex (Equiv.symm (indexEquiv K)) (Equiv.symm (indexEquiv K)) :
          (a : Matrix (K →+* ℂ) (K →+* ℂ) ℂ) → Matrix (index K) (index K) ℂ)
        N)ᵀ
Tactic: suffices M.map ofRealHom = matrixToStdBasis K *
      (Matrix.reindex (indexEquiv K).symm (indexEquiv K).symm N).transpose by
    calc volume (fundamentalDomain (latticeBasis K))
      _ = ‖((mixedEmbedding.stdBasis K).toMatrix ((latticeBasis K).reindex e.symm)).det‖₊ := by
        rw [← fundamentalDomain_reindex _ e.symm, ← norm_toNNReal, measure_fundamentalDomain
          ((latticeBasis K).reindex e.symm), volume_fundamentalDomain_stdBasis, mul_one]
        rfl
      _ = ‖(matrixToStdBasis K).det * N.det‖₊ := by
        rw [← nnnorm_real, ← ofRealHom_eq_coe, RingHom.map_det, RingHom.mapMatrix_apply, this,
          det_mul, det_transpose, det_reindex_self]
      _ = (2 : ℝ≥0∞)⁻¹ ^ Fintype.card {w : InfinitePlace K // IsComplex w} * sqrt ‖N.det ^ 2‖₊ := by
        have : ‖Complex.I‖₊ = 1 := by rw [← norm_toNNReal, norm_I, Real.toNNReal_one]
        rw [det_matrixToStdBasis, nnnorm_mul, nnnorm_pow, nnnorm_mul, this, mul_one, nnnorm_inv,
          coe_mul, ENNReal.coe_pow, ← norm_toNNReal, RCLike.norm_two, Real.toNNReal_ofNat,
          coe_inv two_ne_zero, coe_ofNat, nnnorm_pow, NNReal.sqrt_sq]
      _ = (2 : ℝ≥0∞)⁻¹ ^ Fintype.card { w // IsComplex w } * NNReal.sqrt ‖discr K‖₊ := by
        rw [← Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, Algebra.discr_reindex,
          ← coe_discr, map_intCast, ← Complex.nnnorm_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  Basis.indexEquiv (canonicalEmbedding.latticeBasis K) (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Equiv.trans (indexEquiv K) f.symm
M : Matrix (index K) (index K) ℝ :=
  Basis.toMatrix (mixedEmbedding.stdBasis K) (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ
    (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
      (⇑f.symm : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))
    RingHom.equivRatAlgHom
⊢ M.map (⇑ofRealHom : (a : ℝ) → ℂ) =
    HMul.hMul (α := Matrix (index K) (index K) ℂ) (matrixToStdBasis K)
      ((reindex (Equiv.symm (indexEquiv K)) (Equiv.symm (indexEquiv K)) :
            (a : Matrix (K →+* ℂ) (K →+* ℂ) ℂ) → Matrix (index K) (index K) ℂ)
          N)ᵀ
have a : ∀ (i j : index K),
  M.map (⇑ofRealHom : (a : ℝ) → ℂ) i j =
    HMul.hMul (α := Matrix (index K) (index K) ℂ) (β := Matrix (index K) (index K) ℂ) (matrixToStdBasis K)
      ((reindex (Equiv.symm (indexEquiv K)) (Equiv.symm (indexEquiv K)) :
            (a : Matrix (K →+* ℂ) (K →+* ℂ) ℂ) → Matrix (index K) (index K) ℂ)
          N)ᵀ
      i j
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  Basis.indexEquiv (canonicalEmbedding.latticeBasis K) (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Equiv.trans (indexEquiv K) f.symm
M : Matrix (index K) (index K) ℝ :=
  Basis.toMatrix (mixedEmbedding.stdBasis K) (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ
    (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
      (⇑f.symm : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))
    RingHom.equivRatAlgHom
i j : index K
⊢ Matrix.map
      (Basis.toMatrix (mixedEmbedding.stdBasis K)
        (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))
      (⇑ofRealHom : (a : ℝ) → ℂ) i j =
    HMul.hMul (α := Matrix (index K) (index K) ℂ) (β := Matrix (index K) (index K) ℂ) (matrixToStdBasis K)
      ((reindex (Equiv.symm (indexEquiv K)) (Equiv.symm (indexEquiv K)) :
            (a : Matrix (K →+* ℂ) (K →+* ℂ) ℂ) → Matrix (index K) (index K) ℂ)
          N)ᵀ
      i j
have a : (matrixToStdBasis K *ᵥ
      Function.comp (β := K →+* ℂ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
          (((integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
              ((e : (a : index K) → Free.ChooseBasisIndex ℤ (𝓞 K)) j : Free.ChooseBasisIndex ℤ (𝓞 K)) :
            K))
        (⇑(indexEquiv K) : (a : index K) → K →+* ℂ))
    i =
  HMul.hMul (α := Matrix (index K) (index K) ℂ) (β := Matrix (index K) (index K) ℂ) (matrixToStdBasis K)
    ((reindex (Equiv.symm (indexEquiv K)) (Equiv.symm (indexEquiv K)) :
          (a : Matrix (K →+* ℂ) (K →+* ℂ) ℂ) → Matrix (index K) (index K) ℂ)
        N)ᵀ
    i j
Tactic: rw [Matrix.map_apply, Basis.toMatrix_apply, Basis.coe_reindex, Function.comp_apply,
    Equiv.symm_symm, latticeBasis_apply, ← commMap_canonical_eq_mixed, Complex.ofRealHom_eq_coe,
    stdBasis_repr_eq_matrixToStdBasis_mul K _ (fun _ => rfl)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ ZLattice.covolume.{u_1} (E := mixedSpace K) (mixedEmbedding.integerLattice K) (volume : Measure (mixedSpace 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 ℤ (𝓞 K)) (K := ℝ) (latticeBasis 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) : ℝ)|
⊢ ZLattice.covolume.{u_1} (E := mixedSpace K) (mixedEmbedding.integerLattice K) (volume : Measure (mixedSpace K)) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
have 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) : ℝ)|
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) : ℝ)|
⊢ 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 (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞)).toReal =
  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) : ℝ)|
⊢ 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 (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K)).toReal * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
  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) : ℝ)|
⊢ ZLattice.covolume.{u_1} (E := mixedSpace K) (mixedEmbedding.integerLattice K) (volume : Measure (mixedSpace K)) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
have rw₄ : ENNReal.toReal 2⁻¹ ^ nrComplexPlaces K * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
  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) : ℝ)|
⊢ ZLattice.covolume.{u_1} (E := mixedSpace K) (mixedEmbedding.integerLattice K) (volume : Measure (mixedSpace K)) =
    HPow.hPow (α := ℝ) 2⁻¹ (nrComplexPlaces K) * √|(↑(discr K) : ℝ)|
have rw₅ : (ENNReal.toReal 2)⁻¹ ^ nrComplexPlaces K * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
  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) : ℝ)|
⊢ 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) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞).toReal =
  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) : ℝ)|
⊢ 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) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖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]