-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
F : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ (Type u)
G_1 : PresheafOfModules R
F₁ F₂ : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ (Type u)
G : PresheafOfModules R
f : F₁ ⟶ F₂
g :
  F₂ ⟶
    (toPresheaf R ⋙
          Functor.obj (Functor.whiskeringRight Cᵒᵖ Ab (Type u))
            (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier))).obj
      G
w :
  ∀ (x : Cᵒᵖ) (x_1 : F₁.obj x),
    Eq (α :=
      ((toPresheaf R).obj G ⋙
            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier)).obj
        x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (freeAdjunctionUnit R F₁ ≫
              Functor.whiskerRight
                ((toPresheaf R).map
                  ((Equiv.symm freeHomEquiv :
                      (a : F₁ ⟶ (toPresheaf R ⋙ (Functor.whiskeringRight Cᵒᵖ Ab (Type u)).obj (forget Ab)).obj G) →
                        (free R).obj F₁ ⟶ G)
                    (f ≫ g)))
                (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier)))
            x))
        x_1)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (freeAdjunctionUnit R F₁ ≫
              Functor.whiskerRight
                ((toPresheaf R).map
                  ((free R).map f ≫
                    (Equiv.symm freeHomEquiv :
                        (a : F₂ ⟶ (toPresheaf R ⋙ (Functor.whiskeringRight Cᵒᵖ Ab (Type u)).obj (forget Ab)).obj G) →
                          (free R).obj F₂ ⟶ G)
                      g))
                (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier)))
            x))
        x_1)
⊢ Eq (α :=
    F₁ ⟶
      (toPresheaf R).obj G ⋙
        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier))
    (freeAdjunctionUnit R F₁ ≫
      Functor.whiskerRight
        ((toPresheaf R).map
          ((Equiv.symm freeHomEquiv :
              (a : F₁ ⟶ (toPresheaf R ⋙ (Functor.whiskeringRight Cᵒᵖ Ab (Type u)).obj (forget Ab)).obj G) →
                (free R).obj F₁ ⟶ G)
            (f ≫ g)))
        (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier)))
    (freeAdjunctionUnit R F₁ ≫
      Functor.whiskerRight
        ((toPresheaf R).map
          ((free R).map f ≫
            (Equiv.symm freeHomEquiv :
                (a : F₂ ⟶ (toPresheaf R ⋙ (Functor.whiskeringRight Cᵒᵖ Ab (Type u)).obj (forget Ab)).obj G) →
                  (free R).obj F₂ ⟶ G)
              g))
        (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier)))

Tactic:
ext