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
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 (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) x : M ⧸ N) (0 : M ⧸ N)

Tactic:
simpa
-- 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
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
rw : Eq.{u + 1} (α := Ideal A) (Submodule.colon (M := M ⧸ N) ⊥ {0}) ⊤
⊢ Eq.{u + 1} (α := Ideal A)
    (Submodule.colon (M := M ⧸ N) ⊥ (singleton (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) x : M ⧸ N))) ⊤

Tactic:
rw [show N.mkQ x = 0 by simpa]
-- 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
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) ⊥ {0}) ⊤

Tactic:
simp
-- 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
hp :
  Ideal.IsPrime.{u} (α := A)
    (Submodule.colon (M := M ⧸ N) ⊥ (singleton (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) x : M ⧸ N)))
⊢ x ∉ N

Tactic:
have hxN : x ∉ N := fun h ↦ hp.ne_top (by rw [show N.mkQ x = 0 by simpa]; simp)
-- 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
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
⊢ N.IsQuotientEquivQuotientPrime (N ⊔ A ∙ x)

Tactic:
have := Submodule.isQuotientEquivQuotientPrime_iff.mpr ⟨x, hp, 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_1 : 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
this : N.IsQuotientEquivQuotientPrime (N ⊔ A ∙ x)
⊢ (s.snoc (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₂}) ⊔
            A ∙ x)
          ⋯).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

Tactic:
simpa [hs₂]
-- 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_1 : 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
this : N.IsQuotientEquivQuotientPrime (N ⊔ A ∙ x)
⊢ (s.snoc (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₂}) ⊔
            A ∙ x)
          ⋯).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:
simpa
-- 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_1 : 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
this : N.IsQuotientEquivQuotientPrime (N ⊔ A ∙ 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:
refine ⟨_, by simpa [hs₂], s.snoc _ (hs₂ ▸ this), by simpa, rfl⟩
-- 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₂
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
⊢ 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 _)
-- 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₂
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
⊢ motive M

Tactic:
obtain ⟨s, hs1, hs2⟩ := IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime A M

Premises used: IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime
-- 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 :
  ∀ (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
    ↥(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:
replace H : motive s.last := H s.length s.length.lt_add_one
-- 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
    ↥(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 ↥⊤

Tactic:
rw [hs2] at 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 : 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:
equiv _ _ Submodule.topEquiv H

Premises used: Submodule.topEquiv