-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (hypothesis)
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
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)
ih :
  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 • ⊤)
⊢ Exact.{u_3, u_4, u_5} (M := M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (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) (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) • ⊤)
    (⇑((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) • ⊤)
have H₁ : (↑(quotOfListConsSMulTopEquivQuotSMulTopInner M₂ r rs) :
      M₂ ⧸ Ideal.ofList (r :: rs) • ⊤ →ₗ[R] QuotSMulTop r M₂ ⧸ Ideal.ofList 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 =
  (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₁) sorry ∘ₗ
    (↑(quotOfListConsSMulTopEquivQuotSMulTopInner M r rs) :
      M ⧸ Ideal.ofList (r :: rs) • ⊤ →ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs • ⊤)
Tactic: have H₁ := quotOfListConsSMulTopEquivQuotSMulTopInner_naturality r rs f₁