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

Tactic:
specialize ih
      (map_first_exact_on_four_term_exact_of_isSMulRegular_last h₁₂ h₂₃ h₄)
      (map_exact r h₂₃ h₃) (map_surjective r h₃)

Premises used: QuotSMulTop.map_surjective, QuotSMulTop.map_exact, QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last