-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
t : Cocone F
x_1 : (colimitCocone F).pt ⟶ t.pt
h : ∀ (j : J), (colimitCocone F).ι.app j ≫ x_1 = t.ι.app j
x_2 : (↑(colimitCocone F).pt : Type (max u v))
j : J
x :
  ((((F ⋙
              forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier) AddCommGrpCat (FD :=
                fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                AddCommGrpCat.carrier)) ⋙
            forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
              (CC := AddCommGrpCat.carrier) AddGrpCat (FD := fun (x1 x2 : AddGrpCat) ↦
              (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddGrpCat.carrier)) ⋙
          forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
            AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
            (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier)) ⋙
        forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
          AddMonCat.carrier)).obj
    j
⊢ Eq (α := (↑t.pt : Type (max u v)))
    ((Hom.hom x_1 : (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        (Quot.mk
          ((((F ⋙
                    forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                      (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier) AddCommGrpCat (FD :=
                      fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                      AddCommGrpCat.carrier)) ⋙
                  forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                    (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC := AddCommGrpCat.carrier) AddGrpCat (FD :=
                    fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                    AddGrpCat.carrier)) ⋙
                forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
                  (CC := AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
                  (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier)) ⋙
              forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
                AddMonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((((F ⋙
                        forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                          (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier) AddCommGrpCat (FD :=
                          fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                          AddCommGrpCat.carrier)) ⋙
                      forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                        (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC := AddCommGrpCat.carrier) AddGrpCat (FD :=
                        fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                        AddGrpCat.carrier)) ⋙
                    forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
                      (CC := AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
                      (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier)) ⋙
                  forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
                    (CC := AddMonCat.carrier)).obj
              j)
            j x)) :
      (↑t.pt : Type (max u v)))
    ((Hom.hom (colimitDesc F t) : (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        (Quot.mk
          ((((F ⋙
                    forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                      (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier) AddCommGrpCat (FD :=
                      fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                      AddCommGrpCat.carrier)) ⋙
                  forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                    (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC := AddCommGrpCat.carrier) AddGrpCat (FD :=
                    fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                    AddGrpCat.carrier)) ⋙
                forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
                  (CC := AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
                  (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier)) ⋙
              forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
                AddMonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((((F ⋙
                        forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                          (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier) AddCommGrpCat (FD :=
                          fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                          AddCommGrpCat.carrier)) ⋙
                      forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                        (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC := AddCommGrpCat.carrier) AddGrpCat (FD :=
                        fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                        AddGrpCat.carrier)) ⋙
                    forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
                      (CC := AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
                      (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier)) ⋙
                  forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
                    (CC := AddMonCat.carrier)).obj
              j)
            j x)) :
      (↑t.pt : Type (max u v)))

Tactic:
(congr_hom ((forget (ModuleCat _)).congr_map (h j)) _).trans
      (congr_hom ((forget (ModuleCat _)).congr_map (ι_colimitDesc F t j)) x).symm

Premises used: ModuleCat, CategoryTheory.forget, CategoryTheory.Functor.congr_map, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Functor.ιColimitType, Eq.trans