awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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 ↥⊤
⊢ motive M

Tactic:
exact equiv _ _ Submodule.topEquiv H

Premises used: Submodule.topEquiv
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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₂}) =
    ⊤
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)))
⊢ motive M

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
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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
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₂}))
⊢ 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)))

Tactic:
change motive s.head

Premises used: Membership.mem, Subtype, RelSeries.head
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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
zero : motive ↥⊥
⊢ 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:
rw [hs1]
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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 ↥⊥

Tactic:
subsingleton _
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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 ↥⊥

Tactic:
exact subsingleton _
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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
inst_7 : Subsingleton N
⊢ Set.Finite (α := Ideal A) (associatedPrimes A N)

Tactic:
simp [associatedPrimes.eq_empty_of_subsingleton]

Premises used: associatedPrimes.eq_empty_of_subsingleton
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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
⊢ Eq (α := Set (Ideal A)) (associatedPrimes A (A ⧸ p.asIdeal)) {p.asIdeal.radical}

Tactic:
have := associatedPrimes.eq_singleton_of_isPrimary p.2.isPrimary
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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
this : Eq (α := Set (Ideal A)) (associatedPrimes A (A ⧸ p.asIdeal)) {p.asIdeal.radical}
⊢ Set.Finite (α := Ideal A) (associatedPrimes A N)

Tactic:
simp [LinearEquiv.AssociatedPrimes.eq f, this]

Premises used: LinearEquiv.AssociatedPrimes.eq
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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₁
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₃
hf : Function.Injective (α := N₁) (β := N₂) (⇑f : (a : N₁) → N₂)
h : 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:
(h₁.union h₃).subset (associatedPrimes.subset_union_of_exact hf hfg)

Premises used: Set.Finite.union, Set.Finite.subset, associatedPrimes.subset_union_of_exact
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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₁
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₃
hf : Function.Injective (α := N₁) (β := N₂) (⇑f : (a : N₁) → N₂)
h : 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:
exact (h₁.union h₃).subset (associatedPrimes.subset_union_of_exact hf hfg)

Premises used: Set.Finite.union, Set.Finite.subset, associatedPrimes.subset_union_of_exact
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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)
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₂)
⊢ Set.Finite (α := Ideal A) (associatedPrimes A M)

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)

Premises used: associatedPrimes.eq_empty_of_subsingleton, Module.Finite
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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)
simp_rw : (↑I : Set A) ⊆ (↑(nonZeroDivisors A) : Set A)ᶜ
⊢ (↑I : Set A) ⊆
    ⋃ (i : Ideal A), ⋃ (_ : Membership.mem (γ := Set (Ideal A)) (associatedPrimes A A) i), (↑(id i) : Set A)

Tactic:
simp_rw [id, biUnion_associatedPrimes_eq_compl_nonZeroDivisors]

Premises used: id, biUnion_associatedPrimes_eq_compl_nonZeroDivisors
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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) ⊆ (↑(nonZeroDivisors A) : Set A)ᶜ

Tactic:
fun x hx h ↦ hI.ne_top <| I.eq_top_of_isUnit_mem hx
      (IsFractionRing.self_iff_nonZeroDivisors_le_isUnit.mp ‹_› h)

Premises used: Set.Mem, setOf, Ideal.eq_top_of_isUnit_mem, Set.Subset, Iff.mp, Ideal.IsMaximal.ne_top, IsFractionRing.self_iff_nonZeroDivisors_le_isUnit, Not
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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) ⊆ (↑(nonZeroDivisors A) : Set A)ᶜ

Tactic:
exact fun x hx h ↦ hI.ne_top <| I.eq_top_of_isUnit_mem hx
      (IsFractionRing.self_iff_nonZeroDivisors_le_isUnit.mp ‹_› h)

Premises used: Ideal.eq_top_of_isUnit_mem, Iff.mp, Ideal.IsMaximal.ne_top, IsFractionRing.self_iff_nonZeroDivisors_le_isUnit
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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
inst_5 : IsFractionRing A A
⊢ Finite.{u + 1} (MaximalSpectrum A)

Tactic:
(MaximalSpectrum.equivSubtype A).finite_iff.mpr <| Set.finite_coe_iff.mpr <|
    (associatedPrimes.finite A A).subset fun _ ↦ (·.mem_associatedPrimes_of_isFractionRing)

Premises used: Iff.mpr, Ideal.IsMaximal.mem_associatedPrimes_of_isFractionRing, associatedPrimes.finite, Equiv.finite_iff, Set.Finite.subset, Set.finite_coe_iff, MaximalSpectrum.equivSubtype
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
inst_1 : IsNoetherianRing A
I : Ideal A
h : Disjoint (↑I : Set A) (↑(nonZeroDivisors A) : Set A)
⊢ ∃ (P : Ideal A), Membership.mem (γ := Set (Ideal A)) (associatedPrimes A A) P ∧ I ≤ P

Tactic:
(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

Premises used: Disjoint.subset_compl_right, Set.Mem, associatedPrimes.finite, Eq.rec, Ideal.subset_union_prime_finite, biUnion_associatedPrimes_eq_compl_nonZeroDivisors, Iff.mp, OfNat.ofNat, Eq.symm, Submodule.IsAssociatedPrime.toIsPrime