awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
have 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) → ℕ) ⊥
Tactic: subst hI
Cleared hypotheses: I, inst_5, inst_6, hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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 ↥⊥
⊢ 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) → ℕ) ⊥
have this : Ne.{u_1 + 1} (α := S) 1 0
Tactic: have : (1 : S) ≠ 0 := one_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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
⊢ 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) → ℕ) ⊥
have this₁ : Eq.{u_1 + 1} (α := S) 1 0
Tactic: have : (1 : S) = 0 := EquivLike.injective e (Subsingleton.elim _ _)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ (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))
have 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))
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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))
⊢ (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))
have 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))
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ (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))
have 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))
Tactic: rw [← natAbs_det_equiv _ (b.equiv (basisSpanSingleton b hr) (Equiv.refl _))]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ 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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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)
have 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)
Tactic: refine b.ext fun i => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
x : S
h : x ∈ I
⊢ Dvd.dvd (α := ℤ) ((↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ) : ℤ) ((Algebra.norm ℤ : (a : S) → ℤ) x : ℤ)
have rw : Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ((absNorm : (a : Ideal S) → ℕ) (span {x}) : ℕ)
Tactic: rw [← Int.dvd_natAbs, ← absNorm_span_singleton x, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
s : Set S
⊢ (absNorm : (a : Ideal S) → ℕ) (span {r}) ∣ Int.natAbs ((Algebra.norm ℤ : (a : S) → ℤ) r)
have rw : Int.natAbs ((Algebra.norm ℤ : (a : S) → ℤ) r) ∣ Int.natAbs ((Algebra.norm ℤ : (a : S) → ℤ) r)
Tactic: rw [absNorm_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ I = ⊥
have mp : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) → I = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
mp : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) → I = ⊥
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ I = ⊥
have mpr : I = ⊥ → Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
hI : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
⊢ I = ⊥
have mp : I ≤ ⊥
Tactic: rw [← le_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
hI : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
x : S
hx : x ∈ I
⊢ Membership.mem (γ := Submodule S S) ⊥ x
have mp : Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ((absNorm : (a : Ideal S) → ℕ) (span {x}) : ℕ)
Tactic: rw [mem_bot, ← Algebra.norm_eq_zero_iff (R := ℤ), ← Int.natAbs_eq_zero,
      ← Ideal.absNorm_span_singleton, ← zero_dvd_iff, ← hI]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
hI : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
x : S
hx : x ∈ I
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ((absNorm : (a : Ideal S) → ℕ) (span {x}) : ℕ)
have mp : span {x} ≤ I
Tactic: apply Ideal.absNorm_dvd_absNorm_of_le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
have simp_rw : ¬Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
Tactic: simp_rw [ne_eq, Ideal.absNorm_eq_zero_iff, mem_nonZeroDivisors_iff_ne_zero, Submodule.zero_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
simp_rw :
  ¬Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
⊢ Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
have simp_rw₁ : ¬I = ⊥ ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
Tactic: simp_rw [ne_eq, Ideal.absNorm_eq_zero_iff, mem_nonZeroDivisors_iff_ne_zero, Submodule.zero_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
simp_rw :
  ¬Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
simp_rw₁ : ¬I = ⊥ ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
⊢ Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
have simp_rw₂ : ¬I = ⊥ ↔ I ≠ 0
Tactic: simp_rw [ne_eq, Ideal.absNorm_eq_zero_iff, mem_nonZeroDivisors_iff_ne_zero, Submodule.zero_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ LT.lt (α := ℕ) (0 : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
have rw : LT.lt (α := ℕ) (0 : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ↔ Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
Tactic: rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, Nat.pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
rw :
  LT.lt (α := ℕ) (0 : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ↔
    Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
⊢ LT.lt (α := ℕ) (0 : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ↔ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
have rw₁ : Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
Tactic: rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, Nat.pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
hI : I ≠ ⊥
⊢ AddSubgroup.FiniteIndex.{u_1} (G := S) (toAddSubgroup I)
have rwa : AddSubgroup.index.{u_1} (G := S) (toAddSubgroup I) ≠ 0
Tactic: rwa [AddSubgroup.finiteIndex_iff, ← absNorm_eq_index, Ne, absNorm_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
hI : I ≠ ⊥
rwa : AddSubgroup.index.{u_1} (G := S) (toAddSubgroup I) ≠ 0
⊢ AddSubgroup.FiniteIndex.{u_1} (G := S) (toAddSubgroup I)
have rwa₁ : Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
Tactic: rwa [AddSubgroup.finiteIndex_iff, ← absNorm_eq_index, Ne, absNorm_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
hI : I ≠ ⊥
rwa : AddSubgroup.index.{u_1} (G := S) (toAddSubgroup I) ≠ 0
rwa₁ : Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
⊢ AddSubgroup.FiniteIndex.{u_1} (G := S) (toAddSubgroup I)
have rwa₂ : ¬Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
Tactic: rwa [AddSubgroup.finiteIndex_iff, ← absNorm_eq_index, Ne, absNorm_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
hI : I ≠ ⊥
rwa : AddSubgroup.index.{u_1} (G := S) (toAddSubgroup I) ≠ 0
rwa₁ : Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
rwa₂ : ¬Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
⊢ AddSubgroup.FiniteIndex.{u_1} (G := S) (toAddSubgroup I)
have rwa₃ : ¬I = ⊥
Tactic: rwa [AddSubgroup.finiteIndex_iff, ← absNorm_eq_index, Ne, absNorm_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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
hI : I ≠ ⊥
J : Ideal S
⊢ IsFiniteRelIndex.{u_1} (G := S) (toAddSubgroup I) (toAddSubgroup J)
have this : FiniteIndex.{u_1} (G := S) (toAddSubgroup I)
Tactic: have := finiteIndex hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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
P : Ideal S
inst_5 : P.IsMaximal
⊢ ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n
have this : IsAddTorsionFree S
Tactic: have : IsAddTorsionFree S := .of_isTorsionFree ℤ _
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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
P : Ideal S
inst_5 : P.IsMaximal
this : IsAddTorsionFree S
⊢ ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n
have this₁ : CharZero S
Tactic: have := CharZero.of_isAddTorsionFree S S
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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
P : Ideal S
inst_5 : P.IsMaximal
this_1 : IsAddTorsionFree S
this : CharZero S
⊢ ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n
have this₁ : Finite.{u_1 + 1} (S ⧸ P)
Tactic: have : Finite (S ⧸ P) := Submodule.finiteQuotientOfFreeOfRankEq (P.restrictScalars ℤ)
    (Ideal.finrank_eq_finrank (Module.Free.chooseBasis _ _) _
      (Ideal.IsMaximal.ne_bot_of_isIntegral_int P))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
P : Ideal S
inst_5 : P.IsMaximal
this_1 : IsAddTorsionFree S
this_2 : CharZero S
this : Finite.{u_1 + 1} (S ⧸ P)
⊢ ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n
have intro : ∀ (val : Fintype (S ⧸ P)),
  ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n
Tactic: cases nonempty_fintype (S ⧸ P)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
P : Ideal S
inst_5 : P.IsMaximal
this_1 : IsAddTorsionFree S
this_2 : CharZero S
this_3 : Finite.{u_1 + 1} (S ⧸ P)
val : Fintype (S ⧸ P)
this : Field (S ⧸ P) := Quotient.field P
⊢ ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n
have intro : ∀ (p : ℕ) (hpR : CharP.{u_1} (S ⧸ P) p),
  ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n
Tactic: obtain ⟨p, hpR⟩ := CharP.exists (S ⧸ P)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
P : Ideal S
inst_5 : P.IsMaximal
this_1 : IsAddTorsionFree S
this_2 : CharZero S
this_3 : Finite.{u_1 + 1} (S ⧸ P)
val : Fintype (S ⧸ P)
this : Field (S ⧸ P) := Quotient.field P
p : ℕ
hpR : CharP.{u_1} (S ⧸ P) p
⊢ ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n
have intro : ∀ (n : ℕ+) (hp : Nat.Prime p) (e : Fintype.card.{u_1} (S ⧸ P) = p ^ (↑n : ℕ)),
  ∃ (p : ℕ) (n : ℕ), 0 < n ∧ (↑p : S) ∈ P ∧ Nat.Prime p ∧ (absNorm : (a : Ideal S) → ℕ) P = p ^ n
Tactic: obtain ⟨n, hp, e⟩ := FiniteField.card (S ⧸ P) p