awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h :
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
x : M
hx :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
⊢ { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)), isPrime := hx :
        PrimeSpectrum A }.asIdeal ≤
    comap (toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂)) (N₁.submoduleOf N₂)

Tactic:
simp [SetLike.le_def, ← Quotient.mk_smul, submoduleOf]

Premises used: SetLike.le_def, Submodule.Quotient.mk_smul, Submodule.submoduleOf
-- 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
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h :
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
x : M
hx :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
⊢ Function.Injective.{u + 1, v + 1} (α :=
    A ⧸
      { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
          isPrime := hx : PrimeSpectrum A }.asIdeal)
    (β := ↥N₂ ⧸ N₁.submoduleOf N₂)
    (⇑(mapQ
          { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
              isPrime := hx }.asIdeal
          (N₁.submoduleOf N₂) (toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂)) ⋯) :
      (a : A ⧸ { asIdeal := ⊥.colon {(N₁.mkQ : (a : M) → M ⧸ N₁) x}, isPrime := hx }.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂)

Tactic:
ker_eq_bot.mp (ker_liftQ_eq_bot _ _ _ ?_)

Premises used: LinearMap.ker_eq_bot, Submodule.ker_liftQ_eq_bot, Iff.mp
-- 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
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h :
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
x : M
hx :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
refine_2 :
  ((N₁.submoduleOf N₂).mkQ ∘ₗ toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂)).ker ≤
    { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
        isPrime := hx }.asIdeal
⊢ Function.Injective.{u + 1, v + 1} (α :=
    A ⧸
      { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
          isPrime := hx : PrimeSpectrum A }.asIdeal)
    (β := ↥N₂ ⧸ N₁.submoduleOf N₂)
    (⇑(mapQ
          { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
              isPrime := hx }.asIdeal
          (N₁.submoduleOf N₂) (toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂)) ⋯) :
      (a : A ⧸ { asIdeal := ⊥.colon {(N₁.mkQ : (a : M) → M ⧸ N₁) x}, isPrime := hx }.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂)

Tactic:
refine ker_eq_bot.mp (ker_liftQ_eq_bot _ _ _ ?_)

Premises used: LinearMap.ker_eq_bot, Submodule.ker_liftQ_eq_bot, Iff.mp
-- 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
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h :
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
x : M
hx :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
⊢ ((N₁.submoduleOf N₂).mkQ ∘ₗ toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂)).ker ≤
    { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
        isPrime := hx }.asIdeal

Tactic:
simp [← Quotient.mk_smul, SetLike.le_def, submoduleOf]

Premises used: SetLike.le_def, Submodule.Quotient.mk_smul, Submodule.submoduleOf
-- 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
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h :
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
x : M
hx :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
refine_2 :
  map (N₁.submoduleOf N₂).mkQ (range (toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂))) = ⊤
⊢ Function.Surjective.{u + 1, v + 1} (α :=
    A ⧸
      { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
          isPrime := hx : PrimeSpectrum A }.asIdeal)
    (β := ↥N₂ ⧸ N₁.submoduleOf N₂)
    (⇑(mapQ
          { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
              isPrime := hx }.asIdeal
          (N₁.submoduleOf N₂) (toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂)) ⋯) :
      (a : A ⧸ { asIdeal := ⊥.colon {(N₁.mkQ : (a : M) → M ⧸ N₁) x}, isPrime := hx }.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂)

Tactic:
rw [mapQ, ← range_eq_top, range_liftQ, range_comp]

Premises used: LinearMap.range_comp, LinearMap.range_eq_top, Submodule.mapQ, Submodule.range_liftQ
-- 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
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h :
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
x : M
hx :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
⊢ N₂.submoduleOf N₂ = (N₁ ⊔ A ∙ x).submoduleOf N₂

