-- 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₂}) =
    ⊤
n : ℕ
h :
  n + 1 <
    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
hle :
  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, ⋯⟩ :
          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₂}))).castSucc ≤
    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, ⋯⟩.succ
p : PrimeSpectrum A
f :
  LinearEquiv.{u, u, v, u} (RingHom.id A)
    (HasQuotient.Quotient
      ↥(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, ⋯⟩ :
              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₂}))).succ)
      (B :=
      Submodule A
        ↥(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, ⋯⟩ :
                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₂}))).succ))
      ((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, ⋯⟩.castSucc).submoduleOf
        (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, ⋯⟩.succ)))
    (A ⧸ p.asIdeal)
ih :
  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, ⋯⟩.castSucc).submoduleOf
        (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, ⋯⟩.succ))
⊢ 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 + 1, 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:
exact _ _ _ _ _ (Submodule.injective_subtype _) (Submodule.mkQ_surjective _)
      (LinearMap.exact_subtype_mkQ _) ih (quotient _ p f)

Premises used: LinearMap.exact_subtype_mkQ, Submodule.injective_subtype, Submodule.mkQ_surjective