awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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₂ ⋯

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
-- 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:
quot_hom_ext _ _ _ fun _ => rfl

Premises used: rfl, Submodule.quot_hom_ext
-- 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:
exact quot_hom_ext _ _ _ fun _ => rfl

Premises used: rfl, Submodule.quot_hom_ext
-- 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_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₂ ⋯

Tactic:
quot_hom_ext _ _ _ fun _ => rfl

Premises used: rfl, Submodule.quot_hom_ext
-- 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_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₂ ⋯

Tactic:
exact quot_hom_ext _ _ _ fun _ => rfl

Premises used: rfl, Submodule.quot_hom_ext
-- 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_1 : List R
M_1 : Type u_6
inst_3 : AddCommGroup M_1
inst_4 : Module R M_1
r : R
rs : List R
h₄ : IsSMulRegular M_1 r
h2 : IsWeaklyRegular.{u_1, u_6} (QuotSMulTop r M_1) rs
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)
ih :
  Exact.{u_3, u_4, u_5} (M :=
    QuotSMulTop r M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤) (N :=
    QuotSMulTop r M₂ ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M₂)) (Ideal.ofList rs) ⊤) (P :=
    QuotSMulTop r M₃ ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M₃)) (Ideal.ofList rs) ⊤)
    (⇑((HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤).mapQ
          (HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M₂)) (Ideal.ofList rs) ⊤)
          ((QuotSMulTop.map r : (a : M →ₗ[R] M₂) → QuotSMulTop r M →ₗ[R] QuotSMulTop r M₂) f₁) ⋯) :
      (a : QuotSMulTop r M ⧸ Ideal.ofList rs • ⊤) → QuotSMulTop r M₂ ⧸ Ideal.ofList rs • ⊤)
    (⇑((HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M₂)) (Ideal.ofList rs) ⊤).mapQ
          (HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M₃)) (Ideal.ofList rs) ⊤)
          ((QuotSMulTop.map r : (a : M₂ →ₗ[R] M₃) → QuotSMulTop r M₂ →ₗ[R] QuotSMulTop r M₃) f₂) ⋯) :
      (a : QuotSMulTop r M₂ ⧸ Ideal.ofList rs • ⊤) → QuotSMulTop r M₃ ⧸ Ideal.ofList rs • ⊤)
⊢ (↑(quotOfListConsSMulTopEquivQuotSMulTopInner M₂ r rs) :
        M₂ ⧸ Ideal.ofList (r :: rs) • ⊤ →ₗ[R] QuotSMulTop r M₂ ⧸ Ideal.ofList rs • ⊤) ∘ₗ
      (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤).mapQ
        (HSMul.hSMul (α := Ideal R) (β := Submodule R M₂) (Ideal.ofList (r :: rs)) ⊤) f₁ ⋯ =
    (HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤).mapQ
        (HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M₂)) (Ideal.ofList rs) ⊤)
        ((QuotSMulTop.map r : (a : M →ₗ[R] M₂) → QuotSMulTop r M →ₗ[R] QuotSMulTop r M₂) f₁) ⋯ ∘ₗ
      (↑(quotOfListConsSMulTopEquivQuotSMulTopInner M r rs) :
        M ⧸ Ideal.ofList (r :: rs) • ⊤ →ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs • ⊤)

Tactic:
have H₁ := quotOfListConsSMulTopEquivQuotSMulTopInner_naturality r rs f₁
-- 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
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) ⊥
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
⊢ IsWeaklyRegular M [b, a]

Tactic:
rw [isWeaklyRegular_cons_iff, isWeaklyRegular_singleton_iff] at h1 ⊢

Premises used: RingTheory.Sequence.isWeaklyRegular_cons_iff, RingTheory.Sequence.isWeaklyRegular_singleton_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
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 a

Tactic:
obtain ⟨ha, hb⟩ := h1
-- 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
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.{u_1, u_3} (QuotSMulTop a M) b

Tactic:
obtain ⟨ha, hb⟩ := h1
-- 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
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
⊢ 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

Premises used: isSMulRegular_iff_torsionBy_eq_bot
-- 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
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
h2₁ : torsionBy R M b = HSMul.hSMul (β := Submodule R M) a (torsionBy R M b) → IsSMulRegular M b
⊢ IsSMulRegular M a

Tactic:
rw [← isSMulRegular_iff_torsionBy_eq_bot] at h2

Premises used: isSMulRegular_iff_torsionBy_eq_bot
-- 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
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
h2₁ : torsionBy R M b = HSMul.hSMul (β := Submodule R M) a (torsionBy R M b) → IsSMulRegular M b
ha₁ : IsSMulRegular M a
⊢ IsSMulRegular.{u_1, u_3} (QuotSMulTop a M) b

