-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
rw : (↑(↑(discr K) : ℚ) : ℂ) = HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
rw₁ :
  (↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      ℂ) =
    HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
rw₂ :
  (↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      ℂ) =
    HPow.hPow (β := ℕ)
      (det (n := K →+* ℂ)
        (Algebra.embeddingsMatrixReindex ℚ ℂ
          (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
            (⇑(equivReindex K : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K)) :
              (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))
          RingHom.equivRatAlgHom))
      2
rw₃ :
  Eq (α := ℂ)
    ((↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
            (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
        ℂ) :
      ℂ)
    ((algebraMap ℚ ℂ : (a : ℚ) → ℂ)
        (Algebra.discr (ι := K →+* ℂ) ℚ (B := K)
          (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
            (⇑(equivReindex K : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K)) :
              (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))) :
      ℂ)
rw₄ :
  Eq (α := ℂ)
    ((↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
            (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
        ℂ) :
      ℂ)
    ((algebraMap ℚ ℂ : (a : ℚ) → ℂ)
        (Algebra.discr (ι := K →+* ℂ) ℚ (B := K)
          (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
            (⇑(Equiv.symm (Equiv.symm (equivReindex K)) : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K)) :
              (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))) :
      ℂ)
rw₅ :
  Eq (α := ℂ)
    ((↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
            (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
        ℂ) :
      ℂ)
    ((algebraMap ℚ ℂ : (a : ℚ) → ℂ)
        (Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      ℂ)
rw₆ rw₇ :
  Eq (α := ℂ)
    (↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      ℂ)
    (↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      ℂ)
⊢ (↑(discr K) : ℂ) = HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2

Tactic:
rw [← Rat.cast_intCast, coe_discr, basisMatrix_eq_embeddingsMatrixReindex,
    ← Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, ← (equivReindex K).symm_symm,
    Algebra.discr_reindex, eq_ratCast]

Premises used: NumberField.basisMatrix_eq_embeddingsMatrixReindex, Rat.cast_intCast, Equiv.symm_symm, Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, eq_ratCast, NumberField.coe_discr, NumberField.equivReindex, Algebra.discr_reindex