-- Mathlib/RingTheory/FractionalIdeal/Norm.lean
theorem abs_det_basis_change [NoZeroDivisors K] {ι : Type*} [Fintype ι]
    [DecidableEq ι] (b : Basis ι ℤ R) (I : FractionalIdeal R⁰ K) (bI : Basis ι ℤ I) :
    |(b.localizationLocalization ℚ ℤ⁰ K).det ((↑) ∘ bI)| = absNorm I

Proof state:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Module.Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : NoZeroDivisors K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |(algebraMap ℤ ℚ) ((Algebra.norm ℤ) ↑I.den)| ≠ 0

Tactic:
rw [ne_eq, abs_eq_zero, IsFractionRing.to_map_eq_zero_iff, Algebra.norm_eq_zero_iff_of_basis b]

Result:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Module.Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : NoZeroDivisors K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ ¬↑I.den = 0

Proof state:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Module.Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : NoZeroDivisors K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| =
    |(algebraMap ℤ ℚ) (b.toMatrix (Subtype.val ∘ ⇑bI.num)).det| / |↑((Algebra.norm ℤ) ↑I.den)|

Tactic:
rw [RingHom.map_det, show RingHom.mapMatrix (algebraMap ℤ ℚ) (b.toMatrix ((↑) ∘ bI.num)) =
    b₀.toMatrix ((algebraMap R K (den I : R)) • ((↑) ∘ bI)) by
  ext : 2
  simp_rw [bI.num, RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
    ← Basis.localizationLocalization_repr_algebraMap ℚ ℤ⁰ K, Function.comp_apply,
    Basis.map_apply, LinearEquiv.restrictScalars_apply, equivNum_apply, Submonoid.smul_def,
    Algebra.smul_def]
  rfl]

Result:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Module.Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : NoZeroDivisors K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| =
    |(b₀.toMatrix ((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI)).det| / |↑((Algebra.norm ℤ) ↑I.den)|

Proof state:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Module.Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : NoZeroDivisors K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| =
    |(b₀.toMatrix ((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI)).det| / |↑((Algebra.norm ℤ) ↑I.den)|

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

Result:
no goals

Proof state:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Module.Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : NoZeroDivisors K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ ↑((Algebra.norm ℤ) ↑I.den) = (algebraMap ℤ ℚ) ((Algebra.norm ℤ) ↑I.den)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Module.Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : NoZeroDivisors K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| = absNorm I

Tactic:
rw [absNorm_eq, ← Ideal.natAbs_det_basis_change b I.num bI.num, Int.cast_natAbs, Int.cast_abs,
  Int.cast_abs, Basis.det_apply, Basis.det_apply]

Result:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Module.Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : NoZeroDivisors K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| =
    |↑(b.toMatrix (Subtype.val ∘ ⇑bI.num)).det| / |↑((Algebra.norm ℤ) ↑I.den)|