-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem natAbs_det_equiv (I : Ideal S) {E : Type*} [EquivLike E S I] [AddEquivClass E S I] (e : E) :
    Int.natAbs
        (LinearMap.det
          ((Submodule.subtype I).restrictScalars ℤ ∘ₗ AddMonoidHom.toIntLinearMap (e : S →+ I))) =
      Ideal.absNorm I

Proof state:
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S ↥I
inst✝ : AddEquivClass E S ↥I
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI
ab_eq : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑((selfBasis b I hI) i) = smithCoeffs b I hI i • (ringBasis b I hI) i
e' : S ≃ₗ[ℤ] ↥I := b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := ↑ℤ (Submodule.subtype I) ∘ₗ ↑e'
f_apply : ∀ (x : S), f x = ↑((b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), f (b' i) = a i • b' i
⊢ (LinearMap.det f).natAbs = absNorm I

Tactic:
letI := Classical.decEq ι

Result:
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S ↥I
inst✝ : AddEquivClass E S ↥I
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝¹ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI
this✝ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI
ab_eq : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑((selfBasis b I hI) i) = smithCoeffs b I hI i • (ringBasis b I hI) i
e' : S ≃ₗ[ℤ] ↥I := b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := ↑ℤ (Submodule.subtype I) ∘ₗ ↑e'
f_apply : ∀ (x : S), f x = ↑((b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), f (b' i) = a i • b' i
this : DecidableEq ι := Classical.decEq ι
⊢ (LinearMap.det f).natAbs = absNorm I

Proof state:
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S ↥I
inst✝ : AddEquivClass E S ↥I
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI
⊢ (LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I

Tactic:
have ab_eq := I.selfBasis_def b hI

Result:
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S ↥I
inst✝ : AddEquivClass E S ↥I
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI
ab_eq : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑((selfBasis b I hI) i) = smithCoeffs b I hI i • (ringBasis b I hI) i
⊢ (LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I

Proof state:
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S ↥I
inst✝ : AddEquivClass E S ↥I
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝¹ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI
this✝ : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI
ab_eq : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑((selfBasis b I hI) i) = smithCoeffs b I hI i • (ringBasis b I hI) i
e' : S ≃ₗ[ℤ] ↥I := b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))
f : S →ₗ[ℤ] S := ↑ℤ (Submodule.subtype I) ∘ₗ ↑e'
f_apply : ∀ (x : S), f x = ↑((b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl
ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), f (b' i) = a i • b' i
this : DecidableEq ι := Classical.decEq ι
⊢ (Matrix.diagonal a).det.natAbs = (∏ i : Module.Free.ChooseBasisIndex ℤ S, a i).natAbs

Tactic:
rw [Matrix.det_diagonal]

Result:
no goals

Proof state:
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S ↥I
inst✝ : AddEquivClass E S ↥I
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
⊢ (LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I

Tactic:
let b' := I.ringBasis b hI

Result:
case neg.inr
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S ↥I
inst✝ : AddEquivClass E S ↥I
e : E
hI : ¬I = ⊥
ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
h✝ : Nonempty ι
this✝ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI
this : DecidableEq ι := Classical.decEq ι
a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI
b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI
⊢ (LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I