awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (e : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((e : (a : M) → M₂) x : M₂))
    as bs
a : IsWeaklyRegular M as ∧ Nontrivial.{u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList as) ⊤)
b : IsWeaklyRegular M₂ bs ∧ Nontrivial.{u_4} (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList bs) ⊤)
| IsRegular M as ↔ IsRegular M₂ bs

Tactic:
congr <;> rw [isRegular_iff, ne_comm, ← Quotient.nontrivial_iff]

Premises used: RingTheory.Sequence.isRegular_iff, ne_comm, Submodule.Quotient.nontrivial_iff
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (e : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((e : (a : M) → M₂) x : M₂))
    as bs
conv :
  IsWeaklyRegular M as ∧ Nontrivial.{u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList as) ⊤) ↔
    IsWeaklyRegular M₂ bs ∧ Nontrivial.{u_4} (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList bs) ⊤)
⊢ IsRegular M as ↔ IsRegular M₂ bs

Tactic:
conv => congr <;> rw [isRegular_iff, ne_comm, ← Quotient.nontrivial_iff]

Premises used: RingTheory.Sequence.isRegular_iff, ne_comm, Submodule.Quotient.nontrivial_iff
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (e : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((e : (a : M) → M₂) x : M₂))
    as bs
e' : AddEquiv.{u_3, u_4} (M ⧸ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList as) ⊤).toAddSubgroup)
  (M₂ ⧸ (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList bs) ⊤).toAddSubgroup) :=
  QuotientAddGroup.congr (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList as) ⊤).toAddSubgroup
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList bs) ⊤).toAddSubgroup e ⋯
⊢ IsWeaklyRegular M as ∧ Nontrivial.{u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList as) ⊤) ↔
    IsWeaklyRegular M₂ bs ∧ Nontrivial.{u_4} (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList bs) ⊤)

Tactic:
and_congr (e.isWeaklyRegular_congr h) e'.nontrivial_congr

Premises used: Equiv.nontrivial_congr, AddEquiv.isWeaklyRegular_congr, AddEquiv.toEquiv, and_congr
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (e : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((e : (a : M) → M₂) x : M₂))
    as bs
e' : AddEquiv.{u_3, u_4} (M ⧸ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList as) ⊤).toAddSubgroup)
  (M₂ ⧸ (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList bs) ⊤).toAddSubgroup) :=
  QuotientAddGroup.congr (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList as) ⊤).toAddSubgroup
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList bs) ⊤).toAddSubgroup e ⋯
⊢ IsWeaklyRegular M as ∧ Nontrivial.{u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList as) ⊤) ↔
    IsWeaklyRegular M₂ bs ∧ Nontrivial.{u_4} (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList bs) ⊤)

Tactic:
exact and_congr (e.isWeaklyRegular_congr h) e'.nontrivial_congr

Premises used: Equiv.nontrivial_congr, AddEquiv.isWeaklyRegular_congr, AddEquiv.toEquiv, and_congr
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
rs : List R
⊢ IsRegular M rs ↔ IsRegular.{u_2, u_4} (R := S) M₂ (List.map (⇑σ : (a : R) → S) rs)

Tactic:
e.toAddEquiv.isRegular_congr <| List.forall₂_map_right_iff.mpr <|
    List.forall₂_same.mpr fun r _ x => e.map_smul' r x

Premises used: Iff.mpr, List.forall₂_map_right_iff, AddEquiv.isRegular_congr, List.forall₂_same, LinearEquiv.toLinearMap, LinearMap.map_smul'
-- 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₂
e : M ≃ₗ[R] M₂
rs : List R
⊢ IsRegular M rs ↔ IsRegular M₂ rs

Tactic:
Iff.trans (e.isRegular_congr' rs) <| iff_of_eq <| congrArg _ rs.map_id

Premises used: congrArg, List.map_id, Iff.trans, LinearEquiv.isRegular_congr', iff_of_eq
-- Module: Mathlib.RingTheory.Regular.RegularSequence
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
rs : List R
⊢ IsWeaklyRegular.{u_2, u_3} (R := S) M (List.map (⇑(algebraMap R S) : (a : R) → S) rs) ↔ IsWeaklyRegular M rs

Tactic:
(AddEquiv.refl M).isWeaklyRegular_congr <| List.forall₂_map_left_iff.mpr <|
    List.forall₂_same.mpr fun r _ => algebraMap_smul S r

Premises used: Iff.mpr, List.forall₂_map_left_iff, algebraMap_smul, List.forall₂_same, AddEquiv.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
r : R
rs : List R
⊢ IsWeaklyRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs

Tactic:
have := Eq.trans (congrArg (· • ⊤) Ideal.ofList_nil) (bot_smul ⊤)
  let e i := quotOfListConsSMulTopEquivQuotSMulTopInner M r (rs.take i)
  Iff.trans (isWeaklyRegular_iff_Fin _ _) <| Iff.trans Fin.forall_iff_succ <|
    and_congr ((quotEquivOfEqBot _ this).isSMulRegular_congr r) <|
      Iff.trans (forall_congr' fun i => (e i).isSMulRegular_congr (rs.get i))
        (isWeaklyRegular_iff_Fin _ _).symm

Premises used: congrArg, RingTheory.Sequence.isWeaklyRegular_iff_Fin, List.get, Submodule.bot_smul, Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner, Submodule.quotEquivOfEqBot, Fin.val, List.cons, Fin.forall_iff_succ, Ideal.ofList, Ideal.ofList_nil, LinearEquiv.isSMulRegular_congr, forall_congr', Iff.trans, HSMul.hSMul, Top.top, List.take, QuotSMulTop, Iff.symm, and_congr, Eq.trans, List.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
r : R
rs : List R
⊢ IsWeaklyRegular M (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)

Tactic:
Iff.trans (isWeaklyRegular_cons_iff M r rs) <| and_congr_right' <|
    Iff.symm <| isWeaklyRegular_map_algebraMap_iff (R ⧸ Ideal.span {r}) _ rs

Premises used: RingTheory.Sequence.isWeaklyRegular_map_algebraMap_iff, RingTheory.Sequence.isWeaklyRegular_cons_iff, and_congr_right', HasQuotient.Quotient, Iff.trans, Ideal.span, Singleton.singleton, 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
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) ⊤
rw₅ 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

Tactic:
rw [isRegular_iff, isRegular_iff, isWeaklyRegular_cons_iff M r rs,
    ne_eq, top_eq_ofList_cons_smul_iff, and_assoc]

Premises used: RingTheory.Sequence.isWeaklyRegular_cons_iff, Submodule.top_eq_ofList_cons_smul_iff, ne_eq, and_assoc, RingTheory.Sequence.isRegular_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
r : R
rs : List R
a : IsRegular M (r :: rs)
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)
| 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)

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

