awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  IsWeaklyRegular M (r :: rs) ∧ ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    IsSMulRegular M r ∧ IsRegular.{u_1, u_3} (QuotSMulTop r M) rs
rw₁ :
  IsWeaklyRegular M (r :: rs) ∧ ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs ∧
        ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
rw₂ :
  (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs) ∧
      ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs ∧
        ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
rw₃ :
  (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs) ∧
      ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs ∧
        ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
rw₄ :
  (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs) ∧
      ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs ∧
        ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
⊢ IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsRegular.{u_1, u_3} (QuotSMulTop r M) rs
have rw₅ : IsSMulRegular M r ∧
    IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs ∧
      ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤ ↔
  IsSMulRegular M r ∧
    IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs ∧
      ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
Tactic: rw [isRegular_iff, isRegular_iff, isWeaklyRegular_cons_iff M r rs,
    ne_eq, top_eq_ofList_cons_smul_iff, and_assoc]
-- 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
| IsRegular M (r :: rs) ↔
    IsSMulRegular M r ∧
      IsRegular.{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)
have a : IsRegular M (r :: rs)
Tactic: congr
-- 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
a : IsRegular M (r :: rs)
| IsRegular M (r :: rs) ↔
    IsSMulRegular M r ∧
      IsRegular.{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)
have b : IsSMulRegular M r ∧
  IsRegular.{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)
Tactic: congr
-- 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
| IsRegular M (r :: rs)
have a : IsWeaklyRegular M (r :: rs) ∧ ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤
Tactic: rw [isRegular_iff, ne_eq]
-- 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
| IsSMulRegular M r ∧
    IsRegular.{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)
have b : 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)) ⊤
Tactic: rw [isRegular_iff, ne_eq]
-- 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
| IsRegular M (r :: rs) ↔
    IsSMulRegular M r ∧
      IsRegular.{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)
have a : IsWeaklyRegular M (r :: rs) ∧ ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤
Tactic: congr <;> rw [isRegular_iff, ne_eq]
-- 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
a : IsWeaklyRegular M (r :: rs) ∧ ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤
| IsRegular M (r :: rs) ↔
    IsSMulRegular M r ∧
      IsRegular.{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)
have b : 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)) ⊤
Tactic: congr <;> rw [isRegular_iff, ne_eq]
-- 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
⊢ IsRegular M (r :: rs) ↔
    IsSMulRegular M r ∧
      IsRegular.{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)
have conv : 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)) ⊤
Tactic: conv => congr <;> rw [isRegular_iff, ne_eq]
-- 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
⊢ 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 (⇑(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)) ⊤
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]
-- 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)) ⊤
⊢ 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 (⇑(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)) ⊤))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
inst : CommRing R
rs₂ : List R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ IsWeaklyRegular M ([] ++ rs₂) ↔
    IsWeaklyRegular.{u_1, u_3} (R := R) M [] ∧
      IsWeaklyRegular.{u_1, u_3}
        (M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤) rs₂
have nil : IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤)
    rs₂ ↔
  IsWeaklyRegular M ([] ++ rs₂)
Tactic: refine Iff.symm <| Iff.trans (and_iff_right (.nil R M)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
inst : CommRing R
rs₂ : List R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤)
      rs₂ ↔
    IsWeaklyRegular M ([] ++ rs₂)
have nil : HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤ = ⊥
Tactic: refine (quotEquivOfEqBot _ ?_).isWeaklyRegular_congr rs₂
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
inst : CommRing R
rs₂ : List R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤ = ⊥
have nil : HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) ⊥ ⊤ = ⊥
Tactic: rw [Ideal.ofList_nil, bot_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
inst : CommRing R
rs₂ : List R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
nil : HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) ⊥ ⊤ = ⊥
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤ = ⊥
have nil₁ : Eq.{u_3 + 1} (α := Submodule R M) ⊥ ⊥
Tactic: rw [Ideal.ofList_nil, bot_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
inst : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst_3 : AddCommGroup M] [inst_4 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔
      IsWeaklyRegular M rs₁ ∧
        IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₁) ⊤) rs₂
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
e : (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) ≃ₗ[R]
  QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs₁) ⊤ :=
  quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
