awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂ : List R
r : R
l₁ l₂ : List R
h_2 : 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 :
  IsSMulRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) r ∧
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₀)) ⊤) l₁
e : (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₀)) ⊤) ≃ₗ[R]
  QuotSMulTop r (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) :=
  quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
cons : r :: rs₀ ++ l₁ <+~ rs
cons₁ : r :: rs₀ ++ l₂ <+~ rs
⊢ IsSMulRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) r ∧
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₀)) ⊤) l₂

Tactic:
refine h.imp_right (ih (r :: rs₀) ?_ ?_)

Premises used: List.cons, And.imp_right
-- 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₂ : List R
r : R
l₁ l₂ : List R
h_2 : 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 :
  IsSMulRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) r ∧
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₀)) ⊤) l₁
e : (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₀)) ⊤) ≃ₗ[R]
  QuotSMulTop r (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) :=
  quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
⊢ r :: rs₀ ++ l₁ <+~ rs

Tactic:
List.perm_middle.subperm_right.mp ‹_›

Premises used: List.append, List.Perm.subperm_right, Iff.mp, List.perm_middle
-- 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₂ : List R
r : R
l₁ l₂ : List R
h_2 : 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 :
  IsSMulRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) r ∧
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₀)) ⊤) l₁
e : (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₀)) ⊤) ≃ₗ[R]
  QuotSMulTop r (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) :=
  quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
⊢ r :: rs₀ ++ l₁ <+~ rs

Tactic:
exact List.perm_middle.subperm_right.mp ‹_›

Premises used: List.Perm.subperm_right, Iff.mp, List.perm_middle
-- 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₂ : List R
r : R
l₁ l₂ : List R
h_2 : 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 :
  IsSMulRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) r ∧
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₀)) ⊤) l₁
e : (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₀)) ⊤) ≃ₗ[R]
  QuotSMulTop r (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) :=
  quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
⊢ r :: rs₀ ++ l₂ <+~ rs

Tactic:
List.perm_middle.subperm_right.mp ‹_›

Premises used: List.append, List.Perm.subperm_right, Iff.mp, List.perm_middle
-- 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₂ : List R
r : R
l₁ l₂ : List R
h_2 : 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 :
  IsSMulRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) r ∧
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₀)) ⊤) l₁
e : (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₀)) ⊤) ≃ₗ[R]
  QuotSMulTop r (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) :=
  quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
⊢ r :: rs₀ ++ l₂ <+~ rs

Tactic:
exact List.perm_middle.subperm_right.mp ‹_›

Premises used: List.Perm.subperm_right, Iff.mp, List.perm_middle
-- 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₂ : List R
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)
swap :
  ∀
    (h :
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) [b, a] ∧
        IsWeaklyRegular.{u_1, u_3}
          ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
            HSMul.hSMul (α := Ideal R) (β :=
              Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤))
              (Ideal.ofList [b, a]) ⊤)
          t),
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) [a, b] ∧
      IsWeaklyRegular.{u_1, u_3}
        ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
          HSMul.hSMul (α := Ideal R) (β :=
            Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤))
            (Ideal.ofList [a, b]) ⊤)
        t
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) (a :: b :: t)

Tactic:
rw [show ∀ x y z, x :: y :: z = [x, y] ++ z from fun _ _ _ => rfl,
      isWeaklyRegular_append_iff] at h ⊢

Premises used: RingTheory.Sequence.isWeaklyRegular_append_iff, rfl
-- 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₂ : List R
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] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [b, a])
          ⊤)
      t
⊢ Eq (α := Ideal R) (Ideal.ofList [b, a]) (Ideal.ofList [a, b])

Tactic:
have : Ideal.ofList [b, a] = Ideal.ofList [a, b] :=
      congrArg Ideal.span <| Set.ext fun _ => (List.Perm.swap a b []).mem_iff
-- 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₂ : List R
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] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [b, a])
          ⊤)
      t
