-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
rs : List R
rw :
  (IsSMulRegular M r ∧
        IsWeaklyRegular.{u_1, u_3} (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M)
          (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r})) : (a : R) → R ⧸ Ideal.span {r}) rs)) ∧
      ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular.{u_1, u_3} (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M)
          (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r})) : (a : R) → R ⧸ Ideal.span {r}) rs) ∧
        ¬⊤ =
            HSMul.hSMul (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))) (β :=
              Submodule.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M))
              (Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r})) : (a : R) → R ⧸ Ideal.span {r}) rs)) ⊤
rw₁ :
  (IsSMulRegular M r ∧
        IsWeaklyRegular.{u_1, u_3} (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M)
          (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r})) : (a : R) → R ⧸ Ideal.span {r}) rs)) ∧
      ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular.{u_1, u_3} (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M)
          (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r})) : (a : R) → R ⧸ Ideal.span {r}) rs) ∧
        ¬Eq (α := Submodule R (QuotSMulTop r M))
            (restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) ⊤)
            (restrictScalars R
              (HSMul.hSMul (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))) (β :=
                Submodule.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M))
                (Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r})) : (a : R) → R ⧸ Ideal.span {r}) rs)) ⊤))
rw₂ :
  (IsSMulRegular M r ∧
        IsWeaklyRegular.{u_1, u_3} (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M)
          (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r})) : (a : R) → R ⧸ Ideal.span {r}) rs)) ∧
      ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular.{u_1, u_3} (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M)
          (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r})) : (a : R) → R ⧸ Ideal.span {r}) rs) ∧
        ¬Eq (α := Submodule R (QuotSMulTop r M))
            (restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) ⊤)
            (restrictScalars R
              (HSMul.hSMul (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))) (β :=
                Submodule.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M))
                (Ideal.map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
                  (Ideal.Quotient.mk (Ideal.span {r})) (Ideal.ofList rs))
                ⊤))
rw₃ :
  (IsSMulRegular M r ∧
        IsWeaklyRegular.{u_1, u_3} (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M)
          (List.map
            (⇑(algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) :
                  R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) :
              (a : R) → R ⧸ Ideal.span {r})
            rs)) ∧
      ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular.{u_1, u_3} (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M)
          (List.map
            (⇑(algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) :
                  R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) :
              (a : R) → R ⧸ Ideal.span {r})
            rs) ∧
        ¬Eq (α := Submodule R (QuotSMulTop r M))
            (restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) ⊤)
            (restrictScalars R
              (HSMul.hSMul (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))) (β :=
                Submodule.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M))
                (Ideal.map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
                  (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))) (Ideal.ofList rs))
                ⊤))
⊢ IsWeaklyRegular M (r :: rs) ∧ ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular.{u_1, u_3} (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M)
          (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r})) : (a : R) → R ⧸ Ideal.span {r}) rs) ∧
        ¬⊤ =
            HSMul.hSMul (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))) (β :=
              Submodule.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M))
              (Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r})) : (a : R) → R ⧸ Ideal.span {r}) rs)) ⊤
have rw₄ : (IsSMulRegular M r ∧
      IsWeaklyRegular.{u_1, u_3} (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M)
        (List.map
          (⇑(algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) :
                R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) :
            (a : R) → R ⧸ Ideal.span {r})
          rs)) ∧
    ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
  IsSMulRegular M r ∧
    IsWeaklyRegular.{u_1, u_3} (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) (QuotSMulTop r M)
        (List.map
          (⇑(algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) :
                R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) :
            (a : R) → R ⧸ Ideal.span {r})
          rs) ∧
      ¬restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) ⊤ =
          HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs)
            (restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) ⊤)
Tactic: rw [isWeaklyRegular_cons_iff', ← restrictScalars_inj R (R ⧸ _),
    ← Ideal.map_ofList, ← Ideal.Quotient.algebraMap_eq, Ideal.smul_restrictScalars,
    restrictScalars_top, top_eq_ofList_cons_smul_iff, and_assoc]