awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
I : Ideal S
hI : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) I)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
hJ : Ne (α := Ideal ℤ) (comap (F := ℤ →+* S) (algebraMap ℤ S) I) ⊤
IJ : LE.le (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) (comap (F := ℤ →+* S) (algebraMap ℤ S) I)
apply : Ne (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) ⊥
⊢ Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) (comap (F := ℤ →+* S) (algebraMap ℤ S) I)

Tactic:
apply (this.isMaximal _).eq_of_le

Premises used: Ideal.IsPrime.isMaximal, Ideal.IsMaximal.eq_of_le
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
I : Ideal S
hI : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) I)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
⊢ Ne (α := Ideal ℤ) (comap (F := ℤ →+* S) (algebraMap ℤ S) I) ⊤

Tactic:
((isPrime_of_irreducible_absNorm
      ((Nat.irreducible_iff_nat_prime _).mpr hI)).comap (algebraMap ℤ S)).ne_top

Premises used: Algebra.algebraMap, Ideal.IsPrime.comap, Int, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
I : Ideal S
hI : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) I)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
⊢ Ne (α := Ideal ℤ) (comap (F := ℤ →+* S) (algebraMap ℤ S) I) ⊤

Tactic:
exact ((isPrime_of_irreducible_absNorm
      ((Nat.irreducible_iff_nat_prime _).mpr hI)).comap (algebraMap ℤ S)).ne_top

Premises used: Algebra.algebraMap, Ideal.IsPrime.comap, Int, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
I : Ideal S
hI : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) I)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
IJ : (↑((absNorm : (a : Ideal S) → ℕ) I) : S) ∈ I
⊢ LE.le (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) (comap (F := ℤ →+* S) (algebraMap ℤ S) I)

Tactic:
rw [span_singleton_le_iff_mem, mem_comap, algebraMap_int_eq, map_natCast]

Premises used: Ideal.span_singleton_le_iff_mem, map_natCast, algebraMap_int_eq, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
I : Ideal S
hI : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) I)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
⊢ (↑((absNorm : (a : Ideal S) → ℕ) I) : S) ∈ I

Tactic:
absNorm_mem I

Premises used: Set.Mem, Ideal.absNorm_mem
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
I : Ideal S
hI : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) I)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
⊢ (↑((absNorm : (a : Ideal S) → ℕ) I) : S) ∈ I

Tactic:
exact absNorm_mem I

Premises used: Ideal.absNorm_mem
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
I : Ideal S
hI : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) I)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
rw : ¬Eq (α := ℤ) (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ) 0
⊢ Ne (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) ⊥

Tactic:
rw [Ne, span_singleton_eq_bot]

Premises used: Ideal.span_singleton_eq_bot, Ne
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
I : Ideal S
hI : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) I)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
⊢ ¬Eq (α := ℤ) (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ) 0

Tactic:
Int.ofNat_ne_zero.mpr hI.ne_zero

Premises used: Iff.mpr, Int.ofNat_ne_zero, Nat.Prime.ne_zero
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
I : Ideal S
hI : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) I)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
⊢ ¬Eq (α := ℤ) (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ) 0

Tactic:
exact Int.ofNat_ne_zero.mpr hI.ne_zero

Premises used: Iff.mpr, Int.ofNat_ne_zero, Nat.Prime.ne_zero
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst_5 : EquivLike E S ↥I
inst_6 : AddEquivClass E S ↥I
e : E
pos :
  ∀ (hI : I = ⊥),
    Int.natAbs
        ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
          ((↑ℤ :
                {S M M₂ : Type u_1} →
                  [inst : Semiring ℤ] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module ℤ M] →
                            [inst_11 : Module ℤ M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
              (Submodule.subtype I) ∘ₗ
            AddMonoidHom.toIntLinearMap (↑e : S →+ ↥I))) =
      (absNorm : (a : Ideal S) → ℕ) I
neg :
  ∀ (hI : ¬I = ⊥),
    Int.natAbs
        ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
          ((↑ℤ :
                {S M M₂ : Type u_1} →
                  [inst : Semiring ℤ] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module ℤ M] →
                            [inst_11 : Module ℤ M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
              (Submodule.subtype I) ∘ₗ
            AddMonoidHom.toIntLinearMap (↑e : S →+ ↥I))) =
      (absNorm : (a : Ideal S) → ℕ) I
