-- 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
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)
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.fromFreeYoneda.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.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.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)
⊢ (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₂ : 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) =
  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]