awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : PresheafOfModules R
φ :
  F ⟶
    G.presheaf ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
X Y : Cᵒᵖ
f : X ⟶ Y
h :
  ∀ (x : F.obj X),
    Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
              LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
              (CC := ModuleCat.carrier) (X := Functor.obj (ModuleCat.free (↑(R.obj X) : Type u)) (F.obj X))
              (ModuleCat.freeDesc
                  (↾fun (x : F.obj X) ↦
                    ModuleCat.freeMk
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj Y) x)) ≫
                (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (ModuleCat.freeDesc (φ.app Y))) :
            (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
          (ModuleCat.freeMk x) :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
              LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
              (CC := ModuleCat.carrier) (ModuleCat.freeDesc (φ.app X) ≫ G.map f) :
            (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
          (ModuleCat.freeMk x) :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
⊢ ModuleCat.freeDesc
        (↾fun (x : F.obj X) ↦
          ModuleCat.freeMk ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj Y) x)) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (ModuleCat.freeDesc (φ.app Y)) =
    ModuleCat.freeDesc (φ.app X) ≫ G.map f

Tactic:
ext x
-- 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 : PresheafOfModules R
φ :
  F ⟶
    G.presheaf ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
X Y : Cᵒᵖ
f : X ⟶ Y
x : F.obj X
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
            LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (X := Functor.obj (ModuleCat.free (↑(R.obj X) : Type u)) (F.obj X))
            (ModuleCat.freeDesc
                (↾fun (x : F.obj X) ↦
                  ModuleCat.freeMk ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj Y) x)) ≫
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (ModuleCat.freeDesc (φ.app Y))) :
          (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
        (ModuleCat.freeMk x) :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
            LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (ModuleCat.freeDesc (φ.app X) ≫ G.map f) :
          (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))
        (ModuleCat.freeMk x) :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (G.obj Y)) : Type u))

Tactic:
simpa using NatTrans.naturality_apply φ f x

Premises used: CategoryTheory.NatTrans.naturality_apply
-- 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 : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
h :
  ∀ (x : F.obj X),
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f ≫ ↾fun (x : F.obj Y) ↦ ModuleCat.freeMk x)) x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (x : F.obj X) ↦ ModuleCat.freeMk x) ≫
            (presheaf (R := R) (freeObj F) ⋙
                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                    AddCommGrpCat.carrier)).map
              f))
        x
⊢ (F.map f ≫ ↾fun (x : F.obj Y) ↦ ModuleCat.freeMk x) =
    (↾fun (x : F.obj X) ↦ ModuleCat.freeMk x) ≫
      (presheaf (R := R) (freeObj F) ⋙
            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier)).map
        f

Tactic:
ext
-- 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 : PresheafOfModules R
ψ : freeObj F ⟶ G
h :
  ∀ (X : Cᵒᵖ),
    Hom.app
        ((fun
              (φ :
                F ⟶
                  G.presheaf ⋙
                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                      AddCommGrpCat.carrier)) ↦
            freeObjDesc φ)
          ((fun (ψ : freeObj F ⟶ G) ↦
              freeAdjunctionUnit R F ≫
                Functor.whiskerRight ((toPresheaf R).map ψ)
                  (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                    AddCommGrpCat.carrier)))
            ψ))
        X =
      ψ.app X
⊢ (fun
          (φ :
            F ⟶
              G.presheaf ⋙
                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier)) ↦
        freeObjDesc φ)
      ((fun (ψ : freeObj F ⟶ G) ↦
          freeAdjunctionUnit R F ≫
            Functor.whiskerRight ((toPresheaf R).map ψ)
              (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier)))
        ψ) =
    ψ

Tactic:
ext1 X
-- 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 : PresheafOfModules R
ψ : freeObj F ⟶ G
X : Cᵒᵖ
h :
  ModuleCat.freeDesc
      (CategoryStruct.comp (Y := (↑(Functor.obj (ModuleCat.free (↑(R.obj X) : Type u)) (F.obj X)) : Type u))
        (↾fun (x : F.obj X) ↦ ModuleCat.freeMk x)
        (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) (((toPresheaf R).map ψ).app X)) :
            (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) → (↑(G.obj X) : Type u)))) =
    ψ.app X
⊢ Hom.app
      ((fun
            (φ :
              F ⟶
                G.presheaf ⋙
                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                    AddCommGrpCat.carrier)) ↦
          freeObjDesc φ)
        ((fun (ψ : freeObj F ⟶ G) ↦
            freeAdjunctionUnit R F ≫
              Functor.whiskerRight ((toPresheaf R).map ψ)
                (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier)))
          ψ))
      X =
    ψ.app X

