-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rs : List R
h_1 : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K : Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) :=
        torsionBy.{u_1, u_3} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ rs₀ : List R
h₁₂ : rs₁ ~ rs₂
H₁ : rs₀ ++ rs₁ <+~ rs
H₃ : rs₀ ++ rs₂ <+~ rs
h : IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) rs₁
nil :
  ∀ (rs₀ : List R) (H₁ H₃ : rs₀ ++ [] <+~ rs)
    (h :
      IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)
        []),
    IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) []
cons :
  ∀ (r : R) {l₁ l₂ : List R},
    l₁ ~ l₂ →
      ∀
        (ih :
          ∀ (rs₀ : List R) (H₁ : rs₀ ++ l₁ <+~ rs) (H₃ : rs₀ ++ l₂ <+~ rs)
            (h :
              IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₁),
            IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₂)
        (rs₀ : List R) (H₁ : rs₀ ++ r :: l₁ <+~ rs) (H₃ : rs₀ ++ r :: l₂ <+~ rs)
        (h :
          IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)
            (r :: l₁)),
        IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) (r :: l₂)
swap :
  ∀ (a b : R) (t rs₀ : List R) (H₁ : rs₀ ++ b :: a :: t <+~ rs) (H₃ : rs₀ ++ a :: b :: t <+~ rs)
    (h :
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)
        (b :: a :: t)),
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) (a :: b :: t)
trans :
  ∀ {l₁ l₂ l₃ : List R} (h₁₂ : l₁ ~ l₂),
    l₂ ~ l₃ →
      ∀
        (ih₁₂ :
          ∀ (rs₀ : List R) (H₁ : rs₀ ++ l₁ <+~ rs) (H₃ : rs₀ ++ l₂ <+~ rs)
            (h :
              IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₁),
            IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₂)
        (ih₂₃ :
          ∀ (rs₀ : List R) (H₁ : rs₀ ++ l₂ <+~ rs) (H₃ : rs₀ ++ l₃ <+~ rs)
            (h :
              IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₂),
            IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₃)
        (rs₀ : List R) (H₁ : rs₀ ++ l₁ <+~ rs) (H₃ : rs₀ ++ l₃ <+~ rs)
        (h : IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₁),
        IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₃
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) rs₂

Tactic:
{
  induction h₁₂ generalizing rs₀ with
  | nil => exact .nil R _
  | cons r _ ih =>
    let e := quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
    rw [isWeaklyRegular_cons_iff, ← e.isWeaklyRegular_congr] at h ⊢
    refine h.imp_right (ih (r :: rs₀) ?_ ?_) <;>
      exact List.perm_middle.subperm_right.mp ‹_›
  | swap a b t =>
    rw [show ∀ x y z, x :: y :: z = [x, y] ++ z from fun _ _ _ => rfl,
      isWeaklyRegular_append_iff] at h ⊢
    have : Ideal.ofList [b, a] = Ideal.ofList [a, b] :=
      congrArg Ideal.span <| Set.ext fun _ => (List.Perm.swap a b []).mem_iff
    rw [(quotEquivOfEq _ _ (congrArg₂ _ this rfl)).isWeaklyRegular_congr] at h
    rw [List.append_cons, List.append_cons, List.append_assoc _ [b] [a]] at H₁
    apply (List.sublist_append_left (rs₀ ++ [b, a]) _).subperm.trans at H₁
    apply List.perm_append_comm.subperm.trans at H₁
    exact h.imp_left (swap · (h' b a rs₀ H₁))
  | trans h₁₂ _ ih₁₂ ih₂₃ =>
    have H₂ := (h₁₂.append_left rs₀).subperm_right.mp H₁
    exact ih₂₃ rs₀ H₂ H₃ (ih₁₂ rs₀ H₁ H₂ h) }

Premises used: RingTheory.Sequence.isWeaklyRegular_cons_iff, _private.0.RingTheory.Sequence.IsWeaklyRegular.swap, RingTheory.Sequence.IsWeaklyRegular.cons, List.Subperm.trans, RingTheory.Sequence.IsWeaklyRegular.nil, RingTheory.Sequence.isWeaklyRegular_append_iff, List.Perm.subperm, List.perm_append_comm, List.Perm.subperm_right, List.append_cons, Iff.mp, List.perm_middle, rfl