awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
M : PresheafOfModules R
s : M.sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ HSMul.hSMul (α := (↑(R.obj Y) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
              (R.map f) :
            (a : (↑(R.obj X) : Type u)) → (↑(R.obj Y) : Type u))
          1 :
        (↑(R.obj Y) : Type u))
      (s.eval Y) =
    (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) (M.map f) :
        (a : (↑(M.obj X) : Type u)) →
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
      (HSMul.hSMul (α := (↑(R.obj X) : Type u)) 1 (s.eval X))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
M : PresheafOfModules R
f : unit R ⟶ M
h :
  ∀ (X : Cᵒᵖ),
    ModuleCat.Hom.hom
        (Hom.app
          ((fun (s : M.sections) ↦
              ({
                  app := fun (X : Cᵒᵖ) ↦
                    ModuleCat.ofHom
                      ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                          (a : (↑(M.obj X) : Type u)) →
                            (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                        ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)),
                  naturality := ⋯ } :
                (unit R).Hom M))
            ((fun (f : unit R ⟶ M) ↦
                sectionsMk
                  (fun (X : Cᵒᵖ) ↦
                    (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) (f.app X) :
                        (a : (↑((unit R).obj X) : Type u)) → (↑(M.obj X) : Type u))
                      1)
                  ⋯)
              f))
          X) =
      ModuleCat.Hom.hom (f.app X)
⊢ (fun (s : M.sections) ↦
        ({
            app := fun (X : Cᵒᵖ) ↦
              ModuleCat.ofHom
                ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                    (a : (↑(M.obj X) : Type u)) → (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                  ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)),
            naturality := ⋯ } :
          (unit R).Hom M))
      ((fun (f : unit R ⟶ M) ↦
          sectionsMk
            (fun (X : Cᵒᵖ) ↦
              (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) (f.app X) :
                  (a : (↑((unit R).obj X) : Type u)) → (↑(M.obj X) : Type u))
                1)
            ⋯)
        f) =
    f

Tactic:
ext X : 2
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
M : PresheafOfModules R
f : unit R ⟶ M
X : Cᵒᵖ
⊢ ModuleCat.Hom.hom
      (Hom.app
        ((fun (s : M.sections) ↦
            ({
                app := fun (X : Cᵒᵖ) ↦
                  ModuleCat.ofHom
                    ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                        (a : (↑(M.obj X) : Type u)) →
                          (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                      ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)),
                naturality := ⋯ } :
              (unit R).Hom M))
          ((fun (f : unit R ⟶ M) ↦
              sectionsMk
                (fun (X : Cᵒᵖ) ↦
                  (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) (f.app X) :
                      (a : (↑((unit R).obj X) : Type u)) → (↑(M.obj X) : Type u))
                    1)
                ⋯)
            f))
        X) =
    ModuleCat.Hom.hom (f.app X)

Tactic:
(LinearMap.ringLmapEquivSelf (R.obj X) ℤ (M.obj X)).symm_apply_apply (f.app X).hom

Premises used: LinearMap.ringLmapEquivSelf, LinearEquiv.symm_apply_apply, Int, PresheafOfModules.obj, ModuleCat.carrier, ModuleCat.Hom.hom, PresheafOfModules.Hom.app, RingCat.carrier, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
M : PresheafOfModules R
f : unit R ⟶ M
X : Cᵒᵖ
⊢ ModuleCat.Hom.hom
      (Hom.app
        ((fun (s : M.sections) ↦
            ({
                app := fun (X : Cᵒᵖ) ↦
                  ModuleCat.ofHom
                    ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                        (a : (↑(M.obj X) : Type u)) →
                          (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                      ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)),
                naturality := ⋯ } :
              (unit R).Hom M))
          ((fun (f : unit R ⟶ M) ↦
              sectionsMk
                (fun (X : Cᵒᵖ) ↦
                  (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) (f.app X) :
                      (a : (↑((unit R).obj X) : Type u)) → (↑(M.obj X) : Type u))
                    1)
                ⋯)
            f))
        X) =
    ModuleCat.Hom.hom (f.app X)

Tactic:
exact (LinearMap.ringLmapEquivSelf (R.obj X) ℤ (M.obj X)).symm_apply_apply (f.app X).hom