Tactic:
rw [isRegular_iff, ne_eq]

Premises used: ne_eq, RingTheory.Sequence.isRegular_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
r : R
rs : List R
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)) ⊤
| 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:
rw [isRegular_iff, ne_eq]

Premises used: ne_eq, RingTheory.Sequence.isRegular_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
r : R
rs : List R
a : IsWeaklyRegular M (r :: rs) ∧ ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: rs)) ⊤
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)) ⊤
| 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)

Tactic:
congr <;> rw [isRegular_iff, ne_eq]

Premises used: ne_eq, RingTheory.Sequence.isRegular_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
r : R
rs : List R
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)) ⊤
⊢ 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)

Tactic:
conv => congr <;> rw [isRegular_iff, ne_eq]

Premises used: ne_eq, RingTheory.Sequence.isRegular_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
⊢ IsWeaklyRegular.{u_1, u_3} (R := R) M []

Tactic:
.mk (False.elim <| Nat.not_lt_zero · ·)

Premises used: False.elim, RingTheory.Sequence.IsWeaklyRegular.mk, Nat.not_lt_zero
-- 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 : IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs
⊢ IsWeaklyRegular M (r :: rs)

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

Premises used: Iff.mpr, RingTheory.Sequence.isWeaklyRegular_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 :
  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)
⊢ IsWeaklyRegular M (r :: rs)

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

Premises used: Iff.mpr, RingTheory.Sequence.isWeaklyRegular_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
⊢ IsWeaklyRegular M [r] ↔ IsSMulRegular M r

Tactic:
Iff.trans (isWeaklyRegular_cons_iff M r []) (and_iff_left (.nil R _))

Premises used: RingTheory.Sequence.isWeaklyRegular_cons_iff, and_iff_left, RingTheory.Sequence.IsWeaklyRegular.nil, Iff.trans, List.nil
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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₂

Tactic:
Iff.symm <| Iff.trans (and_iff_right (.nil R M)) ?_

Premises used: and_iff_right, RingTheory.Sequence.IsWeaklyRegular.nil, Iff.trans, Iff.symm
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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 :
  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₂)
⊢ 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:
refine Iff.symm <| Iff.trans (and_iff_right (.nil R M)) ?_

Premises used: and_iff_right, Iff.trans, Iff.symm
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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) (Ideal.ofList []) ⊤ = ⊥
⊢ 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 (quotEquivOfEqBot _ ?_).isWeaklyRegular_congr rs₂

Premises used: Submodule.quotEquivOfEqBot, LinearEquiv.isWeaklyRegular_congr
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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) ⊥ ⊤ = ⊥
nil₁ nil₂ : Eq.{u_3 + 1} (α := Submodule R M) ⊥ ⊥
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤ = ⊥

Tactic:
rw [Ideal.ofList_nil, bot_smul]

Premises used: Submodule.bot_smul, Ideal.ofList_nil
-- Module: Mathlib.RingTheory.Regular.RegularSequence
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₂
cons₅ 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₂
⊢ 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₂]

Premises used: RingTheory.Sequence.isWeaklyRegular_cons_iff, and_assoc, LinearEquiv.isWeaklyRegular_congr, List.cons_append
-- 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
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₂
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₂
⊢ IsWeaklyRegular M (rs₁ ++ rs₂) ↔
    IsWeaklyRegular M rs₁ ∧
      IsWeaklyRegular.{u_1, u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList 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₂]

Premises used: RingTheory.Sequence.isWeaklyRegular_cons_iff, Submodule.bot_smul, Submodule.quotEquivOfEqBot, and_iff_right, and_assoc, Ideal.ofList_nil, Iff.trans, LinearEquiv.isWeaklyRegular_congr, List.cons_append, Iff.symm