this : Eq (α := Ideal R) (Ideal.ofList [b, a]) (Ideal.ofList [a, b])
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) [b, a] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t

Tactic:
rw [(quotEquivOfEq _ _ (congrArg₂ _ this rfl)).isWeaklyRegular_congr] at h

Premises used: congrArg₂, LinearEquiv.isWeaklyRegular_congr, Submodule.quotEquivOfEq, rfl
-- 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₂ : List R
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] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [b, a])
          ⊤)
      t
this : Eq (α := Ideal R) (Ideal.ofList [b, a]) (Ideal.ofList [a, b])
h₁ :
  IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) [b, a] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t
⊢ Eq (α := Ideal R) (Ideal.ofList [b, a]) (Ideal.ofList [a, b])

Tactic:
rw [(quotEquivOfEq _ _ (congrArg₂ _ this rfl)).isWeaklyRegular_congr] at h

Premises used: congrArg₂, LinearEquiv.isWeaklyRegular_congr, Submodule.quotEquivOfEq, rfl
-- 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₂ : List R
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] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t
this : Eq (α := Ideal R) (Ideal.ofList [b, a]) (Ideal.ofList [a, b])
⊢ rs₀ ++ ([b] ++ [a]) ++ t <+~ rs

Tactic:
rw [List.append_cons, List.append_cons, List.append_assoc _ [b] [a]] at H₁

Premises used: List.append_assoc, List.cons, List.append_cons, List.nil
-- 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₂ : List R
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] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t
this : Eq (α := Ideal R) (Ideal.ofList [b, a]) (Ideal.ofList [a, b])
H₂ : rs₀ ++ ([b] ++ [a]) ++ t <+~ rs
⊢ rs₀ ++ a :: b :: t <+~ rs

Tactic:
rw [List.append_cons, List.append_cons, List.append_assoc _ [b] [a]] at H₁

Premises used: List.append_assoc, List.cons, List.append_cons, List.nil
-- 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₂ : List R
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] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t
this : Eq (α := Ideal R) (Ideal.ofList [b, a]) (Ideal.ofList [a, b])
H₂ : rs₀ ++ ([b] ++ [a]) ++ t <+~ rs
H₄ : rs₀ ++ a :: b :: t <+~ rs
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) [b, a] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t

Tactic:
rw [List.append_cons, List.append_cons, List.append_assoc _ [b] [a]] at H₁

Premises used: List.append_assoc, List.cons, List.append_cons, List.nil
-- 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₂ : List R
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] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t
this : Eq (α := Ideal R) (Ideal.ofList [b, a]) (Ideal.ofList [a, b])
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] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t
⊢ Eq (α := Ideal R) (Ideal.ofList [b, a]) (Ideal.ofList [a, b])

Tactic:
rw [List.append_cons, List.append_cons, List.append_assoc _ [b] [a]] at H₁

Premises used: List.append_assoc, List.cons, List.append_cons, List.nil
-- 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₂ : List R
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] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t
this : Eq (α := Ideal R) (Ideal.ofList [b, a]) (Ideal.ofList [a, b])
⊢ rs₀ ++ [b, a] <+~ rs

Tactic:
apply (List.sublist_append_left (rs₀ ++ [b, a]) _).subperm.trans at H₁

Premises used: List.Subperm.trans, List.cons, List.sublist_append_left, List.Sublist.subperm, HAppend.hAppend, List.nil
-- 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₂ : List R
a b : R
t rs₀ : List R
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] ∧
    IsWeaklyRegular.{u_1, u_3}
      ((M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) ⧸
        HSMul.hSMul (α := Ideal R) (β :=
          Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤)) (Ideal.ofList [a, b])
          ⊤)
      t
this : Eq (α := Ideal R) (Ideal.ofList [b, a]) (Ideal.ofList [a, b])
H₁ : rs₀ ++ [b, a] <+~ rs
⊢ [b, a] ++ rs₀ <+~ rs

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

Premises used: List.Subperm.trans, List.Perm.subperm, List.perm_append_comm