⊢ Int.natAbs
      ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
        ((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module ℤ M] →
                          [inst_11 : Module ℤ M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (Submodule.subtype I) ∘ₗ
          AddMonoidHom.toIntLinearMap (↑e : S →+ ↥I))) =
    (absNorm : (a : Ideal S) → ℕ) I

Tactic:
by_cases hI : I = ⊥
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst_5 : EquivLike E S ↥I
inst_6 : AddEquivClass E S ↥I
e : E
hI : I = ⊥
pos :
  ∀ [inst_7 : EquivLike E S ↥⊥] [inst_8 : AddEquivClass E S ↥⊥],
    Int.natAbs
        ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
          ((↑ℤ :
                {S M M₂ : Type u_1} →
                  [inst : Semiring ℤ] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module ℤ M] →
                            [inst_13 : Module ℤ M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
              (Submodule.subtype ⊥) ∘ₗ
            AddMonoidHom.toIntLinearMap (↑e : S →+ ↥⊥))) =
      (absNorm : (a : Ideal S) → ℕ) ⊥
⊢ Int.natAbs
      ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
        ((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module ℤ M] →
                          [inst_11 : Module ℤ M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (Submodule.subtype I) ∘ₗ
          AddMonoidHom.toIntLinearMap (↑e : S →+ ↥I))) =
    (absNorm : (a : Ideal S) → ℕ) I

Tactic:
subst hI
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
E : Type u_2
e : E
inst_5 : EquivLike E S ↥⊥
inst_6 : AddEquivClass E S ↥⊥
⊢ Ne.{u_1 + 1} (α := S) 1 0

Tactic:
have : (1 : S) ≠ 0 := one_ne_zero
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
E : Type u_2
e : E
inst_5 : EquivLike E S ↥⊥
inst_6 : AddEquivClass E S ↥⊥
this : Ne.{u_1 + 1} (α := S) 1 0
⊢ Eq.{u_1 + 1} (α := S) 1 0

Tactic:
have : (1 : S) = 0 := EquivLike.injective e (Subsingleton.elim _ _)
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
E : Type u_2
e : E
inst_5 : EquivLike E S ↥⊥
inst_6 : AddEquivClass E S ↥⊥
this_1 : Ne.{u_1 + 1} (α := S) 1 0
this : Eq.{u_1 + 1} (α := S) 1 0
⊢ Int.natAbs
      ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
        ((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module ℤ M] →
                          [inst_11 : Module ℤ M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (Submodule.subtype ⊥) ∘ₗ
          AddMonoidHom.toIntLinearMap (↑e : S →+ ↥⊥))) =
    (absNorm : (a : Ideal S) → ℕ) ⊥

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst_5 : EquivLike E S ↥I
inst_6 : AddEquivClass E S ↥I
e : E
hI : ¬I = ⊥
⊢ Int.natAbs
      ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
        ((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module ℤ M] →
                          [inst_11 : Module ℤ M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (Submodule.subtype I) ∘ₗ
          AddMonoidHom.toIntLinearMap (↑e : S →+ ↥I))) =
    (absNorm : (a : Ideal S) → ℕ) I

Tactic:
Submodule.natAbs_det_equiv (I.restrictScalars ℤ) e

Premises used: LinearMap.restrictScalars, AddSubgroup.index, Set.Mem, Submodule.restrictScalars, Nat.card, Int, Submodule.natAbs_det_equiv, Submodule.cardQuot, Submodule.subtype, ENat.toNat, Submodule.quotientRel, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
I : Ideal S
E : Type u_2
inst_5 : EquivLike E S ↥I
inst_6 : AddEquivClass E S ↥I
e : E
hI : ¬I = ⊥
⊢ Int.natAbs
      ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
        ((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module ℤ M] →
                          [inst_11 : Module ℤ M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (Submodule.subtype I) ∘ₗ
          AddMonoidHom.toIntLinearMap (↑e : S →+ ↥I))) =
    (absNorm : (a : Ideal S) → ℕ) I

Tactic:
exact Submodule.natAbs_det_equiv (I.restrictScalars ℤ) e

Premises used: Submodule.restrictScalars, Int, Submodule.natAbs_det_equiv
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
ι : Type u_2
inst_5 : Fintype ι
inst_6 : DecidableEq ι
b : Basis ι ℤ S
I : Ideal S
bI : Basis.{u_2, 0, u_1} ι ℤ ↥I
⊢ Int.natAbs
      ((b.det : (a : ι → S) → ℤ)
        (Function.comp (β := ↥I) (Subtype.val (p := fun (x : S) ↦ x ∈ I)) (⇑bI : (a : ι) → ↥I))) =
    (absNorm : (a : Ideal S) → ℕ) I

