-- 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_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
h :
  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
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) ⊤) ⊔
      AddSubgroup.map f (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
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 (α := Ideal S) (β := Submodule S 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
cons₂ :
  AddSubgroup.map (G := M)
        (f.comp (((toAddMonoidEnd R M : MonoidHom.{u_1, u_3} R (AddMonoid.End M)) : (a : R) → AddMonoid.End M) r)) ⊤ ⊔
      (HSMul.hSMul (α := Ideal S) (β := Submodule S 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
cons₃ :
  AddSubgroup.map
        (AddMonoidHom.comp
          (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) f)
        ⊤ ⊔
      (HSMul.hSMul (α := Ideal S) (β := Submodule S 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
cons₄ :
  AddSubgroup.map (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s)
        (AddSubgroup.map f ⊤) ⊔
      (HSMul.hSMul (α := Ideal S) (β := Submodule S 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
cons₅ cons₆ :
  AddSubgroup.map (G := M₂)
        (((toAddMonoidEnd S M₂ : MonoidHom.{u_2, u_4} S (AddMonoid.End M₂)) : (a : S) → AddMonoid.End M₂) s) ⊤ ⊔
      (HSMul.hSMul (α := Ideal S) (β := Submodule S 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
      (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

Tactic:
rw [AddSubgroup.map_sup, ih, map_map, h, ← map_map,
      map_top_of_surjective f hf]

Premises used: AddSubgroup.map_map, AddSubgroup.map_top_of_surjective, AddSubgroup.map_sup