-- 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
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
V U : Cᵒᵖ
f : V ⟶ U
⊢ Eq (α :=
    (tensorObj (𝒞 := Functor.category)
            (R ⋙
              forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier))
            (M.presheaf ⋙
              forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                AddCommGrpCat.carrier))).obj
        V ⟶
      Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (ModuleColimit hcR hcM)) U)
    ((tensorObj (𝒞 := Functor.category)
            (R ⋙
              forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier))
            (M.presheaf ⋙
              forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                AddCommGrpCat.carrier))).map
        f ≫
      ↾fun
          (x :
            (tensorObj (𝒞 := Functor.category)
                  (R ⋙
                    forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                      RingCat.carrier))
                  (M.presheaf ⋙
                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                      AddCommGrpCat.carrier))).obj
              U) ↦
        match (motive :=
          (tensorObj (𝒞 := Functor.category)
                  (R ⋙
                    forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                      RingCat.carrier))
                  (M.presheaf ⋙
                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                      AddCommGrpCat.carrier))).obj
              U →
            Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (ModuleColimit hcR hcM)) U)
          x with
        | (r, m) =>
          (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                AddCommGrpCat.carrier) (cM.ι.app U) :
              (a : (↑(M.presheaf.obj U) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cM.pt).obj U) : Type w))
            (r • m))
    ((↾fun
          (x :
            (tensorObj (𝒞 := Functor.category)
                  (R ⋙
                    forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                      RingCat.carrier))
                  (M.presheaf ⋙
                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                      AddCommGrpCat.carrier))).obj
              V) ↦
        match (motive :=
          (tensorObj (𝒞 := Functor.category)
                  (R ⋙
                    forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                      RingCat.carrier))
                  (M.presheaf ⋙
                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                      AddCommGrpCat.carrier))).obj
              V →
            Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (ModuleColimit hcR hcM)) V)
          x with
        | (r, m) =>
          (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                AddCommGrpCat.carrier) (cM.ι.app V) :
              (a : (↑(M.presheaf.obj V) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cM.pt).obj V) : Type w))
            (r • m)) ≫
      CategoryTheory.Functor.map (Functor.obj (Functor.const Cᵒᵖ) (ModuleColimit hcR hcM)) f)
have h : ∀
  (r :
    (R ⋙ forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier)).obj
      V)
  (m :
    (M.presheaf ⋙
          forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier)).obj
      V),
  Eq (α := Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (ModuleColimit hcR hcM)) U)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((tensorObj (𝒞 := Functor.category)
                (R ⋙
                  forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                    RingCat.carrier))
                (M.presheaf ⋙
                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                    AddCommGrpCat.carrier))).map
            f ≫
          ↾fun
              (x :
                (tensorObj (𝒞 := Functor.category)
                      (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                          RingCat.carrier))
                      (M.presheaf ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                          AddCommGrpCat.carrier))).obj
                  U) ↦
            match (motive :=
              (tensorObj (𝒞 := Functor.category)
                      (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                          RingCat.carrier))
                      (M.presheaf ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                          AddCommGrpCat.carrier))).obj
                  U →
                Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (ModuleColimit hcR hcM)) U)
              x with
            | (r, m) =>
              (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                    AddCommGrpCat.carrier) (cM.ι.app U) :
                  (a : (↑(M.presheaf.obj U) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cM.pt).obj U) : Type w))
                (r • m)))
      (r, m))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun
              (x :
                (tensorObj (𝒞 := Functor.category)
                      (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                          RingCat.carrier))
                      (M.presheaf ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                          AddCommGrpCat.carrier))).obj
                  V) ↦
            match (motive :=
              (tensorObj (𝒞 := Functor.category)
                      (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                          RingCat.carrier))
                      (M.presheaf ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                          AddCommGrpCat.carrier))).obj
                  V →
                Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (ModuleColimit hcR hcM)) V)
              x with
            | (r, m) =>
              (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                    AddCommGrpCat.carrier) (cM.ι.app V) :
                  (a : (↑(M.presheaf.obj V) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cM.pt).obj V) : Type w))
                (r • m)) ≫
          CategoryTheory.Functor.map (Functor.obj (Functor.const Cᵒᵖ) (ModuleColimit hcR hcM)) f))
      (r, m))
Tactic: ext ⟨r, m⟩