awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 :
  { 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₂)
refine_2₁ :
  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₂)
⊢ Nonempty
    (LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂)
      (A ⧸
        { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
            isPrime := hx : PrimeSpectrum A }.asIdeal))
have refine_2₂ : 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₂)) sorry) :
    (a : A ⧸ { asIdeal := ⊥.colon {(N₁.mkQ : (a : M) → M ⧸ N₁) x}, isPrime := hx }.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂)
Tactic: refine ⟨.symm (.ofBijective (Submodule.mapQ _ _ (toSpanSingleton A _ ⟨x, hxN₂⟩) ?_) ⟨?_, ?_⟩)⟩
-- 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
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₂)
have 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
Tactic: refine ker_eq_bot.mp (ker_liftQ_eq_bot _ _ _ ?_)
-- 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
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.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₂)
have refine_2 : map (N₁.submoduleOf N₂).mkQ (range (toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂))) = ⊤
Tactic: rw [mapQ, ← range_eq_top, range_liftQ, range_comp]
-- 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
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₂
⊢ map (N₁.submoduleOf N₂).mkQ (range (toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂))) = ⊤
have this : N₂.submoduleOf N₂ = (N₁ ⊔ A ∙ x).submoduleOf N₂
Tactic: have := congr($(hx').submoduleOf N₂)
-- 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
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₂
⊢ map (N₁.submoduleOf N₂).mkQ (range (toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂))) = ⊤
have this₁ : ⊤ = 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
Cleared hypotheses: this
-- 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 : 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₂}) =
        ⊤
have 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
Tactic: refine WellFoundedGT.induction_top ⟨⊥, .singleton _ ⊥, rfl, rfl⟩ ?_
-- 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
⊢ ∃ 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 : Nontrivial.{v} (M ⧸ N)
Tactic: have := Submodule.Quotient.nontrivial_iff.mpr hN
-- 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 : 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)
⊢ ∃ 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 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
Tactic: obtain ⟨p, hp⟩ := associatedPrimes.nonempty A (M ⧸ N)
-- 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)
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
have hp₁ : p.IsPrime ∧ ∃ (x : M ⧸ N), p = Submodule.colon (M := M ⧸ N) ⊥ {x}
Tactic: rw [AssociatedPrimes.mem_iff, isAssociatedPrime_iff] at hp
Cleared hypotheses: hp
-- 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 : 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}
⊢ ∃ 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 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
Tactic: obtain ⟨hp, x, rfl⟩ := hp
Cleared hypotheses: p, hp
-- 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 : 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})
⊢ ∃ 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 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
Tactic: obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
Cleared hypotheses: x, hp
-- 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 : 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)))
h : x ∈ N
⊢ Eq.{u + 1} (α := Ideal A)
    (Submodule.colon (M := M ⧸ N) ⊥ (singleton (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) x : M ⧸ N))) ⊤
have rw : Eq.{u + 1} (α := Ideal A) (Submodule.colon (M := M ⧸ N) ⊥ {0}) ⊤
Tactic: rw [show N.mkQ x = 0 by simpa]
-- 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)))
⊢ ∃ 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 hxN : x ∉ N
Tactic: have hxN : x ∉ N := fun h ↦ hp.ne_top (by rw [show N.mkQ x = 0 by simpa]; simp)