Tactic:
Submodule.natAbs_det_basis_change b (I.restrictScalars ℤ) bI

Premises used: AddSubgroup.index, Submodule.restrictScalars, Nat.card, Int, Submodule.cardQuot, ENat.toNat, Submodule.quotientRel, WithTop.untopD, WithTop.recTopCoe, Submodule.natAbs_det_basis_change
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
r : S
pos :
  ∀ (hr : r = 0),
    (absNorm : (a : Ideal S) → ℕ) (span {r}) =
      Int.natAbs
        (((LinearMap.det.{u_1, 0} (M := S) (A := ℤ) : (S →ₗ[ℤ] S) →* ℤ) : (a : S →ₗ[ℤ] S) → ℤ)
          ((Algebra.lmul ℤ S : (a : S) → End ℤ S) r : End ℤ S))
neg :
  ∀ (hr : ¬r = 0),
    (absNorm : (a : Ideal S) → ℕ) (span {r}) =
      Int.natAbs
        (((LinearMap.det.{u_1, 0} (M := S) (A := ℤ) : (S →ₗ[ℤ] S) →* ℤ) : (a : S →ₗ[ℤ] S) → ℤ)
          ((Algebra.lmul ℤ S : (a : S) → End ℤ S) r : End ℤ S))
⊢ (absNorm : (a : Ideal S) → ℕ) (span {r}) =
    Int.natAbs
      (((LinearMap.det.{u_1, 0} (M := S) (A := ℤ) : (S →ₗ[ℤ] S) →* ℤ) : (a : S →ₗ[ℤ] S) → ℤ)
        ((Algebra.lmul ℤ S : (a : S) → End ℤ S) r : End ℤ S))

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
r : S
hr : r = 0
⊢ (absNorm : (a : Ideal S) → ℕ) (span {r}) =
    Int.natAbs
      (((LinearMap.det.{u_1, 0} (M := S) (A := ℤ) : (S →ₗ[ℤ] S) →* ℤ) : (a : S →ₗ[ℤ] S) → ℤ)
        ((Algebra.lmul ℤ S : (a : S) → End ℤ S) r : End ℤ S))

Tactic:
simp only [hr, Ideal.span_zero, Ideal.absNorm_bot,
      LinearMap.det_zero'', Set.singleton_zero, map_zero, Int.natAbs_zero]

Premises used: Int.natAbs_zero, map_zero, Ideal.span_zero, LinearMap.det_zero'', Ideal.absNorm_bot, Set.singleton_zero
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
r : S
hr : ¬r = 0
b : Basis (Free.ChooseBasisIndex ℤ S) ℤ S := Free.chooseBasis ℤ S
neg :
  Int.natAbs
      ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
        ((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module ℤ M] →
                          [inst_9 : Module ℤ M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (Submodule.subtype (span {r})) ∘ₗ
          AddMonoidHom.toIntLinearMap
            (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Free.ChooseBasisIndex ℤ S))) : S →+ ↥(span {r})))) =
    Int.natAbs
      (((LinearMap.det.{u_1, 0} (M := S) (A := ℤ) : (S →ₗ[ℤ] S) →* ℤ) : (a : S →ₗ[ℤ] S) → ℤ)
        ((Algebra.lmul ℤ S : (a : S) → End ℤ S) r : End ℤ S))
⊢ (absNorm : (a : Ideal S) → ℕ) (span {r}) =
    Int.natAbs
      (((LinearMap.det.{u_1, 0} (M := S) (A := ℤ) : (S →ₗ[ℤ] S) →* ℤ) : (a : S →ₗ[ℤ] S) → ℤ)
        ((Algebra.lmul ℤ S : (a : S) → End ℤ S) r : End ℤ S))

Tactic:
rw [← natAbs_det_equiv _ (b.equiv (basisSpanSingleton b hr) (Equiv.refl _))]

Premises used: Module.Basis.equiv, Ideal.natAbs_det_equiv, Ideal.basisSpanSingleton, Equiv.refl
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
r : S
hr : ¬r = 0
b : Basis (Free.ChooseBasisIndex ℤ S) ℤ S := Free.chooseBasis ℤ S
neg :
  Eq (α := LinearMap (R := ℤ) (RingHom.id ℤ) S S)
    ((↑ℤ :
          {S M M₂ : Type u_1} →
            [inst : Semiring ℤ] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module ℤ M] →
                      [inst_9 : Module ℤ M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
        (Submodule.subtype (span {r})) ∘ₗ
      AddMonoidHom.toIntLinearMap
        (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Free.ChooseBasisIndex ℤ S))) : S →+ ↥(span {r})))
    ((Algebra.lmul ℤ S : (a : S) → End ℤ S) r)
