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₁ rs₂ : List R
⊢ IsWeaklyRegular M (rs₁ ++ rs₂) ↔
    IsWeaklyRegular M rs₁ ∧
      IsWeaklyRegular.{u_1, u_3} (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.ofList rs₁))
        (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₁) ⊤)
        (List.map (⇑(Ideal.Quotient.mk (Ideal.ofList rs₁)) : (a : R) → R ⧸ Ideal.ofList rs₁) rs₂)

Tactic:
Iff.trans (isWeaklyRegular_append_iff M rs₁ rs₂) <| and_congr_right' <|
    Iff.symm <| isWeaklyRegular_map_algebraMap_iff (R ⧸ Ideal.ofList rs₁) _ rs₂

Premises used: RingTheory.Sequence.isWeaklyRegular_map_algebraMap_iff, and_congr_right', RingTheory.Sequence.isWeaklyRegular_append_iff, HasQuotient.Quotient, Ideal.ofList, Iff.trans, Iff.symm
-- 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
inst_3 : Nontrivial M
h : ⊤ = HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤
⊢ Subsingleton.{u_3 + 1} (Submodule R M)

Tactic:
rw [Ideal.ofList_nil, bot_smul, eq_comm, subsingleton_iff_bot_eq_top] at h

Premises used: Submodule.bot_smul, eq_comm, Ideal.ofList_nil, subsingleton_iff_bot_eq_top
-- 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
inst_3 : Nontrivial M
h : Subsingleton.{u_3 + 1} (Submodule R M)
⊢ False

Tactic:
not_subsingleton M ((Submodule.subsingleton_iff _).mp h)

Premises used: Submodule.subsingleton_iff, not_subsingleton, Iff.mp
-- 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
inst_3 : Nontrivial M
h : Subsingleton.{u_3 + 1} (Submodule R M)
⊢ False

Tactic:
exact not_subsingleton M ((Submodule.subsingleton_iff _).mp h)

Premises used: Submodule.subsingleton_iff, not_subsingleton, Iff.mp
-- 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
r : R
rs : List R
h1 : IsSMulRegular M r
h2 : IsRegular.{u_1, u_3} (QuotSMulTop r M) rs
⊢ IsRegular M (r :: rs)

Tactic:
(isRegular_cons_iff M r rs).mpr ⟨h1, h2⟩

Premises used: Iff.mpr, RingTheory.Sequence.isRegular_cons_iff, And.intro
-- 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
r : R
rs : List R
h1 : IsSMulRegular M r
h2 :
  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)
⊢ IsRegular M (r :: rs)

Tactic:
(isRegular_cons_iff' M r rs).mpr ⟨h1, h2⟩

Premises used: Iff.mpr, And.intro, RingTheory.Sequence.isRegular_cons_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 : IsRegular M rs
N : Submodule R M
⊢ Nontrivial.{u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (Ideal.ofList rs) N)

Tactic:
Submodule.Quotient.nontrivial_iff.mpr <|
    ne_top_of_le_ne_top h.top_ne_smul.symm (smul_mono_right _ le_top)

Premises used: Iff.mpr, RingTheory.Sequence.IsRegular.top_ne_smul, smul_mono_right, Ne.symm, ne_top_of_le_ne_top, le_top, Submodule.Quotient.nontrivial_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 : IsRegular M rs
⊢ Nontrivial M

Tactic:
haveI := quot_ofList_smul_nontrivial h ⊤
  (mkQ_surjective (Ideal.ofList rs • ⊤ : Submodule R M)).nontrivial

Premises used: Function.Surjective.nontrivial, Ideal.ofList, HSMul.hSMul, Submodule.mkQ_surjective, Top.top
-- 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
inst_3 : Nontrivial M
inst_4 : Module.Finite R M
rs : List R
h : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (Ideal.jacobson (Module.annihilator R M)) r
⊢ IsRegular M rs ↔ IsWeaklyRegular M rs

Tactic:
Iff.trans (isRegular_iff M rs) <| and_iff_left <|
    top_ne_ideal_smul_of_le_jacobson_annihilator <| Ideal.span_le.mpr h

Premises used: Ideal.span_le, Iff.mpr, and_iff_left, RingTheory.Sequence.isRegular_iff, Iff.trans, Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator
-- 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
inst_3 : IsLocalRing R
inst_4 : Nontrivial M
inst_5 : Module.Finite R M
rs : List R
h : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) r
⊢ IsRegular M rs ↔ IsWeaklyRegular M rs

Tactic:
have H h' := bot_ne_top.symm <| annihilator_eq_top_iff.mp <|
    Eq.trans annihilator_top h'
  isRegular_iff_isWeaklyRegular_of_subset_jacobson_annihilator fun r hr =>
    IsLocalRing.jacobson_eq_maximalIdeal (Module.annihilator R M) H ▸ h r hr

