awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
a b : R
h2 :
  torsionBy R M b = HSMul.hSMul (β := Submodule R M) a (torsionBy R M b) → Eq (α := Submodule R M) (torsionBy R M b) ⊥
ha : IsSMulRegular M a
hb : IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b
⊢ IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop b M) a
have h2₁ : torsionBy R M b = HSMul.hSMul (β := Submodule R M) a (torsionBy R M b) → IsSMulRegular M b
Tactic: rw [← isSMulRegular_iff_torsionBy_eq_bot] at h2
Cleared hypotheses: h2, ha, hb
-- 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
a b : R
h2 : torsionBy R M b = HSMul.hSMul (β := Submodule R M) a (torsionBy R M b) → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b
⊢ IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop b M) a
have specialize : torsionBy R M b ≤ HSMul.hSMul (β := Submodule R M) a (torsionBy R M b)
Tactic: specialize h2 (le_antisymm ?_ (smul_le_self_of_tower a (torsionBy R M b)))
-- 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
a b : R
h2 : torsionBy R M b = HSMul.hSMul (β := Submodule R M) a (torsionBy R M b) → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b
specialize : torsionBy R M b ≤ HSMul.hSMul (β := Submodule R M) a (torsionBy R M b)
⊢ IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop b M) a
have specialize₁ : ∀ (h2 : IsSMulRegular M b), IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop b M) a
Tactic: specialize h2 (le_antisymm ?_ (smul_le_self_of_tower a (torsionBy R M b)))
Cleared hypotheses: h2
-- 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
a b : R
h2 : torsionBy R M b = HSMul.hSMul (β := Submodule R M) a (torsionBy R M b) → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b
⊢ torsionBy R M b ≤ HSMul.hSMul (β := Submodule R M) a (torsionBy R M b)
have refine : torsionBy R M b = HSMul.hSMul (β := Submodule R M) a ⊤ ⊓ torsionBy R M b
Tactic: refine le_of_eq_of_le ?_ <| smul_top_inf_eq_smul_of_isSMulRegular_on_quot <|
      ha.of_injective _ <| ker_eq_bot.mp <| ker_liftQ_eq_bot' _ (lsmul R M b) rfl
-- 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
a b : R
h2 : torsionBy R M b = HSMul.hSMul (β := Submodule R M) a (torsionBy R M b) → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b
⊢ torsionBy R M b = HSMul.hSMul (β := Submodule R M) a ⊤ ⊓ torsionBy R M b
have rw : Eq (α := Submodule R M) (torsionBy R M b)
  (comap (σ₁₂ := RingHom.id R) ((lsmul R M : (a : R) → M →ₗ[R] M) b) (HSMul.hSMul (β := Submodule R M) a ⊤) ⊓
    torsionBy R M b)
Tactic: rw [← (isSMulRegular_on_quot_iff_lsmul_comap_eq _ _).mp hb]
-- 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
a b : R
ha : IsSMulRegular M a
hb : IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b
h2 : IsSMulRegular M b
⊢ IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop b M) a
have rwa : IsSMulRegular M b ∧
  HSMul.hSMul (β := Submodule R M) a ⊤ ⊓ HSMul.hSMul (β := Submodule R M) b ⊤ ≤ a • HSMul.hSMul (β := Submodule R M) b ⊤
Tactic: rwa [ha.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, inf_comm, smul_comm,
      ← h2.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, and_iff_left hb]
-- 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
a b : R
ha : IsSMulRegular M a
hb : IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b
h2 : IsSMulRegular M b
rwa :
  IsSMulRegular M b ∧
    HSMul.hSMul (β := Submodule R M) a ⊤ ⊓ HSMul.hSMul (β := Submodule R M) b ⊤ ≤
      a • HSMul.hSMul (β := Submodule R M) b ⊤
⊢ IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop b M) a
have rwa₁ : IsSMulRegular M b ∧
  HSMul.hSMul (β := Submodule R M) b ⊤ ⊓ HSMul.hSMul (β := Submodule R M) a ⊤ ≤ a • HSMul.hSMul (β := Submodule R M) b ⊤
Tactic: rwa [ha.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, inf_comm, smul_comm,
      ← h2.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, and_iff_left hb]
