-- 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
r : R
x y : (j : J) × (↑(F.obj j) : Type (max u v))
k : J
f :
  x.fst (β := 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)).obj
        j) ⟶
    k
g :
  y.fst (β := 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)).obj
        j) ⟶
    k
hfg :
  Eq (α :=
    (fun (X : Type (max u v)) ↦ X)
      ((F ⋙
            forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
              (CC := carrier)).obj
        k))
    ((hom (FC := TypeCat.Fun)
            ((F ⋙
                  forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                    (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)).map
              f) :
          (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget (ModuleCat R)).obj x.fst)) →
            (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget (ModuleCat R)).obj k))
        (x.snd (β := 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)).obj
            j)) :
      (fun (X : Type (max u v)) ↦ X)
        ((F ⋙
              forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)).obj
          k))
    ((hom (FC := TypeCat.Fun)
            ((F ⋙
                  forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                    (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)).map
              g) :
          (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget (ModuleCat R)).obj y.fst)) →
            (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget (ModuleCat R)).obj k))
        (y.snd (β := 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)).obj
            j)) :
      (fun (X : Type (max u v)) ↦ X)
        ((F ⋙
              forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)).obj
          k))
⊢ Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
      (F.obj k))
    ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj x.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
        (x.snd (β := fun (j : J) ↦
          ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
            (F.obj j))) :
      (↑(F.obj k) : Type (max u v)))
    ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
            (F.map g) :
          (a : (↑(F.obj y.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
        (y.snd (β := fun (j : J) ↦
          ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
            (F.obj j))) :
      (↑(F.obj k) : Type (max u v)))

Tactic:
simp only [Functor.comp_obj, Functor.comp_map, ConcreteCategory.hom_ofHom,
    TypeCat.Fun.coe_mk] at hfg

Premises used: CategoryTheory.Functor.comp_obj, TypeCat.Fun.coe_mk, CategoryTheory.ConcreteCategory.hom_ofHom, CategoryTheory.Functor.comp_map