-- Mathlib/RingTheory/Regular/RegularSequence.lean
lemma IsWeaklyRegular.prototype_perm {rs : List R} (h : IsWeaklyRegular M rs)
    {rs'} (h'' : rs ~ rs') (h' : ∀ a b rs', (a :: b :: rs') <+~ rs →
      let K := torsionBy R (M ⧸ (Ideal.ofList rs' • ⊤ : Submodule R M)) b
      K = a • K → K = ⊥) : IsWeaklyRegular M rs' :=
  have H := LinearEquiv.isWeaklyRegular_congr <| quotEquivOfEqBot _ <|
    Eq.trans (congrArg (· • ⊤) Ideal.ofList_nil) (bot_smul ⊤)
  (H rs').mp <| (aux [] h'' (.refl rs) (h''.symm.subperm)) <| (H rs).mpr h
  where aux {rs₁ rs₂} (rs₀ : List R)
    (h₁₂ : rs₁ ~ rs₂) (H₁ : rs₀ ++ rs₁ <+~ rs) (H₃ : rs₀ ++ rs₂ <+~ rs)
    (h : IsWeaklyRegular (M ⧸ (Ideal.ofList rs₀ • ⊤ : Submodule R M)) rs₁) :
    IsWeaklyRegular (M ⧸ (Ideal.ofList rs₀ • ⊤ : Submodule R M)) rs₂

Proof state:
case trans
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ l₁✝ l₂✝ l₃✝ : List R
h₁₂ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁₂ :
  ∀ (rs₀ : List R),
    rs₀ ++ l₁✝ <+~ rs →
      rs₀ ++ l₂✝ <+~ rs →
        IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₁✝ → IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₂✝
ih₂₃ :
  ∀ (rs₀ : List R),
    rs₀ ++ l₂✝ <+~ rs →
      rs₀ ++ l₃✝ <+~ rs →
        IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₂✝ → IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₃✝
rs₀ : List R
H₁ : rs₀ ++ l₁✝ <+~ rs
H₃ : rs₀ ++ l₃✝ <+~ rs
h : IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₁✝
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₃✝

Tactic:
have H₂ := (h₁₂.append_left rs₀).subperm_right.mp H₁

Result:
case trans
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ l₁✝ l₂✝ l₃✝ : List R
h₁₂ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁₂ :
  ∀ (rs₀ : List R),
    rs₀ ++ l₁✝ <+~ rs →
      rs₀ ++ l₂✝ <+~ rs →
        IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₁✝ → IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₂✝
ih₂₃ :
  ∀ (rs₀ : List R),
    rs₀ ++ l₂✝ <+~ rs →
      rs₀ ++ l₃✝ <+~ rs →
        IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₂✝ → IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₃✝
rs₀ : List R
H₁ : rs₀ ++ l₁✝ <+~ rs
H₃ : rs₀ ++ l₃✝ <+~ rs
h : IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₁✝
H₂ : rs₀ ++ l₂✝ <+~ rs
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₃✝

Proof state:
case swap
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ : List R
a b : R
t rs₀ : List R
H₃ : rs₀ ++ a :: b :: t <+~ rs
h :
  IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) [b, a] ∧
    IsWeaklyRegular ((M ⧸ Ideal.ofList rs₀ • ⊤) ⧸ Ideal.ofList [a, b] • ⊤) t
this : Ideal.ofList [b, a] = Ideal.ofList [a, b]
H₁ : rs₀ ++ [b, a] <+~ rs
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) [a, b] ∧
    IsWeaklyRegular ((M ⧸ Ideal.ofList rs₀ • ⊤) ⧸ Ideal.ofList [a, b] • ⊤) t

Tactic:
apply List.perm_append_comm.subperm.trans at H₁

Result:
case swap
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ : List R
a b : R
t rs₀ : List R
H₃ : rs₀ ++ a :: b :: t <+~ rs
h :
  IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) [b, a] ∧
    IsWeaklyRegular ((M ⧸ Ideal.ofList rs₀ • ⊤) ⧸ Ideal.ofList [a, b] • ⊤) t
this : Ideal.ofList [b, a] = Ideal.ofList [a, b]
H₁ : [b, a] ++ rs₀ <+~ rs
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) [a, b] ∧
    IsWeaklyRegular ((M ⧸ Ideal.ofList rs₀ • ⊤) ⧸ Ideal.ofList [a, b] • ⊤) t