awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
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} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: 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
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rs₁ rs₂ : List R
⊢ IsWeaklyRegular M (rs₁ ++ rs₂) ↔
    IsWeaklyRegular M rs₁ ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₁) ⊤) rs₂
have nil : ∀ (M : Type u_3) [inst_3 : AddCommGroup M] [inst_4 : 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₂
Tactic: induction rs₁ generalizing M with
  | nil =>
    refine Iff.symm <| Iff.trans (and_iff_right (.nil R M)) ?_
    refine (quotEquivOfEqBot _ ?_).isWeaklyRegular_congr rs₂
    rw [Ideal.ofList_nil, bot_smul]
  | cons r rs₁ ih =>
    let e := quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
    rw [List.cons_append, isWeaklyRegular_cons_iff, isWeaklyRegular_cons_iff,
      ih, ← and_assoc, ← e.isWeaklyRegular_congr rs₂]
Cleared hypotheses: M, inst_1, inst_2, 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₁ rs₂ : List R
nil :
  ∀ (M : Type u_3) [inst_3 : AddCommGroup M] [inst_4 : 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₂
⊢ IsWeaklyRegular M (rs₁ ++ rs₂) ↔
    IsWeaklyRegular M rs₁ ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₁) ⊤) rs₂
have cons : ∀ (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_3 : AddCommGroup M] [inst_4 : Module R M],
  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: induction rs₁ generalizing M with
  | nil =>
    refine Iff.symm <| Iff.trans (and_iff_right (.nil R M)) ?_
    refine (quotEquivOfEqBot _ ?_).isWeaklyRegular_congr rs₂
    rw [Ideal.ofList_nil, bot_smul]
  | cons r rs₁ ih =>
    let e := quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
    rw [List.cons_append, isWeaklyRegular_cons_iff, isWeaklyRegular_cons_iff,
      ih, ← and_assoc, ← e.isWeaklyRegular_congr rs₂]
Cleared hypotheses: M, inst_1, inst_2, rs₁
-- 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
inst_3 : Nontrivial M
h : ⊤ = HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤
⊢ False
have h₁ : Subsingleton.{u_3 + 1} (Submodule R M)
Tactic: rw [Ideal.ofList_nil, bot_smul, eq_comm, subsingleton_iff_bot_eq_top] 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
inst_3 : IsArtinian R M
r : R
rs : List R
h : IsRegular M (r :: rs)
⊢ r :: rs = []
have h₁ : (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs) ∧
  HSMul.hSMul (β := Submodule R M) r ⊤ ⊔ HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList rs) ⊤ < ⊤
Tactic: rw [isRegular_iff, ne_comm, ← lt_top_iff_ne_top, Ideal.ofList_cons,
      sup_smul, ideal_span_singleton_smul, isWeaklyRegular_cons_iff] at h
Cleared hypotheses: h
-- 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
inst_3 : IsArtinian R M
r : R
rs : List R
h :
  (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs) ∧
    HSMul.hSMul (β := Submodule R M) r ⊤ ⊔ HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList rs) ⊤ < ⊤