Tactic:
rw [← isSMulRegular_iff_torsionBy_eq_bot] at h2

Premises used: isSMulRegular_iff_torsionBy_eq_bot
-- 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
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)
specialize₁ : ∀ (h2 : IsSMulRegular M b), IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop b M) a
⊢ 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)))

Premises used: Submodule.torsionBy, Submodule.smul_le_self_of_tower, le_antisymm
-- 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
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)

Tactic:
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

Premises used: LinearMap.ker_eq_bot, LinearMap.lsmul, Submodule.ker_liftQ_eq_bot', smul_top_inf_eq_smul_of_isSMulRegular_on_quot, Iff.mp, le_of_eq_of_le, IsSMulRegular.of_injective, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
refine : torsionBy R M b = HSMul.hSMul (β := Submodule R M) a ⊤ ⊓ torsionBy R M b
⊢ 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

Premises used: LinearMap.ker_eq_bot, LinearMap.lsmul, Submodule.ker_liftQ_eq_bot', smul_top_inf_eq_smul_of_isSMulRegular_on_quot, Iff.mp, le_of_eq_of_le, IsSMulRegular.of_injective, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
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)
⊢ torsionBy R M b = HSMul.hSMul (β := Submodule R M) a ⊤ ⊓ torsionBy R M b

Tactic:
rw [← (isSMulRegular_on_quot_iff_lsmul_comap_eq _ _).mp hb]

Premises used: Iff.mp, isSMulRegular_on_quot_iff_lsmul_comap_eq
-- 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
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
⊢ 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:
(inf_eq_right.mpr (ker_le_comap _)).symm

Premises used: Iff.mpr, Submodule.torsionBy, inf_eq_right, Eq.symm, LinearMap.ker_le_comap
-- 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
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
⊢ 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:
exact (inf_eq_right.mpr (ker_le_comap _)).symm

Premises used: Iff.mpr, inf_eq_right, Eq.symm, LinearMap.ker_le_comap
-- 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
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 ⊤
rwa₃ : IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (β := Submodule R M) a ⊤) b
rwa₄ rwa₅ rwa₆ rwa₇ : IsSMulRegular M b
⊢ IsSMulRegular M b ∧ IsSMulRegular.{u_1, u_3} (QuotSMulTop b 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]

Premises used: and_iff_left, inf_comm, IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, SMulCommClass.smul_comm
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rs : List R
h_1 : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K : Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) :=
        torsionBy.{u_1, u_3} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ rs₀ : List R
H₁ H₃ : rs₀ ++ [] <+~ rs
h : IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) []
⊢ IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) []

Tactic:
.nil R _

Premises used: RingTheory.Sequence.IsWeaklyRegular.nil
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rs : List R
h_1 : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K : Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) :=
        torsionBy.{u_1, u_3} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ rs₀ : List R
H₁ H₃ : rs₀ ++ [] <+~ rs
h : IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) []
⊢ IsWeaklyRegular.{u_1, u_3} (R := R) (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) []

Tactic:
exact .nil R _
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rs : List R
h_1 : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K : Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) :=
        torsionBy.{u_1, u_3} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ : List R
r : R
l₁ l₂ : List R
h_2 : l₁ ~ l₂
ih :
  ∀ (rs₀ : List R) (H₁ : rs₀ ++ l₁ <+~ rs) (H₃ : rs₀ ++ l₂ <+~ rs)
    (h : IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₁),
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₂
rs₀ : List R
H₁ : rs₀ ++ r :: l₁ <+~ rs
H₃ : rs₀ ++ r :: l₂ <+~ rs
h : 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₀
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₂
⊢ IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) (r :: l₂)

Tactic:
rw [isWeaklyRegular_cons_iff, ← e.isWeaklyRegular_congr] at h ⊢

Premises used: RingTheory.Sequence.isWeaklyRegular_cons_iff, LinearEquiv.isWeaklyRegular_congr
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rs : List R
h_1 : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K : Submodule R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) :=
        torsionBy.{u_1, u_3} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs') ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ : List R
r : R
l₁ l₂ : List R
h_2 : l₁ ~ l₂
ih :
  ∀ (rs₀ : List R) (H₁ : rs₀ ++ l₁ <+~ rs) (H₃ : rs₀ ++ l₂ <+~ rs)
    (h : IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₁),
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) l₂
rs₀ : List R
H₁ : rs₀ ++ r :: l₁ <+~ rs
H₃ : rs₀ ++ r :: l₂ <+~ rs
h :
  IsSMulRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) r ∧
    IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₀)) ⊤) l₁
e : (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs₀)) ⊤) ≃ₗ[R]
  QuotSMulTop r (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList rs₀) ⊤) :=
  quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
⊢ 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:
h.imp_right (ih (r :: rs₀) ?_ ?_)

Premises used: List.cons, And.imp_right