awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    as bs
⊢ AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList as) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList bs) ⊤).toAddSubgroup
have nil : AddSubgroup.map f (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).toAddSubgroup =
  (HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList []) ⊤).toAddSubgroup
Tactic: induction h with
  | nil =>
    convert! AddSubgroup.map_bot f using 1 <;>
      rw [Ideal.ofList_nil, bot_smul, bot_toAddSubgroup]
  | @cons r s _ _ h _ ih =>
    conv => congr <;> rw [Ideal.ofList_cons, sup_smul, sup_toAddSubgroup,
      ideal_span_singleton_smul, pointwise_smul_toAddSubgroup,
      top_toAddSubgroup, AddSubgroup.pointwise_smul_def]
    apply DFunLike.ext (f.comp (toAddMonoidEnd R M r))
      ((toAddMonoidEnd S M₂ s).comp f) at h
    rw [AddSubgroup.map_sup, ih, map_map, h, ← map_map,
      map_top_of_surjective f hf]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h :
  List.Forall₂
    (fun (r : R) (s : S) ↦ ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
    as bs
nil :
  AddSubgroup.map f
      (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (Ideal.ofList []) ⊤).toAddSubgroup =
    (HSMul.hSMul.{u_2, u_4, u_4} (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList []) ⊤).toAddSubgroup
⊢ AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList as) ⊤).toAddSubgroup =
    (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList bs) ⊤).toAddSubgroup
have cons : ∀ {r : R} {s : S} {l₁ : List R} {l₂ : List S}
  (h : ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)),
  List.Forall₂
      (fun (r : R) (s : S) ↦
        ∀ (x : M), (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂))
      l₁ l₂ →
    ∀
      (ih :
        AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup =
          (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup),
      AddSubgroup.map f (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (r :: l₁)) ⊤).toAddSubgroup =
        (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (s :: l₂)) ⊤).toAddSubgroup
Tactic: induction h with
  | nil =>
    convert! AddSubgroup.map_bot f using 1 <;>
      rw [Ideal.ofList_nil, bot_smul, bot_toAddSubgroup]
  | @cons r s _ _ h _ ih =>
    conv => congr <;> rw [Ideal.ofList_cons, sup_smul, sup_toAddSubgroup,
      ideal_span_singleton_smul, pointwise_smul_toAddSubgroup,
      top_toAddSubgroup, AddSubgroup.pointwise_smul_def]
    apply DFunLike.ext (f.comp (toAddMonoidEnd R M r))
      ((toAddMonoidEnd S M₂ s).comp f) at h
    rw [AddSubgroup.map_sup, ih, map_map, h, ← map_map,
      map_top_of_surjective f hf]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
| IsWeaklyRegular M as ↔ IsWeaklyRegular M₂ bs
have a : IsWeaklyRegular M as
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
| IsWeaklyRegular M as ↔ IsWeaklyRegular M₂ bs
have b : IsWeaklyRegular M₂ bs
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
| IsWeaklyRegular M as
have a : ∀ (i : Fin as.length),
  IsSMulRegular.{u_1, u_3}
    (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (List.take (↑i : ℕ) as)) ⊤)
    (getElem (valid := fun (xs : List R) (i : Fin as.length) ↦ (↑i : ℕ) < xs.length) as i sorry)
Tactic: rw [isWeaklyRegular_iff_Fin]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
| IsWeaklyRegular M₂ bs
have b : ∀ (i : Fin bs.length),
  IsSMulRegular.{u_2, u_4}
    (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (List.take (↑i : ℕ) bs)) ⊤)
    (getElem (valid := fun (xs : List S) (i : Fin bs.length) ↦ (↑i : ℕ) < xs.length) bs i sorry)
Tactic: rw [isWeaklyRegular_iff_Fin]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
| IsWeaklyRegular M as ↔ IsWeaklyRegular M₂ bs
have a : ∀ (i : Fin as.length),
  IsSMulRegular.{u_1, u_3}
    (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (List.take (↑i : ℕ) as)) ⊤)
    (getElem (valid := fun (xs : List R) (i : Fin as.length) ↦ (↑i : ℕ) < xs.length) as i sorry)