Tactic:
have := congr($(hx').submoduleOf N₂)
-- 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
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h :
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
x : M
hx :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
this : ⊤ = (N₁ ⊔ A ∙ x).submoduleOf N₂
⊢ N₁ ≤ N₂

Tactic:
simp_all
-- 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
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h :
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
x : M
hx :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
this : ⊤ = (N₁ ⊔ A ∙ x).submoduleOf N₂
⊢ A ∙ x ≤ N₂

Tactic:
simp_all
-- 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
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h :
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
x : M
hx :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
this : N₂.submoduleOf N₂ = (N₁ ⊔ A ∙ x).submoduleOf N₂
⊢ ⊤ = N₁.submoduleOf N₂ ⊔ A ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂

Tactic:
rw [submoduleOf_self, submoduleOf_sup_of_le (by simp_all) (by simp_all),
        submoduleOf_span_singleton_of_mem _ hxN₂] at this

Premises used: Submodule.submoduleOf_sup_of_le, LinearMap.submoduleOf_span_singleton_of_mem, Submodule.submoduleOf_self
-- 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
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h :
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
x : M
hx :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
this : ⊤ = N₁.submoduleOf N₂ ⊔ A ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂
⊢ map (N₁.submoduleOf N₂).mkQ (range (toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂))) = ⊤

Tactic:
simpa [← span_singleton_eq_range, LinearMap.range_toSpanSingleton] using this.symm

Premises used: LinearMap.range_toSpanSingleton, Submodule.span_singleton_eq_range, Eq.symm
-- 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
⊢ ∃ (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₂}) =
        ⊤

Tactic:
WellFoundedGT.induction_top ⟨⊥, .singleton _ ⊥, rfl, rfl⟩ ?_

Premises used: WellFoundedGT.induction_top
-- 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
refine :
  ∀ (N : Submodule A M),
    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₂}) =
              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
⊢ ∃ (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₂}) =
        ⊤

Tactic:
refine WellFoundedGT.induction_top ⟨⊥, .singleton _ ⊥, rfl, rfl⟩ ?_
-- 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
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
⊢ Nontrivial.{v} (M ⧸ N)

Tactic:
have := Submodule.Quotient.nontrivial_iff.mpr hN
-- 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
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)
obtain :
  ∀ (p : Ideal A) (hp : Membership.mem (γ := Set (Ideal A)) (associatedPrimes.{u, v} A (M ⧸ N)) p),
    ∃ 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
⊢ ∃ 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

Tactic:
obtain ⟨p, hp⟩ := associatedPrimes.nonempty A (M ⧸ N)

Premises used: associatedPrimes.nonempty, HasQuotient.Quotient
-- 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
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)
p : Ideal A
hp : Membership.mem (γ := Set (Ideal A)) (associatedPrimes.{u, v} A (M ⧸ N)) p
⊢ p.IsPrime ∧ ∃ (x : M ⧸ N), p = Submodule.colon (M := M ⧸ N) ⊥ {x}

Tactic:
rw [AssociatedPrimes.mem_iff, isAssociatedPrime_iff] at hp

Premises used: AssociatedPrimes.mem_iff, isAssociatedPrime_iff
-- 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
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)
p : Ideal A
hp : p.IsPrime ∧ ∃ (x : M ⧸ N), p = Submodule.colon (M := M ⧸ N) ⊥ {x}
obtain :
  ∀ (x : M ⧸ N) (hp : Ideal.IsPrime.{u} (α := A) (Submodule.colon (M := M ⧸ N) ⊥ {x})),
    ∃ 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
⊢ ∃ 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

Tactic:
obtain ⟨hp, x, rfl⟩ := hp

Premises used: rfl
-- 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
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 ⧸ N
hp : Ideal.IsPrime.{u} (α := A) (Submodule.colon (M := M ⧸ N) ⊥ {x})
obtain :
  ∀ (x : M)
    (hp :
      Ideal.IsPrime.{u} (α := A)
        (Submodule.colon (M := M ⧸ N) ⊥ (singleton (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) x : M ⧸ 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
⊢ ∃ 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

Tactic:
obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x

Premises used: Submodule.mkQ_surjective, rfl