-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
F : PresheafOfModules R
G : ModuleCat (↑cR.pt : Type w)
β : F ⟶ (constFunctor cR).obj G
X : Cᵒᵖ
m : (↑(F.obj X) : Type w)
⊢ Eq (α := (↑G : Type w))
    ((@ConcreteCategory.hom.{w, w, w + 1, w} _ (ModuleCat.moduleCategory (↑cR.pt : Type w))
            (fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
              LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w) (↑x2 : Type w))
            ModuleCat.carrier
            (fun (X Y : ModuleCat (↑cR.pt : Type w)) ↦
              (LinearMap.instFunLike :
                FunLike (LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑X : Type w) (↑Y : Type w))
                  (↑X : Type w) (↑Y : Type w)))
            _ ((colimitFunctor hcR).obj F) _
            ((Equiv.symm (Adjunction.homEquiv (colimitAdjunction hcR) F G) :
                  (a : F ⟶ (constFunctor cR).obj G) → (colimitFunctor hcR).obj F ⟶ G)
                β :
              (colimitFunctor hcR).obj F ⟶ G) :
          (a : (↑((colimitFunctor hcR).obj F) : Type w)) → (↑G : Type w))
        ((ιM : (a : (↑(F.obj X) : Type w)) → ModuleColimit hcR (colimit.isColimit F.presheaf)) m :
          ModuleColimit (cM := colimit.cocone F.presheaf) hcR (colimit.isColimit F.presheaf)) :
      (↑G : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type w)) ↦
            LinearMap (R := (↑(R.obj X) : Type w)) (RingHom.id (↑(R.obj X) : Type w)) (↑x1 : Type w) (↑x2 : Type w))
            (CC := ModuleCat.carrier) (β.app X) :
          (a : (↑(F.obj X) : Type w)) → (↑(((constFunctor cR).obj G).obj X) : Type w))
        m :
      (↑(((constFunctor cR).obj G).obj X) : Type w))
have rw : Eq (α := (↑G : Type w))
  ((@ConcreteCategory.hom.{w, w, w + 1, w} _ (ModuleCat.moduleCategory (↑cR.pt : Type w))
          (fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
            LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w) (↑x2 : Type w))
          ModuleCat.carrier
          (fun (X Y : ModuleCat (↑cR.pt : Type w)) ↦
            (LinearMap.instFunLike :
              FunLike (LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑X : Type w) (↑Y : Type w))
                (↑X : Type w) (↑Y : Type w)))
          _ ((colimitFunctor hcR).obj F) _
          (((↑(homEquiv hcR (colimit.isColimit F.presheaf)) :
                    (ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR (colimit.isColimit F.presheaf)) ⟶ G) ≃
                      (F ⟶ (constFunctor cR).obj G)).symm :
                (a : F ⟶ (constFunctor cR).obj G) → (colimitFunctor hcR).obj F ⟶ G)
              β :
            (colimitFunctor hcR).obj F ⟶ G) :
        (a : (↑((colimitFunctor hcR).obj F) : Type w)) → (↑G : Type w))
      ((ιM : (a : (↑(F.obj X) : Type w)) → ModuleColimit hcR (colimit.isColimit F.presheaf)) m :
        ModuleColimit (cM := colimit.cocone F.presheaf) hcR (colimit.isColimit F.presheaf)) :
    (↑G : Type w))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type w)) ↦
          LinearMap (R := (↑(R.obj X) : Type w)) (RingHom.id (↑(R.obj X) : Type w)) (↑x1 : Type w) (↑x2 : Type w))
          (CC := ModuleCat.carrier) (β.app X) :
        (a : (↑(F.obj X) : Type w)) → (↑(((constFunctor cR).obj G).obj X) : Type w))
      m :
    (↑(((constFunctor cR).obj G).obj X) : Type w))
Tactic: rw [colimitAdjunction_homEquiv]