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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
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₂)
h_1 :
  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
a :
  AddSubgroup.map (G := M₂)
      (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
    (HSMul.hSMul (α := Submodule S S) (β := Submodule S M₂) (Ideal.ofList l₂) ⊤).toAddSubgroup
| (HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList (s :: l₂)) ⊤).toAddSubgroup

Tactic:
rw [Ideal.ofList_cons, sup_smul, sup_toAddSubgroup,
      ideal_span_singleton_smul, pointwise_smul_toAddSubgroup,
      top_toAddSubgroup, AddSubgroup.pointwise_smul_def]

Premises used: Submodule.ideal_span_singleton_smul, Submodule.pointwise_smul_toAddSubgroup, Submodule.top_toAddSubgroup, Submodule.sup_smul, Ideal.ofList_cons, AddSubgroup.pointwise_smul_def, Submodule.sup_toAddSubgroup
-- 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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
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₂)
h_1 :
  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
a :
  AddSubgroup.map f
    (AddSubgroup.map (G := M)
        (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤ ⊔
      (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup)
a₁ :
  AddSubgroup.map (G := M₂)
      (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
    (HSMul.hSMul (α := Submodule S 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:
congr <;> rw [Ideal.ofList_cons, sup_smul, sup_toAddSubgroup,
      ideal_span_singleton_smul, pointwise_smul_toAddSubgroup,
      top_toAddSubgroup, AddSubgroup.pointwise_smul_def]

Premises used: Submodule.ideal_span_singleton_smul, Submodule.pointwise_smul_toAddSubgroup, Submodule.top_toAddSubgroup, Submodule.sup_smul, Ideal.ofList_cons, AddSubgroup.pointwise_smul_def, Submodule.sup_toAddSubgroup
-- 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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
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₂)
h_1 :
  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
cons :
  AddSubgroup.map f
      (AddSubgroup.map (G := M)
          (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) ⊤ ⊔
        (HSMul.hSMul (α := Submodule R R) (β := Submodule R M) (Ideal.ofList l₁) ⊤).toAddSubgroup) =
    AddSubgroup.map (G := M₂)
        (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
      (HSMul.hSMul (α := Submodule S 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:
conv => congr <;> rw [Ideal.ofList_cons, sup_smul, sup_toAddSubgroup,
      ideal_span_singleton_smul, pointwise_smul_toAddSubgroup,
      top_toAddSubgroup, AddSubgroup.pointwise_smul_def]

Premises used: Submodule.ideal_span_singleton_smul, Submodule.pointwise_smul_toAddSubgroup, Submodule.top_toAddSubgroup, Submodule.sup_smul, Ideal.ofList_cons, AddSubgroup.pointwise_smul_def, Submodule.sup_toAddSubgroup
-- 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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
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₂)
h_1 :
  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
⊢ f.comp (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r) =
    AddMonoidHom.comp
      (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) f

Tactic:
apply DFunLike.ext (f.comp (toAddMonoidEnd R M r))
      ((toAddMonoidEnd S M₂ s).comp f) at h

Premises used: DFunLike.ext, AddMonoidHom.comp, DFunLike.coe, DistribMulAction.toAddMonoidEnd
-- 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₂
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
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
⊢ 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

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]

Premises used: Submodule.ideal_span_singleton_smul, AddSubgroup.map_map, Submodule.pointwise_smul_toAddSubgroup, AddSubgroup.map_top_of_surjective, Submodule.bot_smul, Submodule.top_toAddSubgroup, Submodule.sup_smul, AddSubgroup.map_bot, Ideal.ofList_nil, Ideal.ofList_cons, AddSubgroup.pointwise_smul_def, Submodule.sup_toAddSubgroup, AddSubgroup.map_sup, Submodule.bot_toAddSubgroup
-- 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
b : IsWeaklyRegular M₂ bs
| IsWeaklyRegular M as ↔ IsWeaklyRegular M₂ bs

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

Tactic:
rw [isWeaklyRegular_iff_Fin]

Premises used: RingTheory.Sequence.isWeaklyRegular_iff_Fin
-- 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
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 ⋯)
| IsWeaklyRegular M₂ bs

Tactic:
rw [isWeaklyRegular_iff_Fin]

Premises used: RingTheory.Sequence.isWeaklyRegular_iff_Fin
-- 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 :
  ∀ (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 ⋯)
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 ⋯)
| IsWeaklyRegular M as ↔ IsWeaklyRegular M₂ bs

Tactic:
congr <;> rw [isWeaklyRegular_iff_Fin]

Premises used: RingTheory.Sequence.isWeaklyRegular_iff_Fin
-- 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 :
  (∀ (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 ⋯)
⊢ IsWeaklyRegular M as ↔ IsWeaklyRegular M₂ bs

Tactic:
conv => congr <;> rw [isWeaklyRegular_iff_Fin]

Premises used: RingTheory.Sequence.isWeaklyRegular_iff_Fin
-- 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' : (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 ⋯)

Tactic:
(finCongr h.length_eq).forall_congr @fun _ => (e' _).isSMulRegular_congr ?_

Premises used: Equiv.isSMulRegular_congr, finCongr, Equiv.forall_congr, List.Forall₂.length_eq
-- 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' : (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 ⋯
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 ⋯ • 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 ⋯ : (a : Fin as.length) → Fin bs.length) x : Fin bs.length) ⋯)
        (((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)) ⊤)
⊢ (∀ (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 ⋯)

Tactic:
refine (finCongr h.length_eq).forall_congr @fun _ => (e' _).isSMulRegular_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' : (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 ⋯
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 ⋯ • 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 ⋯ : (a : Fin as.length) → Fin bs.length) x : Fin bs.length) ⋯)
        (((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:
(mkQ_surjective _).forall.mpr fun _ => congrArg (mkQ _) (h.get _ _ _)

Premises used: Iff.mpr, Function.Surjective.forall, congrArg, finCongr, Fin.val, RingTheory.Sequence.isWeaklyRegular_iff_Fin._proof_2, Ideal.ofList, Submodule.mkQ, HSMul.hSMul, Submodule.mkQ_surjective, Top.top, List.take, DFunLike.coe, List.Forall₂.get, List.Forall₂.length_eq
-- 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
⊢ IsWeaklyRegular M rs ↔ IsWeaklyRegular.{u_2, u_4} (R := S) M₂ (List.map (⇑σ : (a : R) → S) rs)

Tactic:
e.toAddEquiv.isWeaklyRegular_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, List.forall₂_same, LinearEquiv.toLinearMap, AddEquiv.isWeaklyRegular_congr, 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
⊢ IsWeaklyRegular M rs ↔ IsWeaklyRegular M₂ rs

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

Premises used: congrArg, List.map_id, LinearEquiv.isWeaklyRegular_congr', Iff.trans, iff_of_eq
-- 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 : IsRegular M as
b : IsRegular M₂ bs
| IsRegular M as ↔ IsRegular M₂ bs

Tactic:
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
a : IsWeaklyRegular M as ∧ Nontrivial.{u_3} (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ideal.ofList as) ⊤)
| IsRegular M as

Tactic:
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
b : IsWeaklyRegular M₂ bs ∧ Nontrivial.{u_4} (M₂ ⧸ HSMul.hSMul (α := Ideal S) (β := Submodule S M₂) (Ideal.ofList bs) ⊤)
| IsRegular M₂ bs

Tactic:
rw [isRegular_iff, ne_comm, ← Quotient.nontrivial_iff]

Premises used: RingTheory.Sequence.isRegular_iff, ne_comm, Submodule.Quotient.nontrivial_iff