-- 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
this : DecidableEq ι := Classical.decEq ι
⊢ (LinearMap.det f).natAbs = absNorm I

Tactic:
calc
  Int.natAbs (LinearMap.det f) = Int.natAbs (LinearMap.toMatrix b' b' f).det := by
    rw [LinearMap.det_toMatrix]
  _ = Int.natAbs (Matrix.diagonal a).det := ?_
  _ = Int.natAbs (∏ i, a i) := by rw [Matrix.det_diagonal]
  _ = ∏ i, Int.natAbs (a i) := map_prod Int.natAbsHom a Finset.univ
  _ = Nat.card (S ⧸ I) := ?_
  _ = absNorm I := (Submodule.cardQuot_apply _).symm

Result:
case neg.inr.calc_1
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.toMatrix b' b') f).det.natAbs = (Matrix.diagonal a).det.natAbs

case neg.inr.calc_2
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 ι
⊢ ∏ i : Module.Free.ChooseBasisIndex ℤ S, (a i).natAbs = Nat.card (S ⧸ I)

Proof state:
case neg
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 = ⊥
⊢ (LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I

Tactic:
let ι := Module.Free.ChooseBasisIndex ℤ S

Result:
case neg
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
⊢ (LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I

Proof state:
case pos
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
E : Type u_2
e : E
inst✝¹ : EquivLike E S ↥⊥
inst✝ : AddEquivClass E S ↥⊥
this✝ : 1 ≠ 0
this : 1 = 0
⊢ (LinearMap.det (↑ℤ (Submodule.subtype ⊥) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm ⊥

Tactic:
contradiction

Result:
no goals

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✝ : IsEmpty ι
inst✝ : Nontrivial S
⊢ Nontrivial S

Tactic:
infer_instance

Result:
no goals