-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
rs : List R
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M₄
h₁₂ : Exact.{u_3, u_4, u_5} (M := M) (N := M₂) (P := M₃) (⇑f₁ : (a : M) → M₂) (⇑f₂ : (a : M₂) → M₃)
h₂₃ : Exact.{u_4, u_5, u_6} (M := M₂) (N := M₃) (P := M₄) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M₄)
h₃ : Surjective.{u_5 + 1, u_6 + 1} (α := M₃) (β := M₄) (⇑f₃ : (a : M₃) → M₄)
h₄ : IsWeaklyRegular M₄ rs
nil :
  ∀ (M : Type u_6) [inst_9 : AddCommGroup M] [inst_10 : Module R M] {M_1 : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5}
    [inst_11 : AddCommGroup M_1] [inst_12 : AddCommGroup M₂] [inst_13 : AddCommGroup M₃] [inst_14 : Module R M_1]
    [inst_15 : Module R M₂] [inst_16 : Module R M₃] {f₁ : M_1 →ₗ[R] M₂} {f₂ : M₂ →ₗ[R] M₃} {f₃ : M₃ →ₗ[R] M}
    (h₁₂ : Exact.{u_3, u_4, u_5} (M := M_1) (N := M₂) (P := M₃) (⇑f₁ : (a : M_1) → M₂) (⇑f₂ : (a : M₂) → M₃))
    (h₂₃ : Exact.{u_4, u_5, u_6} (M := M₂) (N := M₃) (P := M) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M))
    (h₃ : Surjective.{u_5 + 1, u_6 + 1} (α := M₃) (β := M) (⇑f₃ : (a : M₃) → M)),
    Exact.{u_3, u_4, u_5} (M :=
      M_1 ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M_1) (Ideal.ofList []) ⊤) (N :=
      M₂ ⧸ HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) (P :=
      M₃ ⧸ HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤)
      (⇑((HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M_1) (Ideal.ofList []) ⊤).mapQ
            (HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) f₁ ⋯) :
        (a : M_1 ⧸ Ideal.ofList [] • ⊤) → M₂ ⧸ Ideal.ofList [] • ⊤)
      (⇑((HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤).mapQ
            (HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤) f₂ ⋯) :
        (a : M₂ ⧸ Ideal.ofList [] • ⊤) → M₃ ⧸ Ideal.ofList [] • ⊤)
