awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (hypothesis)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsNoetherianRing A
inst_4 : Module.Finite A M
N : Submodule A M
hN : N ≠ ⊤
s :
  RelSeries (α := Submodule A M)
    {x : Submodule A M × Submodule A M |
      match (motive := Submodule A M × Submodule A M → Prop) x with
      | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}
hs₁ :
  s.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
    ⊥
hs₂ :
  s.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
    N
this : Nontrivial.{v} (M ⧸ N)
x : M
hp :
  Ideal.IsPrime.{u} (α := A)
    (Submodule.colon (M := M ⧸ N) ⊥ (singleton (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) x : M ⧸ N)))
hxN : x ∉ N
⊢ ∃ M_1 > N,
    ∃ (s :
      RelSeries (α := Submodule A M)
        {x : Submodule A M × Submodule A M |
          match (motive := Submodule A M × Submodule A M → Prop) x with
          | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}),
      s.head (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
          ⊥ ∧
        s.last (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
          M_1
have this₁ : N.IsQuotientEquivQuotientPrime (N ⊔ A ∙ x)
Tactic: have := Submodule.isQuotientEquivQuotientPrime_iff.mpr ⟨x, hp, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module A M
h : Module.Finite A M
motive : (N : Type v) → [inst_4 : AddCommGroup N] → [inst_5 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst_6 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
    [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (N₃ : Type v)
    [inst_10 : AddCommGroup N₃] [inst_11 : Module A N₃] [inst_12 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂)
    (g : N₂ →ₗ[A] N₃),
    Function.Injective (α := N₁) (β := N₂) (⇑f : (a : N₁) → N₂) →
      Function.Surjective (α := N₂) (β := N₃) (⇑g : (a : N₂) → N₃) →
        Function.Exact (M := N₁) (N := N₂) (P := N₃) (⇑f : (a : N₁) → N₂) (⇑g : (a : N₂) → N₃) →
          motive N₁ → motive N₃ → motive N₂
⊢ motive M
have have : ∀
  (equiv :
    ∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
      [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂) (h : motive N₁),
      motive N₂),
  motive M
Tactic: have equiv (N₁ : Type v) [AddCommGroup N₁] [Module A N₁] [Module.Finite A N₁]
      (N₂ : Type v) [AddCommGroup N₂] [Module A N₂] [Module.Finite A N₂]
      (f : N₁ ≃ₗ[A] N₂) (h : motive N₁) : motive N₂ :=
    exact N₁ N₂ PUnit.{v + 1} f 0 f.injective (Function.surjective_to_subsingleton _)
      ((f.exact_zero_iff_surjective _).2 f.surjective) h (subsingleton _)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module A M
h : Module.Finite A M
motive : (N : Type v) → [inst_4 : AddCommGroup N] → [inst_5 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst_6 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
    [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (N₃ : Type v)
    [inst_10 : AddCommGroup N₃] [inst_11 : Module A N₃] [inst_12 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂)
    (g : N₂ →ₗ[A] N₃),
    Function.Injective (α := N₁) (β := N₂) (⇑f : (a : N₁) → N₂) →
      Function.Surjective (α := N₂) (β := N₃) (⇑g : (a : N₂) → N₃) →
        Function.Exact (M := N₁) (N := N₂) (P := N₃) (⇑f : (a : N₁) → N₂) (⇑g : (a : N₂) → N₃) →
          motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
    [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂) (h : motive N₁),
    motive N₂
⊢ motive M
have obtain : ∀
  (s :
    RelSeries (α := Submodule A M)
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂})
  (hs1 :
    s.head (r :=
        {x : Submodule A M × Submodule A M |
          match (motive := Submodule A M × Submodule A M → Prop) x with
          | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
      ⊥)
  (hs2 :
    s.last (r :=
        {x : Submodule A M × Submodule A M |
          match (motive := Submodule A M × Submodule A M → Prop) x with
          | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
      ⊤),
  motive M
Tactic: obtain ⟨s, hs1, hs2⟩ := IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime A M
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (hypothesis)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module A M
h : Module.Finite A M
motive : (N : Type v) → [inst_4 : AddCommGroup N] → [inst_5 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst_6 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
    [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (N₃ : Type v)
    [inst_10 : AddCommGroup N₃] [inst_11 : Module A N₃] [inst_12 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂)
    (g : N₂ →ₗ[A] N₃),
    Function.Injective (α := N₁) (β := N₂) (⇑f : (a : N₁) → N₂) →
      Function.Surjective (α := N₂) (β := N₃) (⇑g : (a : N₂) → N₃) →
        Function.Exact (M := N₁) (N := N₂) (P := N₃) (⇑f : (a : N₁) → N₂) (⇑g : (a : N₂) → N₃) →
          motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
    [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂) (h : motive N₁),
    motive N₂
s :
  RelSeries (α := Submodule A M)
    {x : Submodule A M × Submodule A M |
      match (motive := Submodule A M × Submodule A M → Prop) x with
      | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}
hs1 :
  s.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
    ⊥
hs2 :
  s.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
    ⊤
H :
  motive
    ↥(s.last (r :=
        {x : Submodule A M × Submodule A M |
          match (motive := Submodule A M × Submodule A M → Prop) x with
          | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}))
⊢ motive M
have H₁ : motive ↥⊤
Tactic: rw [hs2] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module A M
h : Module.Finite A M
motive : (N : Type v) → [inst_4 : AddCommGroup N] → [inst_5 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst_6 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
    [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (N₃ : Type v)
    [inst_10 : AddCommGroup N₃] [inst_11 : Module A N₃] [inst_12 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂)
    (g : N₂ →ₗ[A] N₃),
    Function.Injective (α := N₁) (β := N₂) (⇑f : (a : N₁) → N₂) →
      Function.Surjective (α := N₂) (β := N₃) (⇑g : (a : N₂) → N₃) →
        Function.Exact (M := N₁) (N := N₂) (P := N₃) (⇑f : (a : N₁) → N₂) (⇑g : (a : N₂) → N₃) →
          motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
    [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂) (h : motive N₁),
    motive N₂
s :
  RelSeries (α := Submodule A M)
    {x : Submodule A M × Submodule A M |
      match (motive := Submodule A M × Submodule A M → Prop) x with
      | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}
hs1 :
  s.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
    ⊥
hs2 :
  s.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
    ⊤
⊢ motive M
have suffices : ∀ (n : ℕ)
  (h_1 :
    n <
      s.length (r :=
          {x : Submodule A M × Submodule A M |
            match (motive := Submodule A M × Submodule A M → Prop) x with
            | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) +
        1),
  motive
    ↥(s.toFun (r :=
        {x : Submodule A M × Submodule A M |
          match (motive := Submodule A M × Submodule A M → Prop) x with
          | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂})
        (⟨n, h_1⟩ :
          Fin
            (s.length (r :=
                {x : Submodule A M × Submodule A M |
                  match (motive := Submodule A M × Submodule A M → Prop) x with
                  | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) +
              1)))
Tactic: suffices H : ∀ n, (h : n < s.length + 1) → motive (s ⟨n, h⟩) by
    replace H : motive s.last := H s.length s.length.lt_add_one
    rw [hs2] at H
    exact equiv _ _ Submodule.topEquiv H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module A M
h_1 : Module.Finite A M
motive : (N : Type v) → [inst_4 : AddCommGroup N] → [inst_5 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst_6 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
    [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (N₃ : Type v)
    [inst_10 : AddCommGroup N₃] [inst_11 : Module A N₃] [inst_12 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂)
    (g : N₂ →ₗ[A] N₃),
    Function.Injective (α := N₁) (β := N₂) (⇑f : (a : N₁) → N₂) →
      Function.Surjective (α := N₂) (β := N₃) (⇑g : (a : N₂) → N₃) →
        Function.Exact (M := N₁) (N := N₂) (P := N₃) (⇑f : (a : N₁) → N₂) (⇑g : (a : N₂) → N₃) →
          motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
    [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂) (h : motive N₁),
    motive N₂
s :
  RelSeries (α := Submodule A M)
    {x : Submodule A M × Submodule A M |
      match (motive := Submodule A M × Submodule A M → Prop) x with
      | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}
hs1 :
  s.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
    ⊥
hs2 :
  s.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
    ⊤
h :
  0 <
    s.length (r :=
        {x : Submodule A M × Submodule A M |
          match (motive := Submodule A M × Submodule A M → Prop) x with
          | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) +
      1
⊢ motive
    ↥(s.toFun (r :=
        {x : Submodule A M × Submodule A M |
          match (motive := Submodule A M × Submodule A M → Prop) x with
          | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂})
        (⟨0, h⟩ :
          Fin
            (s.length (r :=
                {x : Submodule A M × Submodule A M |
                  match (motive := Submodule A M × Submodule A M → Prop) x with
                  | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) +
              1)))
have zero : motive
  ↥(s.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}))
Tactic: change motive s.head
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module A M
h_1 : Module.Finite A M
motive : (N : Type v) → [inst_4 : AddCommGroup N] → [inst_5 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst_6 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
    [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (N₃ : Type v)
    [inst_10 : AddCommGroup N₃] [inst_11 : Module A N₃] [inst_12 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂)
    (g : N₂ →ₗ[A] N₃),
    Function.Injective (α := N₁) (β := N₂) (⇑f : (a : N₁) → N₂) →
      Function.Surjective (α := N₂) (β := N₃) (⇑g : (a : N₂) → N₃) →
        Function.Exact (M := N₁) (N := N₂) (P := N₃) (⇑f : (a : N₁) → N₂) (⇑g : (a : N₂) → N₃) →
          motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
    [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂) (h : motive N₁),
    motive N₂
s :
  RelSeries (α := Submodule A M)
    {x : Submodule A M × Submodule A M |
      match (motive := Submodule A M × Submodule A M → Prop) x with
      | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}
hs1 :
  s.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
    ⊥
hs2 :
  s.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) =
    ⊤
h :
  0 <
    s.length (r :=
        {x : Submodule A M × Submodule A M |
          match (motive := Submodule A M × Submodule A M → Prop) x with
          | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}) +
      1
⊢ motive
    ↥(s.head (r :=
        {x : Submodule A M × Submodule A M |
          match (motive := Submodule A M × Submodule A M → Prop) x with
          | (N₁, N₂) => N₁.IsQuotientEquivQuotientPrime N₂}))
have zero : motive ↥⊥
Tactic: rw [hs1]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (hypothesis)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsNoetherianRing A
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
inst_6 : Module.Finite A N
p : PrimeSpectrum A
f : N ≃ₗ[A] A ⧸ p.asIdeal
⊢ Set.Finite (α := Ideal A) (associatedPrimes A N)
have this : Eq (α := Set (Ideal A)) (associatedPrimes A (A ⧸ p.asIdeal)) {p.asIdeal.radical}
Tactic: have := associatedPrimes.eq_singleton_of_isPrimary p.2.isPrimary
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsNoetherianRing A
inst_4 induction : Module.Finite A M
⊢ Set.Finite (α := Ideal A) (associatedPrimes A M)
have subsingleton : ∀ (N : Type v) [inst_5 : AddCommGroup N] [inst_6 : Module A N] [Module.Finite A N] [Subsingleton N],
  Set.Finite (α := Ideal A) (associatedPrimes A N)
Tactic: induction ‹Module.Finite A M› using
    IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime A with
  | subsingleton N => simp [associatedPrimes.eq_empty_of_subsingleton]
  | quotient N p f =>
    have := associatedPrimes.eq_singleton_of_isPrimary p.2.isPrimary
    simp [LinearEquiv.AssociatedPrimes.eq f, this]
  | exact N₁ N₂ N₃ f g hf _ hfg h₁ h₃ =>
    exact (h₁.union h₃).subset (associatedPrimes.subset_union_of_exact hf hfg)
Cleared hypotheses: inst_4
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsNoetherianRing A
inst_4 induction : Module.Finite A M
subsingleton :
  ∀ (N : Type v) [inst_5 : AddCommGroup N] [inst_6 : Module A N] [Module.Finite A N] [Subsingleton N],
    Set.Finite (α := Ideal A) (associatedPrimes A N)
⊢ Set.Finite (α := Ideal A) (associatedPrimes A M)
have quotient : ∀ (N : Type v) [inst_5 : AddCommGroup N] [inst_6 : Module A N] [Module.Finite A N] (p : PrimeSpectrum A)
  (f : N ≃ₗ[A] A ⧸ p.asIdeal), Set.Finite (α := Ideal A) (associatedPrimes A N)
Tactic: induction ‹Module.Finite A M› using
    IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime A with
  | subsingleton N => simp [associatedPrimes.eq_empty_of_subsingleton]
  | quotient N p f =>
    have := associatedPrimes.eq_singleton_of_isPrimary p.2.isPrimary
    simp [LinearEquiv.AssociatedPrimes.eq f, this]
  | exact N₁ N₂ N₃ f g hf _ hfg h₁ h₃ =>
    exact (h₁.union h₃).subset (associatedPrimes.subset_union_of_exact hf hfg)
Cleared hypotheses: inst_4
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsNoetherianRing A
inst_4 induction : Module.Finite A M
subsingleton :
  ∀ (N : Type v) [inst_5 : AddCommGroup N] [inst_6 : Module A N] [Module.Finite A N] [Subsingleton N],
    Set.Finite (α := Ideal A) (associatedPrimes A N)
quotient :
  ∀ (N : Type v) [inst_5 : AddCommGroup N] [inst_6 : Module A N] [Module.Finite A N] (p : PrimeSpectrum A)
    (f : N ≃ₗ[A] A ⧸ p.asIdeal), Set.Finite (α := Ideal A) (associatedPrimes A N)
⊢ Set.Finite (α := Ideal A) (associatedPrimes A M)
have exact : ∀ (N₁ : Type v) [inst_5 : AddCommGroup N₁] [inst_6 : Module A N₁] [Module.Finite A N₁] (N₂ : Type v)
  [inst_8 : AddCommGroup N₂] [inst_9 : Module A N₂] [Module.Finite A N₂] (N₃ : Type v) [inst_11 : AddCommGroup N₃]
  [inst_12 : Module A N₃] [Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃)
  (hf : Function.Injective (α := N₁) (β := N₂) (⇑f : (a : N₁) → N₂)),
  Function.Surjective (α := N₂) (β := N₃) (⇑g : (a : N₂) → N₃) →
    ∀ (hfg : Function.Exact (M := N₁) (N := N₂) (P := N₃) (⇑f : (a : N₁) → N₂) (⇑g : (a : N₂) → N₃))
      (h₁ : Set.Finite (α := Ideal A) (associatedPrimes A N₁)) (h₃ : Set.Finite (α := Ideal A) (associatedPrimes A N₃)),
      Set.Finite (α := Ideal A) (associatedPrimes A N₂)
Tactic: induction ‹Module.Finite A M› using
    IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime A with
  | subsingleton N => simp [associatedPrimes.eq_empty_of_subsingleton]
  | quotient N p f =>
    have := associatedPrimes.eq_singleton_of_isPrimary p.2.isPrimary
    simp [LinearEquiv.AssociatedPrimes.eq f, this]
  | exact N₁ N₂ N₃ f g hf _ hfg h₁ h₃ =>
    exact (h₁.union h₃).subset (associatedPrimes.subset_union_of_exact hf hfg)
Cleared hypotheses: inst_4
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
inst_2 : IsFractionRing A A
I : Ideal A
hI : I.IsMaximal
fin : Set.Finite (α := Ideal A) (associatedPrimes A A)
⊢ (↑I : Set A) ⊆
    ⋃ (i : Ideal A), ⋃ (_ : Membership.mem (γ := Set (Ideal A)) (associatedPrimes A A) i), (↑(id i) : Set A)
have simp_rw : (↑I : Set A) ⊆ (↑(nonZeroDivisors A) : Set A)ᶜ
Tactic: simp_rw [id, biUnion_associatedPrimes_eq_compl_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
h : Disjoint (↑I : Set A) (↑(nonZeroDivisors A) : Set A)
⊢ LT.lt (α := Ideal A) ⊥ (Module.annihilator A ↥I)
have obtain : ∀ (P : Ideal A) (h : Membership.mem (γ := Set (Ideal A)) (associatedPrimes A A) P) (hP : I ≤ P),
  LT.lt (α := Ideal A) ⊥ (Module.annihilator A ↥I)
Tactic: obtain ⟨P, h, hP⟩ : ∃ P ∈ associatedPrimes A A, I ≤ P :=
    (I.subset_union_prime_finite (associatedPrimes.finite ..) (f := id) 0 0 fun _ h _ _ ↦ h.1).1 <|
    biUnion_associatedPrimes_eq_compl_nonZeroDivisors A ▸ h.subset_compl_right
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (hypothesis)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
h_1 : Disjoint (↑I : Set A) (↑(nonZeroDivisors A) : Set A)
P : Ideal A
h : Membership.mem (γ := Set (Ideal A)) (associatedPrimes A A) P
hP : I ≤ P
⊢ LT.lt (α := Ideal A) ⊥ (Module.annihilator A ↥I)
have h₁ : P.IsPrime ∧ ∃ (x : A), P = Submodule.colon (M := A) ⊥ {x}
Tactic: rw [AssociatedPrimes.mem_iff, isAssociatedPrime_iff] at h
Cleared hypotheses: h, hP
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
h_1 : Disjoint (↑I : Set A) (↑(nonZeroDivisors A) : Set A)
P : Ideal A
h : P.IsPrime ∧ ∃ (x : A), P = Submodule.colon (M := A) ⊥ {x}
hP : I ≤ P
⊢ LT.lt (α := Ideal A) ⊥ (Module.annihilator A ↥I)
have obtain : ∀ (x : A) (hP : I ≤ Submodule.colon (M := A) ⊥ {x}) (prime : IsPrime (α := A) (Submodule.colon (M := A) ⊥ {x})),
  LT.lt (α := Ideal A) ⊥ (Module.annihilator A ↥I)
Tactic: obtain ⟨prime, x, rfl⟩ := h
Cleared hypotheses: P, h, hP
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
inst_2 : FaithfulSMul A ↥I
⊢ ((↑I : Set A) ∩ (↑(nonZeroDivisors A) : Set A)).Nonempty
have by_contra! : ∀ (this : (↑I : Set A) ∩ (↑(nonZeroDivisors A) : Set A) = ∅), False
Tactic: by_contra!