Premises used: LinearMap.ringLmapEquivSelf, LinearEquiv.symm_apply_apply, Int, PresheafOfModules.obj, ModuleCat.carrier, ModuleCat.Hom.hom, PresheafOfModules.Hom.app, RingCat.carrier, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
M : PresheafOfModules R
s : M.sections
h :
  ∀ (X : Cᵒᵖ),
    (↑((fun (f : unit R ⟶ M) ↦
                sectionsMk
                  (fun (X : Cᵒᵖ) ↦
                    (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) (f.app X) :
                        (a : (↑((unit R).obj X) : Type u)) → (↑(M.obj X) : Type u))
                      1)
                  ⋯)
              ((fun (s : M.sections) ↦
                  ({
                      app := fun (X : Cᵒᵖ) ↦
                        ModuleCat.ofHom
                          ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                              (a : (↑(M.obj X) : Type u)) →
                                (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                            ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)),
                      naturality := ⋯ } :
                    (unit R).Hom M))
                s)) :
          (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j)
        X =
      (↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X
⊢ (fun (f : unit R ⟶ M) ↦
        sectionsMk
          (fun (X : Cᵒᵖ) ↦
            (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) (f.app X) :
                (a : (↑((unit R).obj X) : Type u)) → (↑(M.obj X) : Type u))
              1)
          ⋯)
      ((fun (s : M.sections) ↦
          ({
              app := fun (X : Cᵒᵖ) ↦
                ModuleCat.ofHom
                  ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                      (a : (↑(M.obj X) : Type u)) →
                        (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                    ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)),
              naturality := ⋯ } :
            (unit R).Hom M))
        s) =
    s