Premises used: Module.annihilator, Eq.rec, Ne.symm, Iff.mp, Submodule.annihilator_top, bot_ne_top, IsLocalRing.jacobson_eq_maximalIdeal, RingTheory.Sequence.isRegular_iff_isWeaklyRegular_of_subset_jacobson_annihilator, Eq.symm, Submodule.annihilator_eq_top_iff, Eq.trans
-- 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
inst_3 : IsArtinian R M
r : R
rs : List R
h : IsRegular M (r :: rs)
⊢ (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

Premises used: RingTheory.Sequence.isWeaklyRegular_cons_iff, Submodule.ideal_span_singleton_smul, lt_top_iff_ne_top, Submodule.sup_smul, RingTheory.Sequence.isRegular_iff, ne_comm, Ideal.ofList_cons
-- 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
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 = []

Tactic:
absurd ?_ (ne_of_lt (lt_of_le_of_lt le_sup_left h.right))

Premises used: lt_of_le_of_lt, le_sup_left, absurd, And.right, ne_of_lt
-- 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
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) ⊤ < ⊤
refine : HSMul.hSMul (β := Submodule R M) r ⊤ = ⊤
⊢ r :: rs = []

Tactic:
refine absurd ?_ (ne_of_lt (lt_of_le_of_lt le_sup_left h.right))

Premises used: lt_of_le_of_lt, le_sup_left, absurd, And.right, ne_of_lt
-- 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
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) ⊤ < ⊤
⊢ HSMul.hSMul (β := Submodule R M) r ⊤ = ⊤

Tactic:
Eq.trans (Submodule.map_top _) <| LinearMap.range_eq_top.mpr <|
      surjective_of_injective_endomorphism (LinearMap.lsmul R M r) h.left.left

Premises used: Iff.mpr, Submodule.map_top, LinearMap.lsmul, LinearMap.range_eq_top, IsArtinian.surjective_of_injective_endomorphism, And.left, DFunLike.coe, Eq.trans
-- 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
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) ⊤ < ⊤
⊢ HSMul.hSMul (β := Submodule R M) r ⊤ = ⊤

Tactic:
exact Eq.trans (Submodule.map_top _) <| LinearMap.range_eq_top.mpr <|
      surjective_of_injective_endomorphism (LinearMap.lsmul R M r) h.left.left

Premises used: Iff.mpr, Submodule.map_top, LinearMap.lsmul, LinearMap.range_eq_top, IsArtinian.surjective_of_injective_endomorphism, And.left, DFunLike.coe, Eq.trans
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
⊢ IsWeaklyRegular (R := R) (M₂ ⊗[R] N) []

Tactic:
nil R (M₂ ⊗[R] N)

Premises used: RingTheory.Sequence.IsWeaklyRegular.nil, TensorProduct
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
⊢ IsWeaklyRegular (R := R) (M₂ ⊗[R] N) []

Tactic:
exact nil R (M₂ ⊗[R] N)

Premises used: RingTheory.Sequence.IsWeaklyRegular.nil, TensorProduct
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
r : R
rs' : List R
h1 : IsSMulRegular N r
h2 : IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r N) rs'
ih : IsWeaklyRegular (TensorProduct.{u_1, u_4, u_3} R M₂ (QuotSMulTop r N)) rs'
e : TensorProduct.{u_1, u_4, u_3} R M₂ (QuotSMulTop r N) ≃ₗ[R] QuotSMulTop r (M₂ ⊗[R] N) :=
  tensorQuotSMulTopEquivQuotSMulTop r M₂ N
