-- 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 : (colimitCocone F).pt ⟶ t.pt
h : ∀ (j : J), (colimitCocone F).ι.app j ≫ x = t.ι.app j
hf :
  ∀ (x_1 : (↑(colimitCocone F).pt : Type (max u v))) (j : J)
    (x_2 :
      ((((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 : (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_2)) :
        (↑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_2)) :
        (↑t.pt : Type (max u v)))
⊢ x = colimitDesc F t

Tactic:
ext ⟨j, x⟩