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)ᵀ
rw : ‖I‖.toNNReal = 1
⊢ ‖I‖₊ = 1
have rw₁ : Real.toNNReal 1 = 1
Tactic: rw [← norm_toNNReal, norm_I, Real.toNNReal_one]
-- 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)ᵀ
rw : ‖I‖.toNNReal = 1
rw₁ : Real.toNNReal 1 = 1
⊢ ‖I‖₊ = 1
have rw₂ : Eq (α := ℝ≥0) 1 1
Tactic: rw [← norm_toNNReal, norm_I, Real.toNNReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (hypothesis)
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)ᵀ
⊢ (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
have this₁ : ‖I‖₊ = 1
Tactic: have : ‖Complex.I‖₊ = 1 := by rw [← norm_toNNReal, norm_I, Real.toNNReal_one]
-- 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_1 :
  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)ᵀ
this : ‖I‖₊ = 1
⊢ (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
have rw : (↑‖(2⁻¹ * I) ^ nrComplexPlaces K * N.det‖₊ : ℝ≥0∞) =
  HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
    (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
Tactic: 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]
-- 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_1 :
  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)ᵀ
this : ‖I‖₊ = 1
rw :
  (↑‖(2⁻¹ * I) ^ nrComplexPlaces K * N.det‖₊ : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
⊢ (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
have rw₁ : (↑(‖(2⁻¹ * I) ^ nrComplexPlaces K‖₊ * ‖N.det‖₊) : ℝ≥0∞) =
  HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
    (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
Tactic: 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]
-- 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_1 :
  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)ᵀ
this : ‖I‖₊ = 1
rw :
  (↑‖(2⁻¹ * I) ^ nrComplexPlaces K * N.det‖₊ : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
rw₁ :
  (↑(‖(2⁻¹ * I) ^ nrComplexPlaces K‖₊ * ‖N.det‖₊) : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
⊢ (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
have rw₂ : (↑(‖2⁻¹ * I‖₊ ^ nrComplexPlaces K * ‖N.det‖₊) : ℝ≥0∞) =
  HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
    (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
Tactic: 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]
-- 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_1 :
  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)ᵀ
this : ‖I‖₊ = 1
rw :
  (↑‖(2⁻¹ * I) ^ nrComplexPlaces K * N.det‖₊ : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
rw₁ :
  (↑(‖(2⁻¹ * I) ^ nrComplexPlaces K‖₊ * ‖N.det‖₊) : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
rw₂ :
  (↑(‖2⁻¹ * I‖₊ ^ nrComplexPlaces K * ‖N.det‖₊) : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
⊢ (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
have rw₃ : (↑((nnnorm (E := ℂ) 2⁻¹ * ‖I‖₊) ^ nrComplexPlaces K * ‖N.det‖₊) : ℝ≥0∞) =
  HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
    (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
Tactic: 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]
-- 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_1 :
  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)ᵀ
this : ‖I‖₊ = 1
rw :
  (↑‖(2⁻¹ * I) ^ nrComplexPlaces K * N.det‖₊ : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
rw₁ :
  (↑(‖(2⁻¹ * I) ^ nrComplexPlaces K‖₊ * ‖N.det‖₊) : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
rw₂ :
  (↑(‖2⁻¹ * I‖₊ ^ nrComplexPlaces K * ‖N.det‖₊) : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
rw₃ :
  (↑((nnnorm (E := ℂ) 2⁻¹ * ‖I‖₊) ^ nrComplexPlaces K * ‖N.det‖₊) : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
⊢ (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
have rw₄ : (↑((nnnorm (E := ℂ) 2⁻¹ * 1) ^ nrComplexPlaces K * ‖N.det‖₊) : ℝ≥0∞) =
  HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
    (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
Tactic: 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]
-- 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_1 :
  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)ᵀ
this : ‖I‖₊ = 1
rw :
  (↑‖(2⁻¹ * I) ^ nrComplexPlaces K * N.det‖₊ : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
rw₁ :
  (↑(‖(2⁻¹ * I) ^ nrComplexPlaces K‖₊ * ‖N.det‖₊) : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
rw₂ :
  (↑(‖2⁻¹ * I‖₊ ^ nrComplexPlaces K * ‖N.det‖₊) : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
rw₃ :
  (↑((nnnorm (E := ℂ) 2⁻¹ * ‖I‖₊) ^ nrComplexPlaces K * ‖N.det‖₊) : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
rw₄ :
  (↑((nnnorm (E := ℂ) 2⁻¹ * 1) ^ nrComplexPlaces K * ‖N.det‖₊) : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
⊢ (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
have rw₅ : (↑(nnnorm (E := ℂ) 2⁻¹ ^ nrComplexPlaces K * ‖N.det‖₊) : ℝ≥0∞) =
  HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
    (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞)
Tactic: 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]
-- 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)ᵀ
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞)
have rw : HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
    (↑((sqrt : (a : ℝ≥0) → ℝ≥0)
          (nnnorm (E := ℂ)
            ((algebraMap ℚ ℂ : (a : ℚ) → ℂ)
                (Algebra.discr (ι := K →+* ℂ) ℚ (B := K)
                  (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
                    (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
                      (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
                    (⇑f.symm : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))) :
              ℂ))) :
      ℝ≥0∞) =
  HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
    (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞)
Tactic: 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
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 :
  HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0)
            (nnnorm (E := ℂ)
              ((algebraMap ℚ ℂ : (a : ℚ) → ℂ)
                  (Algebra.discr (ι := K →+* ℂ) ℚ (B := K)
                    (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
                      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
                        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
                      (⇑f.symm : (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))) :
                ℂ))) :
        ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞)
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖HPow.hPow (β := ℕ) N.det 2‖₊) : ℝ≥0∞) =
    HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
      (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞)
have rw₁ : HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
    (↑((sqrt : (a : ℝ≥0) → ℝ≥0)
          (nnnorm (E := ℂ)
            ((algebraMap ℚ ℂ : (a : ℚ) → ℂ)
                (Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
                  (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
                    (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
              ℂ))) :
      ℝ≥0∞) =
  HPow.hPow (α := ℝ≥0∞) 2⁻¹ (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) *
    (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞)
Tactic: rw [← Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, Algebra.discr_reindex,
          ← coe_discr, map_intCast, ← Complex.nnnorm_intCast]