Tactic: congr <;> rw [isWeaklyRegular_iff_Fin]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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 :
  ∀ (i : Fin as.length),
    IsSMulRegular.{u_1, u_3}
      (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (List.take (↑i : ℕ) as)) ⊤)
      (getElem (valid := fun (xs : List R) (i : Fin as.length) ↦ (↑i : ℕ) < xs.length) as i ⋯)
| IsWeaklyRegular M as ↔ IsWeaklyRegular M₂ bs
have b : ∀ (i : Fin bs.length),
  IsSMulRegular.{u_2, u_4}
    (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (List.take (↑i : ℕ) bs)) ⊤)
    (getElem (valid := fun (xs : List S) (i : Fin bs.length) ↦ (↑i : ℕ) < xs.length) bs i sorry)
Tactic: congr <;> rw [isWeaklyRegular_iff_Fin]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
⊢ IsWeaklyRegular M as ↔ IsWeaklyRegular M₂ bs
have conv : (∀ (i : Fin as.length),
    IsSMulRegular.{u_1, u_3}
      (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (List.take (↑i : ℕ) as)) ⊤)
      (getElem (valid := fun (xs : List R) (i : Fin as.length) ↦ (↑i : ℕ) < xs.length) as i sorry)) ↔
  ∀ (i : Fin bs.length),
    IsSMulRegular.{u_2, u_4}
      (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (List.take (↑i : ℕ) bs)) ⊤)
      (getElem (valid := fun (xs : List S) (i : Fin bs.length) ↦ (↑i : ℕ) < xs.length) bs i sorry)
Tactic: conv => congr <;> rw [isWeaklyRegular_iff_Fin]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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' : (i : ℕ) →
  AddEquiv.{u_3, u_4} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (List.take i as)) ⊤)
    (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (List.take i bs)) ⊤) :=
  fun (i : ℕ) ↦
    QuotientAddGroup.congr
      (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (List.take i as)) ⊤).toAddSubgroup
      (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (List.take i bs)) ⊤).toAddSubgroup e ⋯
⊢ (∀ (i : Fin as.length),
      IsSMulRegular.{u_1, u_3}
        (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (List.take (↑i : ℕ) as)) ⊤)
        (getElem (valid := fun (xs : List R) (i : Fin as.length) ↦ (↑i : ℕ) < xs.length) as i ⋯)) ↔
    ∀ (i : Fin bs.length),
      IsSMulRegular.{u_2, u_4}
        (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (List.take (↑i : ℕ) bs)) ⊤)
        (getElem (valid := fun (xs : List S) (i : Fin bs.length) ↦ (↑i : ℕ) < xs.length) bs i ⋯)
have refine : ∀ (x : Fin as.length)
  (x_1 : M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (List.take (↑x : ℕ) as)) ⊤),
  ((AddEquiv.toEquiv (e' (↑x : ℕ)) :
          Equiv.{u_3 + 1, u_4 + 1}
            (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (List.take (↑x : ℕ) as)) ⊤)
            (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (List.take (↑x : ℕ) bs)) ⊤)) :
        (a : M ⧸ Ideal.ofList (List.take (↑x : ℕ) as) • ⊤) → M₂ ⧸ Ideal.ofList (List.take (↑x : ℕ) bs) • ⊤)
      (getElem (valid := fun (xs : List R) (i : Fin as.length) ↦ (↑i : ℕ) < xs.length) as x sorry • x_1) =
    HSMul.hSMul (β := M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (List.take (↑x : ℕ) bs)) ⊤)
      (getElem (idx := Fin bs.length) (valid := fun (xs : List S) (i : Fin bs.length) ↦ (↑i : ℕ) < xs.length) bs
        ((finCongr sorry : (a : Fin as.length) → Fin bs.length) x : Fin bs.length) sorry)
      (((AddEquiv.toEquiv (e' (↑x : ℕ)) :
              Equiv.{u_3 + 1, u_4 + 1}
                (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList (List.take (↑x : ℕ) as)) ⊤)
                (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (List.take (↑x : ℕ) bs)) ⊤)) :
            (a : M ⧸ Ideal.ofList (List.take (↑x : ℕ) as) • ⊤) → M₂ ⧸ Ideal.ofList (List.take (↑x : ℕ) bs) • ⊤)
          x_1 :
        M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (List.take (↑x : ℕ) bs)) ⊤)
