-- 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))
    ((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))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(S.obj (op X)) : Type u)) ↦
            LinearMap (R := (↑(S.obj (op X)) : Type u)) (RingHom.id (↑(S.obj (op X)) : Type u)) (↑x1 : Type u)
              (↑x2 : Type u))
            (CC := ModuleCat.carrier) (((pushforward φ).map g).app (op X)) :
          (a : (↑(((pushforward φ).obj M).obj (op X)) : Type u)) → (↑(((pushforward φ).obj N).obj (op X)) : Type u))
        ((freeYonedaEquiv :
              (a : (free S).obj (yoneda.obj X) ⟶ (pushforward φ).obj M) →
                (↑(((pushforward φ).obj M).obj (op X)) : Type u))
            (((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) :
          (↑(((pushforward φ).obj M).obj (op X)) : Type u)) :
      (↑(((pushforward φ).obj 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))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(S.obj (op X)) : Type u)) ↦
          LinearMap (R := (↑(S.obj (op X)) : Type u)) (RingHom.id (↑(S.obj (op X)) : Type u)) (↑x1 : Type u)
            (↑x2 : Type u))
          (CC := ModuleCat.carrier) (((pushforward φ).map g).app (op X)) :
        (a : (↑(((pushforward φ).obj M).obj (op X)) : Type u)) → (↑(((pushforward φ).obj N).obj (op X)) : Type u))
      ((freeYonedaEquiv : (a : freeObj (yoneda.obj (F.obj X)) ⟶ M) → (↑(M.obj (op (F.obj X))) : Type u)) f :
        (↑(M.obj (op (F.obj X))) : Type u)) :
    (↑(((pushforward φ).obj N).obj (op X)) : Type u))
Tactic: erw [Equiv.apply_symm_apply]