-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.FilteredColimits (goal)
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
⊢ x = colimitDesc F t
have 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)))
Tactic: ext ⟨j, x⟩