-- 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
⊢ (LinearMap.det f).natAbs = absNorm I

Tactic:
have ha : ∀ i, f (b' i) = a i • b' i := by
  intro i; rw [f_apply, b'.equiv_apply, Equiv.refl_apply, ab_eq]

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

Tactic:
by_cases hI : I = ⊥

Result:
case pos
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

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

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

Tactic:
nontriviality S

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

Proof state:
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)

Tactic:
haveI : ∀ i, NeZero (a i).natAbs := fun i =>
  ⟨Int.natAbs_ne_zero.mpr (Ideal.smithCoeffs_ne_zero b I hI i)⟩

Result:
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 ι
this : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), NeZero (a i).natAbs
⊢ ∏ i : Module.Free.ChooseBasisIndex ℤ S, (a i).natAbs = Nat.card (S ⧸ I)