-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
X : C
M N : PresheafOfModules R
g : M ⟶ N
f : (free R).obj (Functor.obj yoneda (F.obj X)) ⟶ M
dsimp :
  Eq (α :=
    (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app (op X)))) ((pushforward₀Obj F R N).obj (op X))) :
      Type u))
    ((freeYonedaEquiv :
          (a : freeObj (yoneda.obj X) ⟶ (pushforward φ).obj N) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app (op X)))).obj ((pushforward₀Obj F R N).obj (op X))) :
              Type u))
        (((Equiv.trans freeYonedaEquiv (Equiv.symm freeYonedaEquiv) :
                (freeObj (Functor.obj yoneda (F.obj X)) ⟶ N) ≃
                  (freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj N)) :
              (a : freeObj (yoneda.obj (F.obj X)) ⟶ N) → freeObj (yoneda.obj X) ⟶ (pushforward φ).obj N)
            (f ≫ g) :
          freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj N) :
      (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app (op X))))
            ((pushforward₀Obj F R N).obj (op X))) :
        Type u))
    ((freeYonedaEquiv :
          (a : freeObj (yoneda.obj X) ⟶ (pushforward φ).obj N) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app (op X)))).obj ((pushforward₀Obj F R N).obj (op X))) :
              Type u))
        (({
                toFun := fun (g_1 : freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj M) ↦
                  g_1 ≫ (pushforward φ).map g } :
              (a : freeObj (yoneda.obj X) ⟶ (pushforward φ).obj M) → freeObj (yoneda.obj X) ⟶ (pushforward φ).obj N)
            (((Equiv.trans freeYonedaEquiv (Equiv.symm freeYonedaEquiv) :
                    (freeObj (Functor.obj yoneda (F.obj X)) ⟶ M) ≃
                      (freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj M)) :
                  (a : freeObj (yoneda.obj (F.obj X)) ⟶ M) → freeObj (yoneda.obj X) ⟶ (pushforward φ).obj M)
                f :
              freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj M) :
          freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj N) :
      (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app (op X))))
            ((pushforward₀Obj F R N).obj (op X))) :
        Type u))
⊢ Eq (α := (↑(((pushforward φ).obj N).obj (op X)) : Type u))
    ((freeYonedaEquiv :
          (a : (free S).obj (yoneda.obj X) ⟶ (pushforward φ).obj N) → (↑(((pushforward φ).obj N).obj (op X)) : Type u))
        (((Equiv.trans freeYonedaEquiv (Equiv.symm freeYonedaEquiv) :
                ((free R).obj (Functor.obj yoneda (F.obj X)) ⟶ N) ≃
                  (pushforward φ ⋙ Functor.obj coyoneda (op ((free S).obj (Functor.obj yoneda X)))).obj N) :
              (a : (free R).obj (yoneda.obj (F.obj X)) ⟶ N) →
                (pushforward φ ⋙ coyoneda.obj (op ((free S).obj (yoneda.obj X)))).obj N)
            (f ≫ g) :
          (pushforward φ ⋙ Functor.obj coyoneda (op ((free S).obj (Functor.obj yoneda X)))).obj N) :
      (↑(((pushforward φ).obj N).obj (op X)) : Type u))
    ((freeYonedaEquiv :
          (a : (free S).obj (yoneda.obj X) ⟶ (pushforward φ).obj N) → (↑(((pushforward φ).obj N).obj (op X)) : Type u))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((pushforward φ ⋙ Functor.obj coyoneda (op ((free S).obj (Functor.obj yoneda X)))).map g) :
              (a : (fun (X : Type u) ↦ X) ((pushforward φ ⋙ coyoneda.obj (op ((free S).obj (yoneda.obj X)))).obj M)) →
                (fun (X : Type u) ↦ X) ((pushforward φ ⋙ coyoneda.obj (op ((free S).obj (yoneda.obj X)))).obj N))
            (((Equiv.trans freeYonedaEquiv (Equiv.symm freeYonedaEquiv) :
                    ((free R).obj (Functor.obj yoneda (F.obj X)) ⟶ M) ≃
                      (pushforward φ ⋙ Functor.obj coyoneda (op ((free S).obj (Functor.obj yoneda X)))).obj M) :
                  (a : (free R).obj (yoneda.obj (F.obj X)) ⟶ M) →
                    (pushforward φ ⋙ coyoneda.obj (op ((free S).obj (yoneda.obj X)))).obj M)
                f :
              (pushforward φ ⋙ Functor.obj coyoneda (op ((free S).obj (Functor.obj yoneda X)))).obj M) :
          (fun (X : Type u) ↦ X)
            ((pushforward φ ⋙ Functor.obj coyoneda (op ((free S).obj (Functor.obj yoneda X)))).obj N)) :
      (↑(((pushforward φ).obj N).obj (op X)) : Type u))

Tactic:
dsimp