-- 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
a b : R
ha : IsSMulRegular M a
hb : IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b
h2 : IsSMulRegular M b
rwa :
  IsSMulRegular M b ∧
    HSMul.hSMul (β := Submodule R M) a ⊤ ⊓ HSMul.hSMul (β := Submodule R M) b ⊤ ≤
      a • HSMul.hSMul (β := Submodule R M) b ⊤
rwa₁ :
  IsSMulRegular M b ∧
    HSMul.hSMul (β := Submodule R M) b ⊤ ⊓ HSMul.hSMul (β := Submodule R M) a ⊤ ≤
      a • HSMul.hSMul (β := Submodule R M) b ⊤
⊢ IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop b M) a
have rwa₂ : IsSMulRegular M b ∧
  HSMul.hSMul (β := Submodule R M) b ⊤ ⊓ HSMul.hSMul (β := Submodule R M) a ⊤ ≤ b • HSMul.hSMul (β := Submodule R M) a ⊤
Tactic: rwa [ha.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, inf_comm, smul_comm,
      ← h2.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, and_iff_left hb]
-- 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
a b : R
ha : IsSMulRegular M a
hb : IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b
h2 : IsSMulRegular M b
rwa :
  IsSMulRegular M b ∧
    HSMul.hSMul (β := Submodule R M) a ⊤ ⊓ HSMul.hSMul (β := Submodule R M) b ⊤ ≤
      a • HSMul.hSMul (β := Submodule R M) b ⊤
rwa₁ :
  IsSMulRegular M b ∧
    HSMul.hSMul (β := Submodule R M) b ⊤ ⊓ HSMul.hSMul (β := Submodule R M) a ⊤ ≤
      a • HSMul.hSMul (β := Submodule R M) b ⊤
rwa₂ :
  IsSMulRegular M b ∧
    HSMul.hSMul (β := Submodule R M) b ⊤ ⊓ HSMul.hSMul (β := Submodule R M) a ⊤ ≤
      b • HSMul.hSMul (β := Submodule R M) a ⊤
⊢ IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop b M) a
have rwa₃ : IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (β := Submodule R M) a ⊤) b
Tactic: rwa [ha.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, inf_comm, smul_comm,
      ← h2.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, and_iff_left hb]
-- 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
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 : IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) (r :: 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₀
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) (r :: l₂)
have cons : ∀
  (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₁),
  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: rw [isWeaklyRegular_cons_iff, ← e.isWeaklyRegular_congr] at h ⊢
Cleared hypotheses: h, e
-- 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
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₀
⊢ 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₂
have cons : r :: rs₀ ++ l₁ <+~ rs
Tactic: refine h.imp_right (ih (r :: rs₀) ?_ ?_)
-- 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
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
⊢ 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₂
have cons₁ : r :: rs₀ ++ l₂ <+~ rs
Tactic: refine h.imp_right (ih (r :: rs₀) ?_ ?_)
-- 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
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)
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) (a :: b :: t)
have 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
Tactic: rw [show ∀ x y z, x :: y :: z = [x, y] ++ z from fun _ _ _ => rfl,
      isWeaklyRegular_append_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (hypothesis)
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
⊢ 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
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (hypothesis)
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₀) ⊤) [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
have 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
Tactic: rw [(quotEquivOfEq _ _ (congrArg₂ _ this rfl)).isWeaklyRegular_congr] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (hypothesis)
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])
⊢ 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
have H₂ : rs₀ ++ ([b] ++ [a]) ++ t <+~ rs
Tactic: rw [List.append_cons, List.append_cons, List.append_assoc _ [b] [a]] at H₁
Cleared hypotheses: H₁, H₃, h, this
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (hypothesis)
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])
⊢ 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
have H₂ : rs₀ ++ [b, a] <+~ rs
Tactic: apply (List.sublist_append_left (rs₀ ++ [b, a]) _).subperm.trans at H₁
Cleared hypotheses: H₁
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (hypothesis)
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
⊢ 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
have H₂ : [b, a] ++ rs₀ <+~ rs
Tactic: apply List.perm_append_comm.subperm.trans at H₁
Cleared hypotheses: H₁
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (hypothesis)
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₂ l₁ l₂ l₃ : List R
h₁₂ : l₁ ~ l₂
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₂
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₃
have H₂ : rs₀ ++ l₂ <+~ rs
Tactic: have H₂ := (h₁₂.append_left rs₀).subperm_right.mp H₁