-- 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 (α := (↑(((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))
have 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))
Tactic: dsimp