-- Module: Mathlib.RingTheory.FractionalIdeal.Norm
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : IsDomain K
ι : Type u_3
inst_10 : Fintype ι
inst_11 : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
bI : Basis.{u_3, 0, u_2} ι ℤ ↥(↑I : Submodule R K)
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b
bI.num : Basis.{u_3, 0, u_1} ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
rw :
  |Matrix.det.{0, u_3} (n := ι)
        (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
    |(HMul.hMul (α := Matrix ι ι ℚ) (β := Matrix ι ι ℚ)
            (((Algebra.leftMulMatrix b₀ : AlgHom.{0, u_2, u_3} ℚ K (Matrix ι ι ℚ)) : (a : K) → Matrix ι ι ℚ)
                ((algebraMap R K : (a : R) → K) (↑I.den : R)) :
              Matrix ι ι ℚ)
            (b₀.toMatrix
              (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
                (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))).det| /
      |(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)|
rw₁ :
  |Matrix.det.{0, u_3} (n := ι)
        (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
    |Matrix.det.{0, u_3} (n := ι)
            (((Algebra.leftMulMatrix b₀ : AlgHom.{0, u_2, u_3} ℚ K (Matrix ι ι ℚ)) : (a : K) → Matrix ι ι ℚ)
              ((algebraMap R K : (a : R) → K) (↑I.den : R))) *
          Matrix.det
            (b₀.toMatrix
              (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
                (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| /
      |(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)|
rw₂ :
  |Matrix.det.{0, u_3} (n := ι)
        (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
    |Matrix.det.{0, u_3} (n := ι)
            (((Algebra.leftMulMatrix b₀ : AlgHom.{0, u_2, u_3} ℚ K (Matrix ι ι ℚ)) : (a : K) → Matrix ι ι ℚ)
              ((algebraMap R K : (a : R) → K) (↑I.den : R)))| *
        |Matrix.det
            (b₀.toMatrix
              (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
                (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| /
      |(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)|
rw₃ :
  |Matrix.det.{0, u_3} (n := ι)
        (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
    HMul.hMul (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑I.den : R) : K)| : ℚ)
        |Matrix.det
            (b₀.toMatrix
              (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
                (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| /
      |(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)|
rw₄ :
  |Matrix.det.{0, u_3} (n := ι)
        (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
    HMul.hMul (α := ℚ) (|(algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ)| : ℚ)
        |Matrix.det
            (b₀.toMatrix
              (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
                (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| /
      |(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)|
rw₅ :
  |Matrix.det.{0, u_3} (n := ι)
        (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
    HDiv.hDiv (β := ℚ)
      (HMul.hMul (α := ℚ) (|(algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ)| : ℚ)
        |Matrix.det
            (b₀.toMatrix
              (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
                (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))|)
      (|(algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ)| : ℚ)
rw₆ :
  |Matrix.det.{0, u_3} (n := ι)
        (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
    HMul.hMul (α := ℚ) (|(algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ)| : ℚ)
      (HDiv.hDiv (β := ℚ)
        |Matrix.det
            (b₀.toMatrix
              (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
                (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))|
        (|(algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ)| : ℚ))
rw₇ rw₈ :
  |Matrix.det.{0, u_3} (n := ι)
        (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
    |Matrix.det
        (b₀.toMatrix
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))|
⊢ |Matrix.det.{0, u_3} (n := ι)
        (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
    |(b₀.toMatrix
            (HSMul.hSMul (α := K) (β := ι → K) ((algebraMap R K : (a : R) → K) (↑I.den : R) : K)
              (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
                (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))).det| /
      |(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)|

Tactic:
rw [Basis.toMatrix_smul, Matrix.det_mul, abs_mul, ← Algebra.norm_eq_matrix_det,
    Algebra.norm_localization ℤ ℤ⁰, show (Algebra.norm ℤ (den I : R) : ℚ) =
    algebraMap ℤ ℚ (Algebra.norm ℤ (den I : R)) by rfl, mul_div_assoc, mul_div_cancel₀ _ (by
    rw [ne_eq, abs_eq_zero, IsFractionRing.to_map_eq_zero_iff, Algebra.norm_eq_zero_iff_of_basis b]
    exact nonZeroDivisors.coe_ne_zero _)]

Premises used: Algebra.norm_eq_matrix_det, Module.Basis.toMatrix_smul, mul_div_assoc, Algebra.norm_localization, abs_mul, nonZeroDivisors, Int, mul_div_cancel₀, Matrix.det_mul