-- 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
erw :
  Eq (α :=
    (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app (op X)))) ((pushforward₀Obj F R N).obj (op X))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj (op (F.obj X))) : Type u)) ↦
            LinearMap (R := (↑(R.obj (op (F.obj X))) : Type u)) (RingHom.id (↑(R.obj (op (F.obj X))) : Type u))
              (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (g.app (op (F.obj X))) :
          (a : (↑(M.obj (op (F.obj X))) : Type u)) → (↑(N.obj (op (F.obj X))) : Type u))
        ((freeYonedaEquiv : (a : (free R).obj (yoneda.obj (F.obj X)) ⟶ M) → (↑(M.obj (op (F.obj X))) : Type u)) f :
          (↑(M.obj (op (F.obj X))) : Type u)) :
      (↑(N.obj (op (F.obj 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 (α :=
    (↑(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))

Tactic:
erw [Equiv.apply_symm_apply, freeYonedaEquiv_comp]

Premises used: Equiv.apply_symm_apply, PresheafOfModules.freeYonedaEquiv_comp