⊢ Int.natAbs
      ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
        ((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module ℤ M] →
                          [inst_9 : Module ℤ M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (Submodule.subtype (span {r})) ∘ₗ
          AddMonoidHom.toIntLinearMap
            (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Free.ChooseBasisIndex ℤ S))) : S →+ ↥(span {r})))) =
    Int.natAbs
      (((LinearMap.det.{u_1, 0} (M := S) (A := ℤ) : (S →ₗ[ℤ] S) →* ℤ) : (a : S →ₗ[ℤ] S) → ℤ)
        ((Algebra.lmul ℤ S : (a : S) → End ℤ S) r : End ℤ S))

Tactic:
congr
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
r : S
hr : ¬r = 0
b : Basis (Free.ChooseBasisIndex ℤ S) ℤ S := Free.chooseBasis ℤ S
⊢ Eq (α := LinearMap (R := ℤ) (RingHom.id ℤ) S S)
    ((↑ℤ :
          {S M M₂ : Type u_1} →
            [inst : Semiring ℤ] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module ℤ M] →
                      [inst_9 : Module ℤ M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
        (Submodule.subtype (span {r})) ∘ₗ
      AddMonoidHom.toIntLinearMap
        (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Free.ChooseBasisIndex ℤ S))) : S →+ ↥(span {r})))
    ((Algebra.lmul ℤ S : (a : S) → End ℤ S) r)

Tactic:
b.ext fun i => ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
r : S
hr : ¬r = 0
b : Basis (Free.ChooseBasisIndex ℤ S) ℤ S := Free.chooseBasis ℤ S
neg :
  ∀ (i : Free.ChooseBasisIndex ℤ S),
    Eq (α := S)
      (((↑ℤ :
                  {S M M₂ : Type u_1} →
                    [inst : Semiring ℤ] →
                      [inst_5 : Semiring S] →
                        [inst_6 : AddCommMonoid M] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module ℤ M] →
                              [inst_9 : Module ℤ M₂] →
                                [inst_10 : Module S M] →
                                  [inst_11 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
                (Submodule.subtype (span {r})) ∘ₗ
              AddMonoidHom.toIntLinearMap
                (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Free.ChooseBasisIndex ℤ S))) : S →+ ↥(span {r})) :
            (a : S) → S)
          ((b : (a : Free.ChooseBasisIndex ℤ S) → S) i : S) :
        S)
      ((((Algebra.lmul ℤ S : (a : S) → End ℤ S) r : End ℤ S) : (a : S) → S)
          ((b : (a : Free.ChooseBasisIndex ℤ S) → S) i : S) :
        S)
⊢ Eq (α := LinearMap (R := ℤ) (RingHom.id ℤ) S S)
    ((↑ℤ :
          {S M M₂ : Type u_1} →
            [inst : Semiring ℤ] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module ℤ M] →
                      [inst_9 : Module ℤ M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
        (Submodule.subtype (span {r})) ∘ₗ
      AddMonoidHom.toIntLinearMap
        (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Free.ChooseBasisIndex ℤ S))) : S →+ ↥(span {r})))
    ((Algebra.lmul ℤ S : (a : S) → End ℤ S) r)

Tactic:
refine b.ext fun i => ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
r : S
hr : ¬r = 0
b : Basis (Free.ChooseBasisIndex ℤ S) ℤ S := Free.chooseBasis ℤ S
i : Free.ChooseBasisIndex ℤ S
⊢ Eq (α := S)
    (((↑ℤ :
                {S M M₂ : Type u_1} →
                  [inst : Semiring ℤ] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module ℤ M] →
                            [inst_9 : Module ℤ M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
              (Submodule.subtype (span {r})) ∘ₗ
            AddMonoidHom.toIntLinearMap
              (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Free.ChooseBasisIndex ℤ S))) : S →+ ↥(span {r})) :
          (a : S) → S)
        ((b : (a : Free.ChooseBasisIndex ℤ S) → S) i : S) :
      S)
    ((((Algebra.lmul ℤ S : (a : S) → End ℤ S) r : End ℤ S) : (a : S) → S)
        ((b : (a : Free.ChooseBasisIndex ℤ S) → S) i : S) :
      S)

Tactic:
simp