-- Mathlib/RingTheory/Regular/RegularSequence.lean
lemma _root_.AddEquiv.isWeaklyRegular_congr {e : M ≃+ M₂} {as bs}
    (h : List.Forall₂ (fun (r : R) (s : S) => ∀ x, e (r • x) = s • e x) as bs) :
    IsWeaklyRegular M as ↔ IsWeaklyRegular M₂ bs

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs
e' : (i : ℕ) → M ⧸ Ideal.ofList (List.take i as) • ⊤ ≃+ M₂ ⧸ Ideal.ofList (List.take i bs) • ⊤ :=
  fun i =>
    QuotientAddGroup.congr (Ideal.ofList (List.take i as) • ⊤).toAddSubgroup
      (Ideal.ofList (List.take i bs) • ⊤).toAddSubgroup e ⋯
x✝ : Fin as.length
⊢ ∀ (x : M ⧸ Ideal.ofList (List.take (↑x✝) as) • ⊤),
    (e' ↑x✝).toEquiv (as[x✝] • x) = bs[(finCongr ⋯) x✝] • (e' ↑x✝).toEquiv x

Tactic:
exact (mkQ_surjective _).forall.mpr fun _ => congrArg (mkQ _) (h.get _ _ _)

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs
⊢ IsWeaklyRegular M as ↔ IsWeaklyRegular M₂ bs

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

Result:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs
⊢ (∀ (i : Fin as.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take (↑i) as) • ⊤) as[i]) ↔
    ∀ (i : Fin bs.length), IsSMulRegular (M₂ ⧸ Ideal.ofList (List.take (↑i) bs) • ⊤) bs[i]

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs
e' : (i : ℕ) → M ⧸ Ideal.ofList (List.take i as) • ⊤ ≃+ M₂ ⧸ Ideal.ofList (List.take i bs) • ⊤ :=
  fun i =>
    QuotientAddGroup.congr (Ideal.ofList (List.take i as) • ⊤).toAddSubgroup
      (Ideal.ofList (List.take i bs) • ⊤).toAddSubgroup e ⋯
⊢ (∀ (i : Fin as.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take (↑i) as) • ⊤) as[i]) ↔
    ∀ (i : Fin bs.length), IsSMulRegular (M₂ ⧸ Ideal.ofList (List.take (↑i) bs) • ⊤) bs[i]

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

Result:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs
e' : (i : ℕ) → M ⧸ Ideal.ofList (List.take i as) • ⊤ ≃+ M₂ ⧸ Ideal.ofList (List.take i bs) • ⊤ :=
  fun i =>
    QuotientAddGroup.congr (Ideal.ofList (List.take i as) • ⊤).toAddSubgroup
      (Ideal.ofList (List.take i bs) • ⊤).toAddSubgroup e ⋯
x✝ : Fin as.length
⊢ ∀ (x : M ⧸ Ideal.ofList (List.take (↑x✝) as) • ⊤),
    (e' ↑x✝).toEquiv (as[x✝] • x) = bs[(finCongr ⋯) x✝] • (e' ↑x✝).toEquiv x

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs
⊢ (∀ (i : Fin as.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take (↑i) as) • ⊤) as[i]) ↔
    ∀ (i : Fin bs.length), IsSMulRegular (M₂ ⧸ Ideal.ofList (List.take (↑i) bs) • ⊤) bs[i]

Tactic:
let e' i : (M ⧸ (Ideal.ofList (as.take i) • ⊤ : Submodule R M)) ≃+
    M₂ ⧸ (Ideal.ofList (bs.take i) • ⊤ : Submodule S M₂) :=
  QuotientAddGroup.congr _ _ e <|
    AddHom.map_smul_top_toAddSubgroup_of_surjective e.surjective <|
      List.forall₂_take i h

Result:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs
e' : (i : ℕ) → M ⧸ Ideal.ofList (List.take i as) • ⊤ ≃+ M₂ ⧸ Ideal.ofList (List.take i bs) • ⊤ :=
  fun i =>
    QuotientAddGroup.congr (Ideal.ofList (List.take i as) • ⊤).toAddSubgroup
      (Ideal.ofList (List.take i bs) • ⊤).toAddSubgroup e ⋯
⊢ (∀ (i : Fin as.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take (↑i) as) • ⊤) as[i]) ↔
    ∀ (i : Fin bs.length), IsSMulRegular (M₂ ⧸ Ideal.ofList (List.take (↑i) bs) • ⊤) bs[i]