Tactic:
ext X
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
M : PresheafOfModules R
s : M.sections
X : Cᵒᵖ
⊢ (↑((fun (f : unit R ⟶ M) ↦
              sectionsMk
                (fun (X : Cᵒᵖ) ↦
                  (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) (f.app X) :
                      (a : (↑((unit R).obj X) : Type u)) → (↑(M.obj X) : Type u))
                    1)
                ⋯)
            ((fun (s : M.sections) ↦
                ({
                    app := fun (X : Cᵒᵖ) ↦
                      ModuleCat.ofHom
                        ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                            (a : (↑(M.obj X) : Type u)) →
                              (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                          ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)),
                    naturality := ⋯ } :
                  (unit R).Hom M))
              s)) :
        (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j)
      X =
    (↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X

Tactic:
(LinearMap.ringLmapEquivSelf (R.obj X) ℤ (M.obj X)).apply_symm_apply (s.val X)

Premises used: LinearMap.ringLmapEquivSelf, Int, PresheafOfModules.obj, LinearEquiv.apply_symm_apply, ModuleCat.carrier, Subtype.val, RingCat.carrier, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
M : PresheafOfModules R
s : M.sections
X : Cᵒᵖ
⊢ (↑((fun (f : unit R ⟶ M) ↦
              sectionsMk
                (fun (X : Cᵒᵖ) ↦
                  (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) (f.app X) :
                      (a : (↑((unit R).obj X) : Type u)) → (↑(M.obj X) : Type u))
                    1)
                ⋯)
            ((fun (s : M.sections) ↦
                ({
                    app := fun (X : Cᵒᵖ) ↦
                      ModuleCat.ofHom
                        ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                            (a : (↑(M.obj X) : Type u)) →
                              (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                          ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)),
                    naturality := ⋯ } :
                  (unit R).Hom M))
              s)) :
        (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j)
      X =
    (↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X

Tactic:
exact (LinearMap.ringLmapEquivSelf (R.obj X) ℤ (M.obj X)).apply_symm_apply (s.val X)

Premises used: LinearMap.ringLmapEquivSelf, Int, PresheafOfModules.obj, LinearEquiv.apply_symm_apply, ModuleCat.carrier, Subtype.val, RingCat.carrier, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
X : Cᵒᵖ
hX : Limits.IsInitial.{v₁, u₁} X
M : PresheafOfModules.{v, v₁, u₁, u} R
Y : Cᵒᵖ
⊢ (↑(forgetToPresheafModuleCatObjObj X hX M Y) : Type v) = (↑(M.obj Y) : Type v)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
X : Cᵒᵖ
hX : Limits.IsInitial.{v₁, u₁} X
M : PresheafOfModules.{v, v₁, u₁, u} R
Y Z : Cᵒᵖ
f : Y ⟶ Z
⊢ ∀ (x y : (↑(forgetToPresheafModuleCatObjObj X hX M Y) : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M.map f) :
          (a : (↑(M.obj Y) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
        (x + y) =
      HAdd.hAdd (α := (↑(forgetToPresheafModuleCatObjObj X hX M Z) : Type v)) (β :=
        (↑(forgetToPresheafModuleCatObjObj X hX M Z) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (M.map f) :
              (a : (↑(M.obj Y) : Type v)) →
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
            x :
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (M.map f) :
              (a : (↑(M.obj Y) : Type v)) →
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
            y :
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
X : Cᵒᵖ
hX : Limits.IsInitial.{v₁, u₁} X
M : PresheafOfModules.{v, v₁, u₁, u} R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : (↑(R.obj X) : Type u)
x : (↑(forgetToPresheafModuleCatObjObj X hX M Y) : Type v)
e_a : hX.to Y ≫ f = hX.to Z
⊢ HSMul.hSMul (α := (↑(R.obj Z) : Type u)) (β :=
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
      ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
              (R.map (hX.to Y ≫ f)) :
            (a : (↑(R.obj X) : Type u)) → (↑(R.obj Z) : Type u))
          r :
        (↑(R.obj Z) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M.map f) :
            (a : (↑(M.obj Y) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v)) =
    HSMul.hSMul (α := (↑(R.obj Z) : Type u)) (β := (↑(M.obj Z) : Type v))
      ((RingCat.Hom.hom (R.map (hX.to Z)) : (a : (↑(R.obj X) : Type u)) → (↑(R.obj Z) : Type u)) r :
        (↑(R.obj Z) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M.map f) :
            (a : (↑(M.obj Y) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))

Tactic:
congr
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
X : Cᵒᵖ
hX : Limits.IsInitial.{v₁, u₁} X
M : PresheafOfModules.{v, v₁, u₁, u} R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : (↑(R.obj X) : Type u)
x : (↑(forgetToPresheafModuleCatObjObj X hX M Y) : Type v)
⊢ hX.to Y ≫ f = hX.to Z

Tactic:
apply hX.hom_ext

Premises used: CategoryTheory.Limits.IsInitial.hom_ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
X : Cᵒᵖ
hX : Limits.IsInitial.{v₁, u₁} X
M : PresheafOfModules.{v, v₁, u₁, u} R
Y Z : Cᵒᵖ
f : Y ⟶ Z
m : (↑(M.obj Y) : Type v)
⊢ Eq (α := (↑(forgetToPresheafModuleCatObjObj X hX M Z) : Type v))
    ((ModuleCat.Hom.hom (forgetToPresheafModuleCatObjMap X hX M f) :
          (a : (↑(forgetToPresheafModuleCatObjObj X hX M Y) : Type v)) →
            (↑(forgetToPresheafModuleCatObjObj X hX M Z) : Type v))
        m :
      (↑(forgetToPresheafModuleCatObjObj X hX M Z) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M.map f) :
          (a : (↑(M.obj Y) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
        m :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
X_1 : Cᵒᵖ
hX_1 : Limits.IsInitial.{v₁, u₁} X_1
X : Cᵒᵖ
hX : Limits.IsInitial.{v₁, u₁} X
M N : PresheafOfModules.{v, v₁, u₁, u} R
f : M ⟶ N
Y : Cᵒᵖ
⊢ ∀ (x y : (↑((forgetToPresheafModuleCatObj X hX M).obj Y) : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (f.app Y) :
          (a : (↑(M.obj Y) : Type v)) → (↑(N.obj Y) : Type v))
        (x + y) =
      HAdd.hAdd (α := (↑((forgetToPresheafModuleCatObj X hX N).obj Y) : Type v)) (β :=
        (↑((forgetToPresheafModuleCatObj X hX N).obj Y) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (f.app Y) :
              (a : (↑(M.obj Y) : Type v)) → (↑(N.obj Y) : Type v))
            x :
          (↑(N.obj Y) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (f.app Y) :
              (a : (↑(M.obj Y) : Type v)) → (↑(N.obj Y) : Type v))
            y :
          (↑(N.obj Y) : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
X_1 : Cᵒᵖ
hX_1 : Limits.IsInitial.{v₁, u₁} X_1
X : Cᵒᵖ
hX : Limits.IsInitial.{v₁, u₁} X
M N : PresheafOfModules.{v, v₁, u₁, u} R
f : M ⟶ N
Y Z : Cᵒᵖ
g : Y ⟶ Z
x : (↑((forgetToPresheafModuleCatObj X hX M).obj Y) : Type v)
⊢ Eq (α := (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))
    ((ModuleCat.Hom.hom
            ((forgetToPresheafModuleCatObj X hX M).map g ≫
              ModuleCat.ofHom
                {
                  toFun :=
                    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Z) : Type u)) ↦
                          LinearMap.{u, u, v, v} (R := (↑(R.obj Z) : Type u)) (RingHom.id (↑(R.obj Z) : Type u))
                            (↑x1 : Type v) (↑x2 : Type v))
                          (CC := ModuleCat.carrier) (f.app Z)) :
                      (a : (↑(M.obj Z) : Type v)) → (↑(N.obj Z) : Type v)),
                  map_add' := ⋯, map_smul' := ⋯ }) :
          (a : (↑((forgetToPresheafModuleCatObj X hX M).obj Y) : Type v)) →
            (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))
        x :
      (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                {
                  toFun :=
                    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
                          LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u))
                            (↑x1 : Type v) (↑x2 : Type v))
                          (CC := ModuleCat.carrier) (f.app Y)) :
                      (a : (↑(M.obj Y) : Type v)) → (↑(N.obj Y) : Type v)),
                  map_add' := ⋯, map_smul' := ⋯ } ≫
              (forgetToPresheafModuleCatObj X hX N).map g) :
          (a : (↑((forgetToPresheafModuleCatObj X hX M).obj Y) : Type v)) →
            (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))
        x :
      (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))

Tactic:
naturality_apply f g x

Premises used: PresheafOfModules.naturality_apply