⊢ r :: rs = []
have refine : HSMul.hSMul (β := Submodule R M) r ⊤ = ⊤
Tactic: refine absurd ?_ (ne_of_lt (lt_of_le_of_lt le_sup_left h.right))
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : Module R M
inst_4 : Module R M₂
inst_5 : Module.Flat R M₂
rs : List R
h : IsWeaklyRegular M rs
⊢ IsWeaklyRegular (M₂ ⊗[R] M) rs
have nil : ∀ (N : Type u_3) [inst_6 : AddCommGroup N] [inst_7 : Module R N], IsWeaklyRegular (R := R) (M₂ ⊗[R] N) []
Tactic: induction h with
  | nil N => exact nil R (M₂ ⊗[R] N)
  | @cons N _ _ r rs' h1 _ ih =>
    let e := tensorQuotSMulTopEquivQuotSMulTop r M₂ N
    exact ((e.isWeaklyRegular_congr rs').mp ih).cons (h1.lTensor M₂)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : Module R M
inst_4 : Module R M₂
inst_5 : Module.Flat R M₂
rs : List R
h : IsWeaklyRegular M rs
nil : ∀ (N : Type u_3) [inst_6 : AddCommGroup N] [inst_7 : Module R N], IsWeaklyRegular (R := R) (M₂ ⊗[R] N) []
⊢ IsWeaklyRegular (M₂ ⊗[R] M) rs
have cons : ∀ {N : Type u_3} [inst_6 : AddCommGroup N] [inst_7 : Module R N] (r : R) (rs' : List R) (h1 : IsSMulRegular N r),
  IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r N) rs' →
    ∀ (ih : IsWeaklyRegular (TensorProduct.{u_1, u_4, u_3} R M₂ (QuotSMulTop r N)) rs'),
      IsWeaklyRegular (M₂ ⊗[R] N) (r :: rs')
Tactic: induction h with
  | nil N => exact nil R (M₂ ⊗[R] N)
  | @cons N _ _ r rs' h1 _ ih =>
    let e := tensorQuotSMulTopEquivQuotSMulTop r M₂ N
    exact ((e.isWeaklyRegular_congr rs').mp ih).cons (h1.lTensor M₂)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : Module R M
inst_4 : Module R M₂
inst_5 : Module.Flat R M₂
rs : List R
h : IsWeaklyRegular M rs
⊢ IsWeaklyRegular (M ⊗[R] M₂) rs
have nil : ∀ (N : Type u_3) [inst_6 : AddCommGroup N] [inst_7 : Module R N], IsWeaklyRegular (R := R) (N ⊗[R] M₂) []
Tactic: induction h with
  | nil N => exact nil R (N ⊗[R] M₂)
  | @cons N _ _ r rs' h1 _ ih =>
    let e := quotSMulTopTensorEquivQuotSMulTop r M₂ N
    exact ((e.isWeaklyRegular_congr rs').mp ih).cons (h1.rTensor M₂)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : Module R M
inst_4 : Module R M₂
inst_5 : Module.Flat R M₂
rs : List R
h : IsWeaklyRegular M rs
nil : ∀ (N : Type u_3) [inst_6 : AddCommGroup N] [inst_7 : Module R N], IsWeaklyRegular (R := R) (N ⊗[R] M₂) []
⊢ IsWeaklyRegular (M ⊗[R] M₂) rs
have cons : ∀ {N : Type u_3} [inst_6 : AddCommGroup N] [inst_7 : Module R N] (r : R) (rs' : List R) (h1 : IsSMulRegular N r),
  IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r N) rs' →
    ∀ (ih : IsWeaklyRegular (TensorProduct.{u_1, u_3, u_4} R (QuotSMulTop r N) M₂) rs'),
      IsWeaklyRegular (N ⊗[R] M₂) (r :: rs')
Tactic: induction h with
  | nil N => exact nil R (N ⊗[R] M₂)
  | @cons N _ _ r rs' h1 _ ih =>
    let e := quotSMulTopTensorEquivQuotSMulTop r M₂ N
    exact ((e.isWeaklyRegular_congr rs').mp ih).cons (h1.rTensor M₂)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M₄ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M₄
inst_2 : Module R M₄
rs : List R
M_1 : Type u_6
inst_3 : AddCommGroup M_1
inst_4 : Module R M_1
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst_5 : AddCommGroup M
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M_1
h₁₂ : Exact.{u_3, u_4, u_5} (M := M) (N := M₂) (P := M₃) (⇑f₁ : (a : M) → M₂) (⇑f₂ : (a : M₂) → M₃)
h₂₃ : Exact.{u_4, u_5, u_6} (M := M₂) (N := M₃) (P := M_1) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M_1)
h₃ : Surjective.{u_5 + 1, u_6 + 1} (α := M₃) (β := M_1) (⇑f₃ : (a : M₃) → M_1)
⊢ Exact.{u_3, u_4, u_5} (M := M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤)
    (N := M₂ ⧸ HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) (P :=
    M₃ ⧸ HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤)
    (⇑((HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).mapQ
          (HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) f₁ ⋯) :
      (a : M ⧸ Ideal.ofList [] • ⊤) → M₂ ⧸ Ideal.ofList [] • ⊤)
    (⇑((HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤).mapQ
          (HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤) f₂ ⋯) :
      (a : M₂ ⧸ Ideal.ofList [] • ⊤) → M₃ ⧸ Ideal.ofList [] • ⊤)
have apply : (M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤) ≃ₗ[R] M
Tactic: apply (Exact.iff_of_ladder_linearEquiv ?_ ?_).mp h₁₂
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M₄ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M₄
inst_2 : Module R M₄
rs : List R
M_1 : Type u_6
inst_3 : AddCommGroup M_1
inst_4 : Module R M_1
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst_5 : AddCommGroup M
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M_1
h₁₂ : Exact.{u_3, u_4, u_5} (M := M) (N := M₂) (P := M₃) (⇑f₁ : (a : M) → M₂) (⇑f₂ : (a : M₂) → M₃)
h₂₃ : Exact.{u_4, u_5, u_6} (M := M₂) (N := M₃) (P := M_1) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M_1)
h₃ : Surjective.{u_5 + 1, u_6 + 1} (α := M₃) (β := M_1) (⇑f₃ : (a : M₃) → M_1)
apply : (M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤) ≃ₗ[R] M
⊢ Exact.{u_3, u_4, u_5} (M := M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤)
    (N := M₂ ⧸ HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) (P :=
    M₃ ⧸ HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤)
    (⇑((HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).mapQ
          (HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) f₁ ⋯) :
      (a : M ⧸ Ideal.ofList [] • ⊤) → M₂ ⧸ Ideal.ofList [] • ⊤)
    (⇑((HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤).mapQ
          (HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤) f₂ ⋯) :
      (a : M₂ ⧸ Ideal.ofList [] • ⊤) → M₃ ⧸ Ideal.ofList [] • ⊤)
have apply₁ : (M₂ ⧸ HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) ≃ₗ[R] M₂
Tactic: apply (Exact.iff_of_ladder_linearEquiv ?_ ?_).mp h₁₂
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M₄ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M₄
inst_2 : Module R M₄
rs : List R
M_1 : Type u_6
inst_3 : AddCommGroup M_1
inst_4 : Module R M_1
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst_5 : AddCommGroup M
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M_1
h₁₂ : Exact.{u_3, u_4, u_5} (M := M) (N := M₂) (P := M₃) (⇑f₁ : (a : M) → M₂) (⇑f₂ : (a : M₂) → M₃)
h₂₃ : Exact.{u_4, u_5, u_6} (M := M₂) (N := M₃) (P := M_1) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M_1)
h₃ : Surjective.{u_5 + 1, u_6 + 1} (α := M₃) (β := M_1) (⇑f₃ : (a : M₃) → M_1)
apply : (M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤) ≃ₗ[R] M
apply₁ : (M₂ ⧸ HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) ≃ₗ[R] M₂
⊢ Exact.{u_3, u_4, u_5} (M := M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤)
    (N := M₂ ⧸ HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) (P :=
    M₃ ⧸ HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤)
    (⇑((HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).mapQ
          (HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) f₁ ⋯) :
      (a : M ⧸ Ideal.ofList [] • ⊤) → M₂ ⧸ Ideal.ofList [] • ⊤)
    (⇑((HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤).mapQ
          (HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤) f₂ ⋯) :
      (a : M₂ ⧸ Ideal.ofList [] • ⊤) → M₃ ⧸ Ideal.ofList [] • ⊤)
have apply₂ : (M₃ ⧸ HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤) ≃ₗ[R] M₃
Tactic: apply (Exact.iff_of_ladder_linearEquiv ?_ ?_).mp h₁₂
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M₄ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M₄
inst_2 : Module R M₄
rs : List R
M_1 : Type u_6
inst_3 : AddCommGroup M_1
inst_4 : Module R M_1
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst_5 : AddCommGroup M
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M_1
h₁₂ : Exact.{u_3, u_4, u_5} (M := M) (N := M₂) (P := M₃) (⇑f₁ : (a : M) → M₂) (⇑f₂ : (a : M₂) → M₃)
h₂₃ : Exact.{u_4, u_5, u_6} (M := M₂) (N := M₃) (P := M_1) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M_1)
h₃ : Surjective.{u_5 + 1, u_6 + 1} (α := M₃) (β := M_1) (⇑f₃ : (a : M₃) → M_1)
apply : (M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤) ≃ₗ[R] M
apply₁ : (M₂ ⧸ HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) ≃ₗ[R] M₂
apply₂ : (M₃ ⧸ HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤) ≃ₗ[R] M₃
⊢ Exact.{u_3, u_4, u_5} (M := M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤)
    (N := M₂ ⧸ HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) (P :=
    M₃ ⧸ HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤)
    (⇑((HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).mapQ
          (HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) f₁ ⋯) :
      (a : M ⧸ Ideal.ofList [] • ⊤) → M₂ ⧸ Ideal.ofList [] • ⊤)
    (⇑((HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤).mapQ
          (HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤) f₂ ⋯) :
      (a : M₂ ⧸ Ideal.ofList [] • ⊤) → M₃ ⧸ Ideal.ofList [] • ⊤)
have apply₃ : f₁ ∘ₗ
    (↑((HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).quotEquivOfEqBot sorry) :
      M ⧸ Ideal.ofList [] • ⊤ →ₗ[R] M) =
  (↑((HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤).quotEquivOfEqBot sorry) :
      M₂ ⧸ Ideal.ofList [] • ⊤ →ₗ[R] M₂) ∘ₗ
    (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).mapQ
      (HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) f₁ sorry
Tactic: apply (Exact.iff_of_ladder_linearEquiv ?_ ?_).mp h₁₂
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M₄ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M₄
inst_2 : Module R M₄
rs : List R
M_1 : Type u_6
inst_3 : AddCommGroup M_1
inst_4 : Module R M_1
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst_5 : AddCommGroup M
inst_6 : AddCommGroup M₂
inst_7 : AddCommGroup M₃
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
f₃ : M₃ →ₗ[R] M_1
h₁₂ : Exact.{u_3, u_4, u_5} (M := M) (N := M₂) (P := M₃) (⇑f₁ : (a : M) → M₂) (⇑f₂ : (a : M₂) → M₃)
h₂₃ : Exact.{u_4, u_5, u_6} (M := M₂) (N := M₃) (P := M_1) (⇑f₂ : (a : M₂) → M₃) (⇑f₃ : (a : M₃) → M_1)
h₃ : Surjective.{u_5 + 1, u_6 + 1} (α := M₃) (β := M_1) (⇑f₃ : (a : M₃) → M_1)
apply : (M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤) ≃ₗ[R] M
apply₁ : (M₂ ⧸ HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) ≃ₗ[R] M₂
apply₂ : (M₃ ⧸ HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤) ≃ₗ[R] M₃
apply₃ :
  f₁ ∘ₗ
      (↑((HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).quotEquivOfEqBot ⋯) :
        M ⧸ Ideal.ofList [] • ⊤ →ₗ[R] M) =
    (↑((HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤).quotEquivOfEqBot ⋯) :
        M₂ ⧸ Ideal.ofList [] • ⊤ →ₗ[R] M₂) ∘ₗ
      (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).mapQ
        (HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) f₁ ⋯
⊢ Exact.{u_3, u_4, u_5} (M := M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤)
    (N := M₂ ⧸ HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) (P :=
    M₃ ⧸ HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤)
    (⇑((HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).mapQ
          (HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) f₁ ⋯) :
      (a : M ⧸ Ideal.ofList [] • ⊤) → M₂ ⧸ Ideal.ofList [] • ⊤)
    (⇑((HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤).mapQ
          (HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤) f₂ ⋯) :
      (a : M₂ ⧸ Ideal.ofList [] • ⊤) → M₃ ⧸ Ideal.ofList [] • ⊤)
have apply₄ : f₂ ∘ₗ
    (↑((HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤).quotEquivOfEqBot sorry) :
      M₂ ⧸ Ideal.ofList [] • ⊤ →ₗ[R] M₂) =
  (↑((HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤).quotEquivOfEqBot sorry) :
      M₃ ⧸ Ideal.ofList [] • ⊤ →ₗ[R] M₃) ∘ₗ
    (HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤).mapQ
      (HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤) f₂ sorry
Tactic: apply (Exact.iff_of_ladder_linearEquiv ?_ ?_).mp h₁₂
-- 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
h1 : IsWeaklyRegular M [a, b]
h2 :
  torsionBy R M b = HSMul.hSMul (β := Submodule R M) a (torsionBy R M b) → Eq (α := Submodule R M) (torsionBy R M b) ⊥
⊢ IsWeaklyRegular M [b, a]
have rw : ∀ (h1 : IsSMulRegular M a ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b)
  (h2 :
    torsionBy R M b = HSMul.hSMul (β := Submodule R M) a (torsionBy R M b) →
      Eq (α := Submodule R M) (torsionBy R M b) ⊥),
  IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop b M) a
Tactic: rw [isWeaklyRegular_cons_iff, isWeaklyRegular_singleton_iff] at h1 ⊢
Cleared hypotheses: h1, h2
-- 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
h1 : IsSMulRegular M a ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b
h2 :
  torsionBy R M b = HSMul.hSMul (β := Submodule R M) a (torsionBy R M b) → Eq (α := Submodule R M) (torsionBy R M b) ⊥
⊢ IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop b M) a
have ha : IsSMulRegular M a
Tactic: obtain ⟨ha, hb⟩ := h1
Cleared hypotheses: h1
-- 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
h1 : IsSMulRegular M a ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b
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
⊢ IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop b M) a
have hb : IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b
Tactic: obtain ⟨ha, hb⟩ := h1
Cleared hypotheses: h1