⊢ IsWeaklyRegular M (r :: rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
have cons : IsWeaklyRegular M (r :: (rs₁ ++ rs₂)) ↔
  IsWeaklyRegular M (r :: rs₁) ∧
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
Tactic: rw [List.cons_append, isWeaklyRegular_cons_iff, isWeaklyRegular_cons_iff,
      ih, ← and_assoc, ← e.isWeaklyRegular_congr rs₂]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
inst : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst_3 : AddCommGroup M] [inst_4 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔
      IsWeaklyRegular M rs₁ ∧
        IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₁) ⊤) rs₂
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
e : (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) ≃ₗ[R]
  QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs₁) ⊤ :=
  quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
cons :
  IsWeaklyRegular M (r :: (rs₁ ++ rs₂)) ↔
    IsWeaklyRegular M (r :: rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
⊢ IsWeaklyRegular M (r :: rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
have cons₁ : IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) (rs₁ ++ rs₂) ↔
  IsWeaklyRegular M (r :: rs₁) ∧
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
Tactic: rw [List.cons_append, isWeaklyRegular_cons_iff, isWeaklyRegular_cons_iff,
      ih, ← and_assoc, ← e.isWeaklyRegular_congr rs₂]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
inst : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst_3 : AddCommGroup M] [inst_4 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔
      IsWeaklyRegular M rs₁ ∧
        IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₁) ⊤) rs₂
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
e : (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) ≃ₗ[R]
  QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs₁) ⊤ :=
  quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
cons :
  IsWeaklyRegular M (r :: (rs₁ ++ rs₂)) ↔
    IsWeaklyRegular M (r :: rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
cons₁ :
  IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) (rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
⊢ IsWeaklyRegular M (r :: rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
have cons₂ : IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) (rs₁ ++ rs₂) ↔
  (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs₁) ∧
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
Tactic: rw [List.cons_append, isWeaklyRegular_cons_iff, isWeaklyRegular_cons_iff,
      ih, ← and_assoc, ← e.isWeaklyRegular_congr rs₂]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
inst : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst_3 : AddCommGroup M] [inst_4 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔
      IsWeaklyRegular M rs₁ ∧
        IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₁) ⊤) rs₂
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
e : (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) ≃ₗ[R]
  QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs₁) ⊤ :=
  quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
cons :
  IsWeaklyRegular M (r :: (rs₁ ++ rs₂)) ↔
    IsWeaklyRegular M (r :: rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
cons₁ :
  IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) (rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
cons₂ :
  IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) (rs₁ ++ rs₂) ↔
    (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
⊢ IsWeaklyRegular M (r :: rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
have cons₃ : IsSMulRegular M r ∧
    IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs₁ ∧
      IsWeaklyRegular.{u_1, u_3}
        (QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs₁) ⊤) rs₂ ↔
  (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs₁) ∧
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
Tactic: rw [List.cons_append, isWeaklyRegular_cons_iff, isWeaklyRegular_cons_iff,
      ih, ← and_assoc, ← e.isWeaklyRegular_congr rs₂]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
inst : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst_3 : AddCommGroup M] [inst_4 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔
      IsWeaklyRegular M rs₁ ∧
        IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₁) ⊤) rs₂
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
e : (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) ≃ₗ[R]
  QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs₁) ⊤ :=
  quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
cons :
  IsWeaklyRegular M (r :: (rs₁ ++ rs₂)) ↔
    IsWeaklyRegular M (r :: rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
cons₁ :
  IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) (rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
cons₂ :
  IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) (rs₁ ++ rs₂) ↔
    (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
cons₃ :
  IsSMulRegular M r ∧
      IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs₁ ∧
        IsWeaklyRegular.{u_1, u_3}
          (QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs₁) ⊤) rs₂ ↔
    (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
⊢ IsWeaklyRegular M (r :: rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
have cons₄ : (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs₁) ∧
    IsWeaklyRegular.{u_1, u_3}
      (QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs₁) ⊤) rs₂ ↔
  (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs₁) ∧
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₁)) ⊤) rs₂
Tactic: rw [List.cons_append, isWeaklyRegular_cons_iff, isWeaklyRegular_cons_iff,
      ih, ← and_assoc, ← e.isWeaklyRegular_congr rs₂]