-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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 [] • ⊤)
⊢ 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 • ⊤)
have 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₁ sorry) :
              (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₂ sorry) :
              (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₁ sorry) :
          (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₂ sorry) :
          (a : M₂ ⧸ Ideal.ofList (r :: rs) • ⊤) → M₃ ⧸ Ideal.ofList (r :: 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
Cleared hypotheses: M, M₂, M₃, inst_1, inst_2, inst_3, inst_5, inst_6, inst_7, f₁, f₂, f₃, h₁₂, h₂₃, h₃, h₄