Tactic:
dsimp
-- 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 : PresheafOfModules R
ψ : freeObj F ⟶ G
X : Cᵒᵖ
h :
  ∀ (x : F.obj X),
    Eq (α := (↑(G.obj X) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
              LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
              (CC := ModuleCat.carrier) (X := Functor.obj (ModuleCat.free (↑(R.obj X) : Type u)) (F.obj X)) (Y :=
              G.obj X)
              (ModuleCat.freeDesc
                (CategoryStruct.comp (Y := (↑(Functor.obj (ModuleCat.free (↑(R.obj X) : Type u)) (F.obj X)) : Type u))
                  (↾fun (x : F.obj X) ↦ ModuleCat.freeMk x)
                  (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
                          (CC := AddCommGrpCat.carrier) (((toPresheaf R).map ψ).app X)) :
                      (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) →
                        (↑(G.obj X) : Type u))))) :
            (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) → (↑(G.obj X) : Type u))
          (ModuleCat.freeMk x) :
        (↑(G.obj X) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
              LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
              (CC := ModuleCat.carrier) (ψ.app X) :
            (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) → (↑(G.obj X) : Type u))
          (ModuleCat.freeMk x) :
        (↑(G.obj X) : Type u))
⊢ ModuleCat.freeDesc
      (CategoryStruct.comp (Y := (↑(Functor.obj (ModuleCat.free (↑(R.obj X) : Type u)) (F.obj X)) : Type u))
        (↾fun (x : F.obj X) ↦ ModuleCat.freeMk x)
        (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) (((toPresheaf R).map ψ).app X)) :
            (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) → (↑(G.obj X) : Type u)))) =
    ψ.app X

Tactic:
ext x
-- 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 : PresheafOfModules R
ψ : freeObj F ⟶ G
X : Cᵒᵖ
x : F.obj X
⊢ Eq (α := (↑(G.obj X) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
            LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (X := Functor.obj (ModuleCat.free (↑(R.obj X) : Type u)) (F.obj X)) (Y := G.obj X)
            (ModuleCat.freeDesc
              (CategoryStruct.comp (Y := (↑(Functor.obj (ModuleCat.free (↑(R.obj X) : Type u)) (F.obj X)) : Type u))
                (↾fun (x : F.obj X) ↦ ModuleCat.freeMk x)
                (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
                        (CC := AddCommGrpCat.carrier) (((toPresheaf R).map ψ).app X)) :
                    (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) →
                      (↑(G.obj X) : Type u))))) :
          (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) → (↑(G.obj X) : Type u))
        (ModuleCat.freeMk x) :
      (↑(G.obj X) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
            LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (ψ.app X) :
          (a : (↑((ModuleCat.free (↑(R.obj X) : Type u)).obj (F.obj X)) : Type u)) → (↑(G.obj X) : Type u))
        (ModuleCat.freeMk x) :
      (↑(G.obj X) : Type u))

Tactic:
simp [toPresheaf]

Premises used: PresheafOfModules.toPresheaf
-- 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 : PresheafOfModules R
φ :
  F ⟶
    G.presheaf ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
w :
  ∀ (x : Cᵒᵖ) (x_1 : F.obj x),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun (ψ : freeObj F ⟶ G) ↦
                freeAdjunctionUnit R F ≫
                  Functor.whiskerRight ((toPresheaf R).map ψ)
                    (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                      AddCommGrpCat.carrier)))
              ((fun
                    (φ :
                      F ⟶
                        G.presheaf ⋙
                          forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                            AddCommGrpCat.carrier)) ↦
                  freeObjDesc φ)
                φ))
            x))
        x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app x)).toFun x_1
⊢ (fun (ψ : freeObj F ⟶ G) ↦
        freeAdjunctionUnit R F ≫
          Functor.whiskerRight ((toPresheaf R).map ψ)
            (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier)))
      ((fun
            (φ :
              F ⟶
                G.presheaf ⋙
                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                    AddCommGrpCat.carrier)) ↦
          freeObjDesc φ)
        φ) =
    φ

Tactic:
ext
-- 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 : PresheafOfModules R
φ :
  F ⟶
    G.presheaf ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
x : Cᵒᵖ
x_1 : F.obj x
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (ψ : freeObj F ⟶ G) ↦
              freeAdjunctionUnit R F ≫
                Functor.whiskerRight ((toPresheaf R).map ψ)
                  (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                    AddCommGrpCat.carrier)))
            ((fun
                  (φ :
                    F ⟶
                      G.presheaf ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                          AddCommGrpCat.carrier)) ↦
                freeObjDesc φ)
              φ))
          x))
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app x)).toFun x_1

Tactic:
simp [toPresheaf]

Premises used: PresheafOfModules.toPresheaf
-- 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 : PresheafOfModules R
ψ ψ' : freeObj F ⟶ G
h :
  freeAdjunctionUnit R F ≫
      Functor.whiskerRight ((toPresheaf R).map ψ)
        (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 ψ')
        (forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier))
⊢ ψ = ψ'

Tactic:
freeHomEquiv.injective h

Premises used: Equiv.injective, PresheafOfModules.freeHomEquiv
-- 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
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)

Tactic:
simp [freeHomEquiv, toPresheaf]

