-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator (goal)
Goal:
C : Type u
inst : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ (ConcreteCategory.hom (FC :=
          fun
            (x1 x2 :
              ModuleCat
                (↑(R.obj
                      (m.fst (β := fun (c : Cᵒᵖ) ↦
                        ((toPresheaf R).obj M ⋙
                              forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
                                (CC := AddCommGrpCat.carrier)).obj
                          c))) :
                  Type u)) ↦
          LinearMap (R :=
            (↑(R.obj
                  (m.fst (β := fun (c : Cᵒᵖ) ↦
                    ((toPresheaf R).obj M ⋙
                          forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                            AddCommGrpCat.carrier)).obj
                      c))) :
              Type u))
            (RingHom.id
              (↑(R.obj
                    (m.fst (β := fun (c : Cᵒᵖ) ↦
                      ((toPresheaf R).obj M ⋙
                            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                              AddCommGrpCat.carrier)).obj
                        c))) :
                Type u))
            (↑x1 : Type u) (↑x2 : Type u))
          (CC := ModuleCat.carrier)
          (M.fromFreeYonedaCoproduct.app
            (m.fst (β := fun (c : Cᵒᵖ) ↦
              ((toPresheaf R).obj M ⋙
                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                      AddCommGrpCat.carrier)).obj
                c))) :
        (a : (↑(M.freeYonedaCoproduct.obj m.fst) : Type u)) → (↑(M.obj m.fst) : Type u))
      (M.freeYonedaCoproductMk m) =
    m.snd (β := fun (c : Cᵒᵖ) ↦
      ((toPresheaf R).obj M ⋙
            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier)).obj
        c)
have rw : (ConcreteCategory.hom (FC :=
        fun
          (x1 x2 :
            ModuleCat
              (↑(R.obj
                    (m.fst (β := fun (c : Cᵒᵖ) ↦
                      ((toPresheaf R).obj M ⋙
                            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                              AddCommGrpCat.carrier)).obj
                        c))) :
                Type u)) ↦
        LinearMap (R :=
          (↑(R.obj
                (m.fst (β := fun (c : Cᵒᵖ) ↦
                  ((toPresheaf R).obj M ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                          AddCommGrpCat.carrier)).obj
                    c))) :
            Type u))
          (RingHom.id
            (↑(R.obj
                  (m.fst (β := fun (c : Cᵒᵖ) ↦
                    ((toPresheaf R).obj M ⋙
                          forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                            AddCommGrpCat.carrier)).obj
                      c))) :
              Type u))
          (↑x1 : Type u) (↑x2 : Type u))
        (CC := ModuleCat.carrier)
        (M.fromFreeYonedaCoproduct.app
          (m.fst (β := fun (c : Cᵒᵖ) ↦
            ((toPresheaf R).obj M ⋙
                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                    AddCommGrpCat.carrier)).obj
              c))) :
      (a : (↑(M.freeYonedaCoproduct.obj m.fst) : Type u)) → (↑(M.obj m.fst) : Type u))
    ((ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                ModuleCat
                  (↑(R.obj
                        (m.fst (β := fun (c : Cᵒᵖ) ↦
                          ((toPresheaf R).obj M ⋙
                                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
                                  (CC := AddCommGrpCat.carrier)).obj
                            c))) :
                    Type u)) ↦
            LinearMap (R :=
              (↑(R.obj
                    (m.fst (β := fun (c : Cᵒᵖ) ↦
                      ((toPresheaf R).obj M ⋙
                            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                              AddCommGrpCat.carrier)).obj
                        c))) :
                Type u))
              (RingHom.id
                (↑(R.obj
                      (m.fst (β := fun (c : Cᵒᵖ) ↦
                        ((toPresheaf R).obj M ⋙
                              forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
                                (CC := AddCommGrpCat.carrier)).obj
                          c))) :
                  Type u))
              (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier)
            ((M.ιFreeYonedaCoproduct m).app
              (m.fst (β := fun (c : Cᵒᵖ) ↦
                ((toPresheaf R).obj M ⋙
                      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                        AddCommGrpCat.carrier)).obj
                  c))) :
          (a : (↑(m.freeYoneda.obj m.fst) : Type u)) → (↑(M.freeYonedaCoproduct.obj m.fst) : Type u))
        (ModuleCat.freeMk
          (𝟙
            (Opposite.unop
              (m.fst (β := fun (c : Cᵒᵖ) ↦
                ((toPresheaf R).obj M ⋙
                      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                        AddCommGrpCat.carrier)).obj
                  c))))) :
      (↑(M.freeYonedaCoproduct.obj
            (m.fst (β := fun (c : Cᵒᵖ) ↦
              ((toPresheaf R).obj M ⋙
                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                      AddCommGrpCat.carrier)).obj
                c))) :
        Type u)) =
  m.snd (β := fun (c : Cᵒᵖ) ↦
    ((toPresheaf R).obj M ⋙
          forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier)).obj
      c)
Tactic: rw [freeYonedaCoproductMk, M.ι_fromFreeYonedaCoproduct_apply m, m.fromFreeYoneda_app_apply]