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
have : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
have₁ :
  ∀ (this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)),
    (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
have₂ : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
have₃ have₄ :
  ∀ (this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)),
    (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
inl :
  ∀ (this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)) (h : 0 < discr K),
    (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
inr :
  ∀ (this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)) (h : 0 = discr K),
    (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
inr₁ :
  ∀ (this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)) (h : discr K < 0),
    (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
inr₂ :
  ∀ (this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)) (h : 0 = discr K),
    (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
inr₃ inr₄ :
  ∀ (this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)) (h : discr K < 0),
    (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)

Tactic:
classical
  have : 0 ≤ (discr K : ℂ) ↔ Even (nrComplexPlaces K) := by
    rw [discr_eq_basisMatrix_det_sq, Complex.sq_nonneg_iff, ← conj_eq_iff_im, RingHom.map_det,
      RingHom.mapMatrix_apply, conj_basisMatrix, reindex_apply, Equiv.refl_symm, Equiv.coe_refl,
      Function.Involutive.toPerm_symm, det_permute', mul_eq_right₀,
      ComplexEmbedding.conjugate_sign]
    · simp only [Units.val_pow_eq_pow_val, Units.val_neg, Units.val_one, Int.reduceNeg,
        Int.cast_pow, Int.cast_neg, Int.cast_one]
      rw [neg_one_pow_eq_one_iff_even (by norm_num)]
    · exact det_of_basisMatrix_non_zero K
  obtain h | h | h := Int.lt_trichotomy 0 (discr K)
  · rw [Int.sign_eq_one_of_pos h, Even.neg_one_pow (this.mp <| Int.cast_nonneg h.le)]
  · grind [discr_ne_zero]
  · rw [Int.sign_eq_neg_one_of_neg h, Odd.neg_one_pow]
    rwa [← Nat.not_even_iff_odd, ← this, Int.cast_nonneg_iff, not_le]

Premises used: not_le, Int.cast_nonneg_iff, Nat.not_even_iff_odd, Int.lt_trichotomy, NumberField.discr, OfNat.ofNat, NumberField.discr_ne_zero, Odd.neg_one_pow
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw rw₁ :
  HPow.hPow (α := ℝ) (β := ℝ) (↑|discr K| : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹ =
    HPow.hPow (α := ℝ) (β := ℝ) (↑|discr K| : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹
⊢ rootDiscr K = HPow.hPow (α := ℝ) (β := ℝ) (↑|discr K| : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹

Tactic:
rw [rootDiscr]

Premises used: NumberField.rootDiscr
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
⊢ rootDiscr ℚ = 1

Tactic:
simp [rootDiscr_def]

Premises used: NumberField.rootDiscr_def
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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)ᵀ
rw :
  ENNReal.ofReal
      |(Basis.det (mixedEmbedding.stdBasis K) : (a : index K → mixedSpace K) → ℝ)
          (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K)| =
    (↑‖det (n := index K)
              (Basis.toMatrix (mixedEmbedding.stdBasis K)
                (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))‖.toNNReal :
      ℝ≥0∞)
⊢ ((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:
rw [← fundamentalDomain_reindex _ e.symm, ← norm_toNNReal, measure_fundamentalDomain
          ((latticeBasis K).reindex e.symm), volume_fundamentalDomain_stdBasis, mul_one]

Premises used: NumberField.mixedEmbedding.latticeBasis, ZSpan.measure_fundamentalDomain, ZSpan.fundamentalDomain_reindex, Module.Basis.reindex, mul_one, Equiv.symm, norm_toNNReal, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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)ᵀ
⊢ ENNReal.ofReal
      |(Basis.det (mixedEmbedding.stdBasis K) : (a : index K → mixedSpace K) → ℝ)
          (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K)| =
    (↑‖det (n := index K)
              (Basis.toMatrix (mixedEmbedding.stdBasis K)
                (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))‖.toNNReal :
      ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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)ᵀ
rw : ‖I‖.toNNReal = 1
rw₁ : Real.toNNReal 1 = 1
rw₂ rw₃ : Eq (α := ℝ≥0) 1 1
⊢ ‖I‖₊ = 1

Tactic:
rw [← norm_toNNReal, norm_I, Real.toNNReal_one]

Premises used: Real.toNNReal_one, Complex.norm_I, norm_toNNReal
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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)ᵀ
⊢ ‖I‖₊ = 1

Tactic:
have : ‖Complex.I‖₊ = 1 := by rw [← norm_toNNReal, norm_I, Real.toNNReal_one]
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
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)ᵀ
⊢ ((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∞)

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]
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
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
⊢ 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:
ext : 2
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
a :
  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
⊢ 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:
dsimp only [M]
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
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
⊢ 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

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)]

Premises used: Matrix.map_apply, Equiv.symm_symm, Module.Basis.coe_reindex, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, Module.Basis.toMatrix_apply, NumberField.mixedEmbedding.latticeBasis_apply, Complex.ofRealHom_eq_coe, Function.comp_apply, NumberField.mixedEmbedding.commMap_canonical_eq_mixed
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
⊢ (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:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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) : ℝ)|
rw₁₀ 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) : ℝ)|

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]

Premises used: NumberField.mixedEmbedding.fundamentalDomain_integerLattice, ENNReal.coe_toReal, ENNReal.toReal_inv, Int.norm_eq_abs, ENNReal.toReal_pow, ZLattice.covolume_eq_measure_fundamentalDomain, ENNReal.toReal_mul, coe_nnnorm, ENNReal.toReal_ofNat, MeasureTheory.measureReal_def, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, 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) : ℝ)
⊢ minkowskiBound K I ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)

Tactic:
le_of_eq ?_

Premises used: le_of_eq
-- 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) : ℝ)
refine : minkowskiBound K I = ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
⊢ minkowskiBound K I ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)

Tactic:
refine le_of_eq ?_

Premises used: le_of_eq
-- 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) : ℝ)
⊢ 0 ≤ B

Tactic:
positivity