-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback (goal)
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
⊢ 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))
have 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))
Tactic: erw [Equiv.apply_symm_apply, freeYonedaEquiv_comp]