Tactic: refine (finCongr h.length_eq).forall_congr @fun _ => (e' _).isSMulRegular_congr ?_
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
| IsRegular M as ↔ IsRegular M₂ bs
have a : IsRegular M as
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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 : IsRegular M as
| IsRegular M as ↔ IsRegular M₂ bs
have b : IsRegular M₂ bs
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
| IsRegular M as
have a : IsWeaklyRegular M as ∧ Nontrivial.{u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList as) ⊤)
Tactic: rw [isRegular_iff, ne_comm, ← Quotient.nontrivial_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
| IsRegular M₂ bs
have b : IsWeaklyRegular M₂ bs ∧ Nontrivial.{u_4} (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList bs) ⊤)
Tactic: rw [isRegular_iff, ne_comm, ← Quotient.nontrivial_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
| IsRegular M as ↔ IsRegular M₂ bs
have a : IsWeaklyRegular M as ∧ Nontrivial.{u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList as) ⊤)
Tactic: congr <;> rw [isRegular_iff, ne_comm, ← Quotient.nontrivial_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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) ⊤)
| IsRegular M as ↔ IsRegular M₂ bs
have b : IsWeaklyRegular M₂ bs ∧ Nontrivial.{u_4} (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList bs) ⊤)
Tactic: congr <;> rw [isRegular_iff, ne_comm, ← Quotient.nontrivial_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
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
⊢ IsRegular M as ↔ IsRegular M₂ bs
have 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) ⊤)
Tactic: conv => congr <;> rw [isRegular_iff, ne_comm, ← Quotient.nontrivial_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
rs : List R
⊢ IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsRegular.{u_1, u_3} (QuotSMulTop r M) rs
have 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
Tactic: rw [isRegular_iff, isRegular_iff, isWeaklyRegular_cons_iff M r rs,
    ne_eq, top_eq_ofList_cons_smul_iff, and_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
rs : List R
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
⊢ IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsRegular.{u_1, u_3} (QuotSMulTop r M) rs
have 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) ⊤
Tactic: rw [isRegular_iff, isRegular_iff, isWeaklyRegular_cons_iff M r rs,
    ne_eq, top_eq_ofList_cons_smul_iff, and_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
rs : List R
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) ⊤
⊢ IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsRegular.{u_1, u_3} (QuotSMulTop r M) rs
have rw₂ : (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs) ∧
    ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R 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) ⊤
Tactic: rw [isRegular_iff, isRegular_iff, isWeaklyRegular_cons_iff M r rs,
    ne_eq, top_eq_ofList_cons_smul_iff, and_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
rs : List R
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) ⊤
⊢ IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsRegular.{u_1, u_3} (QuotSMulTop r M) rs
have rw₃ : (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs) ∧
    ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R 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) ⊤
Tactic: rw [isRegular_iff, isRegular_iff, isWeaklyRegular_cons_iff M r rs,
    ne_eq, top_eq_ofList_cons_smul_iff, and_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.RegularSequence (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
rs : List R
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) ⊤
⊢ IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsRegular.{u_1, u_3} (QuotSMulTop r M) rs
have rw₄ : (IsSMulRegular M r ∧ IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs) ∧
    ¬⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤ ↔
  IsSMulRegular M r ∧
    IsWeaklyRegular.{u_1, u_3} (QuotSMulTop r M) rs ∧
      ⊤ ≠ HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop r M)) (Ideal.ofList rs) ⊤
Tactic: rw [isRegular_iff, isRegular_iff, isWeaklyRegular_cons_iff M r rs,
    ne_eq, top_eq_ofList_cons_smul_iff, and_assoc]