cons :
  ∀ {M : Type u_6} [inst_9 : AddCommGroup M] [inst_10 : Module R M] (r : R) (rs : List R) (h₄ : IsSMulRegular M r),
    IsWeaklyRegular.{u_1, u_6} (QuotSMulTop r M) rs →
      ∀
        (ih :
          ∀ {M_1 : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [inst_11 : AddCommGroup M_1] [inst_12 : AddCommGroup M₂]
            [inst_13 : AddCommGroup M₃] [inst_14 : Module R M_1] [inst_15 : Module R M₂] [inst_16 : Module R M₃]
            {f₁ : M_1 →ₗ[R] M₂} {f₂ : M₂ →ₗ[R] M₃}
            {f₃ : LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) M₃ (QuotSMulTop r M)}
            (h₁₂ : Exact.{u_3, u_4, u_5} (M := M_1) (N := M₂) (P := M₃) (⇑f₁ : (a : M_1) → M₂) (⇑f₂ : (a : M₂) → M₃))
            (h₂₃ :
              Exact.{u_4, u_5, u_6} (M := M₂) (N := M₃) (P := QuotSMulTop r M) (⇑f₂ : (a : M₂) → M₃)
                (⇑f₃ : (a : M₃) → QuotSMulTop r M))
            (h₃ : Surjective.{u_5 + 1, u_6 + 1} (α := M₃) (β := QuotSMulTop r M) (⇑f₃ : (a : M₃) → QuotSMulTop r M)),
            Exact.{u_3, u_4, u_5} (M := M_1 ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M_1) (Ideal.ofList rs) ⊤)
              (N := M₂ ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList rs) ⊤) (P :=
              M₃ ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList rs) ⊤)
              (⇑((HSMul.hSMul (α := Ideal R) (β := Submodule R M_1) (Ideal.ofList rs) ⊤).mapQ
                    (HSMul.hSMul (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList rs) ⊤) f₁ ⋯) :
                (a : M_1 ⧸ Ideal.ofList rs • ⊤) → M₂ ⧸ Ideal.ofList rs • ⊤)
              (⇑((HSMul.hSMul (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList rs) ⊤).mapQ
                    (HSMul.hSMul (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList rs) ⊤) f₂ ⋯) :
                (a : M₂ ⧸ Ideal.ofList rs • ⊤) → M₃ ⧸ Ideal.ofList rs • ⊤))
        {M_1 : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [inst_11 : AddCommGroup M_1] [inst_12 : AddCommGroup M₂]
        [inst_13 : AddCommGroup M₃] [inst_14 : Module R M_1] [inst_15 : Module R M₂] [inst_16 : Module R M₃]
        {f₁ : M_1 →ₗ[R] M₂} {f₂ : M₂ →ₗ[R] M₃} {f₃ : M₃ →ₗ[R] M}
        (h₁₂ : Exact.{u_3, u_4, u_5} (M := M_1) (N := M₂) (P := M₃) (⇑f₁ : (a : M_1) → M₂) (⇑f₂ : (a : M₂) → M₃))
        (h₂₃ : Exact.{u_4, u_5, u_6} (M := M₂) (N := M₃) (P := M) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M))
        (h₃ : Surjective.{u_5 + 1, u_6 + 1} (α := M₃) (β := M) (⇑f₃ : (a : M₃) → M)),
        Exact.{u_3, u_4, u_5} (M := M_1 ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M_1) (Ideal.ofList (r :: rs)) ⊤)
          (N := M₂ ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList (r :: rs)) ⊤) (P :=
          M₃ ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList (r :: rs)) ⊤)
          (⇑((HSMul.hSMul (α := Ideal R) (β := Submodule R M_1) (Ideal.ofList (r :: rs)) ⊤).mapQ
                (HSMul.hSMul (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList (r :: rs)) ⊤) f₁ ⋯) :
            (a : M_1 ⧸ Ideal.ofList (r :: rs) • ⊤) → M₂ ⧸ Ideal.ofList (r :: rs) • ⊤)
          (⇑((HSMul.hSMul (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList (r :: rs)) ⊤).mapQ
                (HSMul.hSMul (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList (r :: rs)) ⊤) f₂ ⋯) :
            (a : M₂ ⧸ Ideal.ofList (r :: rs) • ⊤) → M₃ ⧸ Ideal.ofList (r :: rs) • ⊤)
⊢ Exact.{u_3, u_4, u_5} (M := M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤) (N :=
    M₂ ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList rs) ⊤) (P :=
    M₃ ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList rs) ⊤)
    (⇑((HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs) ⊤).mapQ
          (HSMul.hSMul (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList rs) ⊤) f₁ ⋯) :
      (a : M ⧸ Ideal.ofList rs • ⊤) → M₂ ⧸ Ideal.ofList rs • ⊤)
    (⇑((HSMul.hSMul (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList rs) ⊤).mapQ
          (HSMul.hSMul (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList rs) ⊤) f₂ ⋯) :
      (a : M₂ ⧸ Ideal.ofList rs • ⊤) → M₃ ⧸ Ideal.ofList rs • ⊤)

Tactic:
induction h₄ generalizing M M₂ M₃ with
  | nil =>
    apply (Exact.iff_of_ladder_linearEquiv ?_ ?_).mp h₁₂
    any_goals exact quotEquivOfEqBot _ <|
      Eq.trans (congrArg (· • ⊤) Ideal.ofList_nil) (bot_smul ⊤)
    all_goals exact quot_hom_ext _ _ _ fun _ => rfl
  | cons r rs h₄ _ ih =>
    specialize ih
      (map_first_exact_on_four_term_exact_of_isSMulRegular_last h₁₂ h₂₃ h₄)
      (map_exact r h₂₃ h₃) (map_surjective r h₃)
    have H₁ := quotOfListConsSMulTopEquivQuotSMulTopInner_naturality r rs f₁
    have H₂ := quotOfListConsSMulTopEquivQuotSMulTopInner_naturality r rs f₂
    exact (Exact.iff_of_ladder_linearEquiv H₁.symm H₂.symm).mp ih

Premises used: Function.Exact.iff_of_ladder_linearEquiv, congrArg, Submodule.bot_smul, Submodule.quotEquivOfEqBot, Ideal.ofList_nil, Iff.mp, HSMul.hSMul, Top.top, rfl, Eq.trans, Submodule.quot_hom_ext