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
this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
inl : ∀ (h : 0 < discr K), (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
inr : ∀ (h : 0 = discr K), (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
have inr₁ : ∀ (h : discr K < 0), (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
Tactic: obtain h | h | h := Int.lt_trichotomy 0 (discr K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
h : 0 < discr K
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
have inl : 1 = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
Tactic: rw [Int.sign_eq_one_of_pos h, Even.neg_one_pow (this.mp <| Int.cast_nonneg 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
this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
h : 0 < discr K
inl : 1 = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
have inl₁ : Eq (α := ℤ) 1 1
Tactic: rw [Int.sign_eq_one_of_pos h, Even.neg_one_pow (this.mp <| Int.cast_nonneg 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
this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
h : discr K < 0
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
have inr : Odd (nrComplexPlaces K)
Tactic: rw [Int.sign_eq_neg_one_of_neg h, Odd.neg_one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
h : discr K < 0
⊢ Odd (nrComplexPlaces K)
have inr : ¬Even (nrComplexPlaces K)
Tactic: rwa [← Nat.not_even_iff_odd, ← this, Int.cast_nonneg_iff, not_le]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
h : discr K < 0
inr : ¬Even (nrComplexPlaces K)
⊢ Odd (nrComplexPlaces K)
have inr₁ : ¬LE.le (α := ℂ) 0 (↑(discr K) : ℂ)
Tactic: rwa [← Nat.not_even_iff_odd, ← this, Int.cast_nonneg_iff, not_le]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
h : discr K < 0
inr : ¬Even (nrComplexPlaces K)
inr₁ : ¬LE.le (α := ℂ) 0 (↑(discr K) : ℂ)
⊢ Odd (nrComplexPlaces K)
have inr₂ : ¬0 ≤ discr K
Tactic: rwa [← Nat.not_even_iff_odd, ← this, Int.cast_nonneg_iff, not_le]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
have have : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
have : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
have have₁ : ∀ (this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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)
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
have inl : ∀ (this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)) (h : 0 < discr 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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)
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
have inr : ∀ (this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)) (h : 0 = discr 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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)
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
have inr₁ : ∀ (this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)) (h : discr K < 0),
  (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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ rootDiscr K = HPow.hPow (α := ℝ) (β := ℝ) (↑|discr K| : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹
have rw : HPow.hPow (α := ℝ) (β := ℝ) (↑|discr K| : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹ =
  HPow.hPow (α := ℝ) (β := ℝ) (↑|discr K| : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹
Tactic: rw [rootDiscr]
-- 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)) =
    (↑‖det (n := index K)
            (Basis.toMatrix (mixedEmbedding.stdBasis K)
              (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))‖₊ :
      ℝ≥0∞)
have 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∞)
Tactic: rw [← fundamentalDomain_reindex _ e.symm, ← norm_toNNReal, measure_fundamentalDomain
          ((latticeBasis K).reindex e.symm), volume_fundamentalDomain_stdBasis, 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
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)
            (Basis.toMatrix (mixedEmbedding.stdBasis K)
              (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))‖₊ :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
have rw : (↑‖(↑(det (n := index K)
              (Basis.toMatrix (mixedEmbedding.stdBasis K)
                (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))) :
          ℂ)‖₊ :
    ℝ≥0∞) =
  (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
Tactic: rw [← nnnorm_real, ← ofRealHom_eq_coe, RingHom.map_det, RingHom.mapMatrix_apply, this,
          det_mul, det_transpose, det_reindex_self]
-- 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 :
  (↑‖(↑(det (n := index K)
                (Basis.toMatrix (mixedEmbedding.stdBasis K)
                  (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))) :
            ℂ)‖₊ :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
⊢ (↑‖det (n := index K)
            (Basis.toMatrix (mixedEmbedding.stdBasis K)
              (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))‖₊ :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
have rw₁ : (↑(nnnorm (E := ℂ)
        ((ofRealHom : (a : ℝ) → ℂ)
            (det (n := index K)
              (Basis.toMatrix (mixedEmbedding.stdBasis K)
                (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))) :
          ℂ)) :
    ℝ≥0∞) =
  (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
Tactic: rw [← nnnorm_real, ← ofRealHom_eq_coe, RingHom.map_det, RingHom.mapMatrix_apply, this,
          det_mul, det_transpose, det_reindex_self]
-- 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 :
  (↑‖(↑(det (n := index K)
                (Basis.toMatrix (mixedEmbedding.stdBasis K)
                  (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))) :
            ℂ)‖₊ :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
rw₁ :
  (↑(nnnorm (E := ℂ)
          ((ofRealHom : (a : ℝ) → ℂ)
              (det (n := index K)
                (Basis.toMatrix (mixedEmbedding.stdBasis K)
                  (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))) :
            ℂ)) :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
⊢ (↑‖det (n := index K)
            (Basis.toMatrix (mixedEmbedding.stdBasis K)
              (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))‖₊ :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
have rw₂ : (↑(nnnorm (E := ℂ)
        (det.{0, u_1} (n := index K)
          ((ofRealHom.mapMatrix : (a : Matrix (index K) (index K) ℝ) → Matrix (index K) (index K) ℂ)
            (Basis.toMatrix (mixedEmbedding.stdBasis K)
              (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))))) :
    ℝ≥0∞) =
  (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
Tactic: rw [← nnnorm_real, ← ofRealHom_eq_coe, RingHom.map_det, RingHom.mapMatrix_apply, this,
          det_mul, det_transpose, det_reindex_self]
-- 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 :
  (↑‖(↑(det (n := index K)
                (Basis.toMatrix (mixedEmbedding.stdBasis K)
                  (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))) :
            ℂ)‖₊ :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
rw₁ :
  (↑(nnnorm (E := ℂ)
          ((ofRealHom : (a : ℝ) → ℂ)
              (det (n := index K)
                (Basis.toMatrix (mixedEmbedding.stdBasis K)
                  (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))) :
            ℂ)) :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
rw₂ :
  (↑(nnnorm (E := ℂ)
          (det.{0, u_1} (n := index K)
            ((ofRealHom.mapMatrix : (a : Matrix (index K) (index K) ℝ) → Matrix (index K) (index K) ℂ)
              (Basis.toMatrix (mixedEmbedding.stdBasis K)
                (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))))) :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
⊢ (↑‖det (n := index K)
            (Basis.toMatrix (mixedEmbedding.stdBasis K)
              (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))‖₊ :
      ℝ≥0∞) =
    (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
have rw₃ : (↑(nnnorm (E := ℂ)
        (det (n := index K)
          (Matrix.map
            (Basis.toMatrix (mixedEmbedding.stdBasis K)
              (⇑(Basis.reindex (latticeBasis K) e.symm) : (a : index K) → mixedSpace K))
            (⇑ofRealHom : (a : ℝ) → ℂ)))) :
    ℝ≥0∞) =
  (↑‖det (n := index K) (matrixToStdBasis K) * N.det‖₊ : ℝ≥0∞)
Tactic: rw [← nnnorm_real, ← ofRealHom_eq_coe, RingHom.map_det, RingHom.mapMatrix_apply, this,
          det_mul, det_transpose, det_reindex_self]
-- 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)ᵀ
⊢ ‖I‖₊ = 1
have rw : ‖I‖.toNNReal = 1
Tactic: rw [← norm_toNNReal, norm_I, Real.toNNReal_one]