⊢ IsWeaklyRegular (M₂ ⊗[R] N) (r :: rs')

Tactic:
((e.isWeaklyRegular_congr rs').mp ih).cons (h1.lTensor M₂)

Premises used: IsSMulRegular.lTensor, RingTheory.Sequence.IsWeaklyRegular.cons, Iff.mp, LinearEquiv.isWeaklyRegular_congr
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
r : R
rs' : List R
h1 : IsSMulRegular N r
h2 : IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r N) rs'
ih : IsWeaklyRegular (TensorProduct.{u_1, u_4, u_3} R M₂ (QuotSMulTop r N)) rs'
e : TensorProduct.{u_1, u_4, u_3} R M₂ (QuotSMulTop r N) ≃ₗ[R] QuotSMulTop r (M₂ ⊗[R] N) :=
  tensorQuotSMulTopEquivQuotSMulTop r M₂ N
⊢ IsWeaklyRegular (M₂ ⊗[R] N) (r :: rs')

Tactic:
exact ((e.isWeaklyRegular_congr rs').mp ih).cons (h1.lTensor M₂)

Premises used: IsSMulRegular.lTensor, RingTheory.Sequence.IsWeaklyRegular.cons, Iff.mp, LinearEquiv.isWeaklyRegular_congr
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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) []
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')
⊢ IsWeaklyRegular (M₂ ⊗[R] M) 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₂)

Premises used: RingTheory.Sequence.IsWeaklyRegular.cons, RingTheory.Sequence.IsWeaklyRegular.nil
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
⊢ IsWeaklyRegular (R := R) (N ⊗[R] M₂) []

Tactic:
nil R (N ⊗[R] M₂)

Premises used: RingTheory.Sequence.IsWeaklyRegular.nil, TensorProduct
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
⊢ IsWeaklyRegular (R := R) (N ⊗[R] M₂) []

Tactic:
exact nil R (N ⊗[R] M₂)

Premises used: RingTheory.Sequence.IsWeaklyRegular.nil, TensorProduct
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
r : R
rs' : List R
h1 : IsSMulRegular N r
h2 : IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r N) rs'
ih : IsWeaklyRegular (TensorProduct.{u_1, u_3, u_4} R (QuotSMulTop r N) M₂) rs'
e : TensorProduct.{u_1, u_3, u_4} R (QuotSMulTop r N) M₂ ≃ₗ[R] QuotSMulTop r (N ⊗[R] M₂) :=
  quotSMulTopTensorEquivQuotSMulTop r M₂ N
⊢ IsWeaklyRegular (N ⊗[R] M₂) (r :: rs')

Tactic:
((e.isWeaklyRegular_congr rs').mp ih).cons (h1.rTensor M₂)

Premises used: RingTheory.Sequence.IsWeaklyRegular.cons, Iff.mp, LinearEquiv.isWeaklyRegular_congr, IsSMulRegular.rTensor
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
r : R
rs' : List R
h1 : IsSMulRegular N r
h2 : IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r N) rs'
ih : IsWeaklyRegular (TensorProduct.{u_1, u_3, u_4} R (QuotSMulTop r N) M₂) rs'
e : TensorProduct.{u_1, u_3, u_4} R (QuotSMulTop r N) M₂ ≃ₗ[R] QuotSMulTop r (N ⊗[R] M₂) :=
  quotSMulTopTensorEquivQuotSMulTop r M₂ N
⊢ IsWeaklyRegular (N ⊗[R] M₂) (r :: rs')

Tactic:
exact ((e.isWeaklyRegular_congr rs').mp ih).cons (h1.rTensor M₂)

Premises used: RingTheory.Sequence.IsWeaklyRegular.cons, Iff.mp, LinearEquiv.isWeaklyRegular_congr, IsSMulRegular.rTensor
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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₂) []
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')
⊢ IsWeaklyRegular (M ⊗[R] M₂) 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₂)

Premises used: RingTheory.Sequence.IsWeaklyRegular.cons, RingTheory.Sequence.IsWeaklyRegular.nil
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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₁ ⋯
apply₄ :
  f₂ ∘ₗ
      (↑((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_5, u_5} (α := 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 []) ⊤).mapQ
        (HSMul.hSMul.{u_1, u_5, u_5} (α := 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 [] • ⊤)

Tactic:
apply (Exact.iff_of_ladder_linearEquiv ?_ ?_).mp h₁₂

Premises used: Function.Exact.iff_of_ladder_linearEquiv, Iff.mp
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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)
⊢ (M ⧸ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤) ≃ₗ[R] M

Tactic:
exact quotEquivOfEqBot _ <|
      Eq.trans (congrArg (· • ⊤) Ideal.ofList_nil) (bot_smul ⊤)

Premises used: congrArg, Submodule.bot_smul, Submodule.quotEquivOfEqBot, Ideal.ofList_nil, HSMul.hSMul, Top.top, Eq.trans
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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)
⊢ (M₂ ⧸ HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList []) ⊤) ≃ₗ[R] M₂

Tactic:
exact quotEquivOfEqBot _ <|
      Eq.trans (congrArg (· • ⊤) Ideal.ofList_nil) (bot_smul ⊤)

Premises used: congrArg, Submodule.bot_smul, Submodule.quotEquivOfEqBot, Ideal.ofList_nil, HSMul.hSMul, Top.top, Eq.trans
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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)
⊢ (M₃ ⧸ HSMul.hSMul.{u_1, u_5, u_5} (α := Ideal R) (β := Submodule R M₃) (Ideal.ofList []) ⊤) ≃ₗ[R] M₃

Tactic:
exact quotEquivOfEqBot _ <|
      Eq.trans (congrArg (· • ⊤) Ideal.ofList_nil) (bot_smul ⊤)

Premises used: congrArg, Submodule.bot_smul, Submodule.quotEquivOfEqBot, Ideal.ofList_nil, HSMul.hSMul, Top.top, Eq.trans
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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)
⊢ 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₁ ⋯

Tactic:
quotEquivOfEqBot _ <|
      Eq.trans (congrArg (· • ⊤) Ideal.ofList_nil) (bot_smul ⊤)

Premises used: congrArg, Submodule.bot_smul, Submodule.quotEquivOfEqBot, Ideal.ofList_nil, HSMul.hSMul, Top.top, Eq.trans