Premises used: PresheafOfModules.toPresheaf, PresheafOfModules.freeHomEquiv
-- 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 : PresheafOfModules R
⊢ (freeAdjunction R).homEquiv F G = freeHomEquiv

Tactic:
simp [freeAdjunction, Adjunction.mkOfHomEquiv_homEquiv]

Premises used: PresheafOfModules.freeAdjunction, CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
-- 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)
⊢ (freeAdjunction R).unit.app F = freeAdjunctionUnit R F

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, ModuleCat.freeMk, TypeCat.Fun.comp, PresheafOfModules.freeObj, PresheafOfModules.freeAdjunctionUnit, rfl, Finsupp.single
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C : Type u
inst : Category.{v, u} C
R : CategoryTheory.Functor.{v, v, u, v + 1} Cᵒᵖ RingCat
M : PresheafOfModules R
X : C
x : (↑(M.obj (Opposite.op X)) : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj (Opposite.op X)) : Type v)) ↦
          LinearMap (R := (↑(R.obj (Opposite.op X)) : Type v)) (RingHom.id (↑(R.obj (Opposite.op X)) : Type v))
            (↑x1 : Type v) (↑x2 : Type v))
          (CC := ModuleCat.carrier) (X := ((free R).obj (Functor.obj yoneda X)).obj (Opposite.op X)) (Y :=
          M.obj (Opposite.op X))
          (Hom.app
            ((Equiv.symm freeYonedaEquiv : (a : (↑(M.obj (Opposite.op X)) : Type v)) → (free R).obj (yoneda.obj X) ⟶ M)
              x)
            (Opposite.op X)) :
        (a : (↑(((free R).obj (yoneda.obj X)).obj (Opposite.op X)) : Type v)) → (↑(M.obj (Opposite.op X)) : Type v))
      (ModuleCat.freeMk (𝟙 (Opposite.unop (Opposite.op X)))) =
    x

Tactic:
simp [freeYonedaEquiv, freeHomEquiv, yonedaEquiv]

Premises used: CategoryTheory.yonedaEquiv, PresheafOfModules.freeHomEquiv, PresheafOfModules.freeYonedaEquiv
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C : Type u
inst : Category.{v, u} C
R : CategoryTheory.Functor.{v, v, u, v + 1} Cᵒᵖ RingCat
M N : PresheafOfModules R
X : C
m : (free R).obj (Functor.obj yoneda X) ⟶ M
φ : M ⟶ N
⊢ Eq.{v + 1} (α := (↑(N.obj (Opposite.op X)) : Type v))
    ((freeYonedaEquiv : (a : (free R).obj (yoneda.obj X) ⟶ N) → (↑(N.obj (Opposite.op X)) : Type v)) (m ≫ φ) :
      (↑(N.obj (Opposite.op X)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj (Opposite.op X)) : Type v)) ↦
            LinearMap (R := (↑(R.obj (Opposite.op X)) : Type v)) (RingHom.id (↑(R.obj (Opposite.op X)) : Type v))
              (↑x1 : Type v) (↑x2 : Type v))
            (CC := ModuleCat.carrier) (φ.app (Opposite.op X)) :
          (a : (↑(M.obj (Opposite.op X)) : Type v)) → (↑(N.obj (Opposite.op X)) : Type v))
        ((freeYonedaEquiv : (a : (free R).obj (yoneda.obj X) ⟶ M) → (↑(M.obj (Opposite.op X)) : Type v)) m :
          (↑(M.obj (Opposite.op X)) : Type v)) :
      (↑(N.obj (Opposite.op X)) : Type v))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C : Type u
inst : Category.{v, u} C
R : CategoryTheory.Functor.{v, v, u, v + 1} Cᵒᵖ RingCat
⊢ ObjectProperty.Small.{u, max u v, max u (v + 1)} (ObjectProperty.ofObj (yoneda ⋙ free R).obj)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Goal:
C : Type u
inst : Category.{v, u} C
R : CategoryTheory.Functor.{v, v, u, v + 1} Cᵒᵖ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ (G : PresheafOfModules R), freeYoneda R G → ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
h₁ :
  ∀ (X : C) (m : (↑(M.obj (Opposite.op X)) : Type v)),
    Eq (α := (↑(N.obj (Opposite.op X)) : Type v))
      ((ModuleCat.Hom.hom (f₁.app (Opposite.op X)) :
            (a : (↑(M.obj (Opposite.op X)) : Type v)) → (↑(N.obj (Opposite.op X)) : Type v))
          m :
        (↑(N.obj (Opposite.op X)) : Type v))
      ((ModuleCat.Hom.hom (f₂.app (Opposite.op X)) :
            (a : (↑(M.obj (Opposite.op X)) : Type v)) → (↑(N.obj (Opposite.op X)) : Type v))
          m :
        (↑(N.obj (Opposite.op X)) : Type v))
⊢ f₁ = f₂

Tactic:
ext ⟨X⟩ m