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 M₁ M₂ X_1 Y_1 : PresheafOfModules.{v, v₁, u₁, u} R
f : X_1 ⟶ Y_1
X Y : Cᵒᵖ
g : X ⟶ Y
x : (↑(X_1.presheaf.obj X) : Type v)
⊢ Eq (α := (↑(Y_1.presheaf.obj Y) : Type v))
    ((AddCommGrpCat.Hom.hom
            (X_1.presheaf.map g ≫
              AddCommGrpCat.ofHom
                (AddMonoidHom.mk'
                  (⇑(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 : (↑(X_1.obj Y) : Type v)) → (↑(Y_1.obj Y) : Type v))
                  ⋯)) :
          (a : (↑(X_1.presheaf.obj X) : Type v)) → (↑(Y_1.presheaf.obj Y) : Type v))
        x :
      (↑(Y_1.presheaf.obj Y) : Type v))
    ((AddCommGrpCat.Hom.hom
            (AddCommGrpCat.ofHom
                (AddMonoidHom.mk'
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                        LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u))
                          (↑x1 : Type v) (↑x2 : Type v))
                        (CC := ModuleCat.carrier) (f.app X)) :
                    (a : (↑(X_1.obj X) : Type v)) → (↑(Y_1.obj X) : Type v))
                  ⋯) ≫
              Y_1.presheaf.map g) :
          (a : (↑(X_1.presheaf.obj X) : Type v)) → (↑(Y_1.presheaf.obj Y) : Type v))
        x :
      (↑(Y_1.presheaf.obj Y) : Type v))

Tactic:
naturality_apply f g x

Premises used: PresheafOfModules.naturality_apply
-- 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 M₁ M₂ X_1 Y_1 : PresheafOfModules.{v, v₁, u₁, u} R
f : X_1 ⟶ Y_1
X Y : Cᵒᵖ
g : X ⟶ Y
x : (↑(X_1.presheaf.obj X) : Type v)
⊢ Eq (α := (↑(Y_1.presheaf.obj Y) : Type v))
    ((AddCommGrpCat.Hom.hom
            (X_1.presheaf.map g ≫
              AddCommGrpCat.ofHom
                (AddMonoidHom.mk'
                  (⇑(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 : (↑(X_1.obj Y) : Type v)) → (↑(Y_1.obj Y) : Type v))
                  ⋯)) :
          (a : (↑(X_1.presheaf.obj X) : Type v)) → (↑(Y_1.presheaf.obj Y) : Type v))
        x :
      (↑(Y_1.presheaf.obj Y) : Type v))
    ((AddCommGrpCat.Hom.hom
            (AddCommGrpCat.ofHom
                (AddMonoidHom.mk'
                  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                        LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u))
                          (↑x1 : Type v) (↑x2 : Type v))
                        (CC := ModuleCat.carrier) (f.app X)) :
                    (a : (↑(X_1.obj X) : Type v)) → (↑(Y_1.obj X) : Type v))
                  ⋯) ≫
              Y_1.presheaf.map g) :
          (a : (↑(X_1.presheaf.obj X) : Type v)) → (↑(Y_1.presheaf.obj Y) : Type v))
        x :
      (↑(Y_1.presheaf.obj Y) : Type v))

Tactic:
exact naturality_apply f g x

Premises used: PresheafOfModules.naturality_apply
-- 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 : PresheafOfModules.{v, v₁, u₁, u} R
X : Cᵒᵖ
⊢ (↑(((toPresheaf R).obj M).obj X) : Type v) = (↑(M.obj X) : 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₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : (↑(M₁.obj X) : Type v)
⊢ Eq (α := (↑(M₂.obj X) : Type v))
    ((AddCommGrpCat.Hom.hom (((toPresheaf R).map f).app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
      (↑(M₂.obj X) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (f.app X) :
          (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v))
        x :
      (↑(M₂.obj X) : 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 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
x x_1 : PresheafOfModules.{u_1, v₁, u₁, u} R
f g : x ⟶ x_1
h : (toPresheaf R).map f = (toPresheaf R).map g
h₁ :
  ∀ (X : Cᵒᵖ) (x_2 : (↑(x.obj X) : Type u_1)),
    Eq (α := (↑(x_1.obj X) : Type u_1))
      ((ModuleCat.Hom.hom (f.app X) : (a : (↑(x.obj X) : Type u_1)) → (↑(x_1.obj X) : Type u_1)) x_2 :
        (↑(x_1.obj X) : Type u_1))
      ((ModuleCat.Hom.hom (g.app X) : (a : (↑(x.obj X) : Type u_1)) → (↑(x_1.obj X) : Type u_1)) x_2 :
        (↑(x_1.obj X) : Type u_1))
⊢ f = g

Tactic:
ext X 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 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
x_1 x_2 : PresheafOfModules.{u_1, v₁, u₁, u} R
f g : x_1 ⟶ x_2
h : (toPresheaf R).map f = (toPresheaf R).map g
X : Cᵒᵖ
x : (↑(x_1.obj X) : Type u_1)
⊢ Eq (α := (↑(x_2.obj X) : Type u_1))
    ((ModuleCat.Hom.hom (f.app X) : (a : (↑(x_1.obj X) : Type u_1)) → (↑(x_2.obj X) : Type u_1)) x :
      (↑(x_2.obj X) : Type u_1))
    ((ModuleCat.Hom.hom (g.app X) : (a : (↑(x_1.obj X) : Type u_1)) → (↑(x_2.obj X) : Type u_1)) x :
      (↑(x_2.obj X) : Type u_1))

Tactic:
ConcreteCategory.congr_hom (((evaluation _ _).obj X ⋙ forget Ab).congr_map h) x

Premises used: CategoryTheory.Functor.comp, Ab, CategoryTheory.forget, CategoryTheory.Functor.congr_map, CategoryTheory.evaluation, CategoryTheory.ConcreteCategory.congr_hom, 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 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
x_1 x_2 : PresheafOfModules.{u_1, v₁, u₁, u} R
f g : x_1 ⟶ x_2
h : (toPresheaf R).map f = (toPresheaf R).map g
X : Cᵒᵖ
x : (↑(x_1.obj X) : Type u_1)
⊢ Eq (α := (↑(x_2.obj X) : Type u_1))
    ((ModuleCat.Hom.hom (f.app X) : (a : (↑(x_1.obj X) : Type u_1)) → (↑(x_2.obj X) : Type u_1)) x :
      (↑(x_2.obj X) : Type u_1))
    ((ModuleCat.Hom.hom (g.app X) : (a : (↑(x_1.obj X) : Type u_1)) → (↑(x_2.obj X) : Type u_1)) x :
      (↑(x_2.obj X) : Type u_1))

Tactic:
exact ConcreteCategory.congr_hom (((evaluation _ _).obj X ⋙ forget Ab).congr_map h) x

Premises used: CategoryTheory.Functor.comp, Ab, CategoryTheory.forget, CategoryTheory.Functor.congr_map, CategoryTheory.evaluation, CategoryTheory.ConcreteCategory.congr_hom, 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 : CategoryTheory.Functor.{v₁, v, u₁, v + 1} Cᵒᵖ Ab
inst_1 : (X : Cᵒᵖ) → Module.{u, v} (↑(R.obj X) : Type u) (↑(M.obj X) : Type v)
map_smul :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : (↑(R.obj X) : Type u)) (m : (↑(M.obj X) : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (M.map f) :
          (a : (↑(M.obj X) : Type v)) → (↑(M.obj Y) : Type v))
        (r • m) =
      HSMul.hSMul (α := (↑(R.obj Y) : Type u)) (β := (↑(M.obj Y) : Type v))
        ((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))
            r :
          (↑(R.obj Y) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (M.map f) :
              (a : (↑(M.obj X) : Type v)) → (↑(M.obj Y) : Type v))
            m :
          (↑(M.obj Y) : Type v))
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (x y : (↑(M.obj X) : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (M.map f) :
          (a : (↑(M.obj X) : Type v)) → (↑(M.obj Y) : Type v))
        (x + y) =
      HAdd.hAdd (α :=
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj
              (ModuleCat.of (↑(R.obj Y) : Type u) (↑(M.obj Y) : Type v))) :
          Type v))
        (β :=
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj
              (ModuleCat.of (↑(R.obj Y) : Type u) (↑(M.obj Y) : Type v))) :
          Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (M.map f) :
              (a : (↑(M.obj X) : Type v)) → (↑(M.obj Y) : Type v))
            x :
          (↑(M.obj Y) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (M.map f) :
              (a : (↑(M.obj X) : Type v)) → (↑(M.obj Y) : Type v))
            y :
          (↑(M.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 : CategoryTheory.Functor.{v₁, v, u₁, v + 1} Cᵒᵖ Ab
inst_1 : (X : Cᵒᵖ) → Module.{u, v} (↑(R.obj X) : Type u) (↑(M.obj X) : Type v)
map_smul :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : (↑(R.obj X) : Type u)) (m : (↑(M.obj X) : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (M.map f) :
          (a : (↑(M.obj X) : Type v)) → (↑(M.obj Y) : Type v))
        (r • m) =
      HSMul.hSMul (α := (↑(R.obj Y) : Type u)) (β := (↑(M.obj Y) : Type v))
        ((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))
            r :
          (↑(R.obj Y) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (M.map f) :
              (a : (↑(M.obj X) : Type v)) → (↑(M.obj Y) : Type v))
            m :
          (↑(M.obj Y) : Type v))
⊢ (ofPresheaf M map_smul).presheaf = M

Tactic:
rfl

Premises used: AddMonoidHom.mk', rfl, PresheafOfModules.presheaf
-- 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 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
φ : M₁.presheaf ⟶ M₂.presheaf
hφ :
  ∀ (X : Cᵒᵖ) (r : (↑(R.obj X) : Type u)) (m : (↑(M₁.obj X) : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (φ.app X) :
          (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
        (r • m) =
      HSMul.hSMul (β := (↑(M₂.presheaf.obj X) : Type v)) r
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (φ.app X) :
              (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
            m :
          (↑(M₂.presheaf.obj X) : Type v))
X : Cᵒᵖ
⊢ ∀ (x y : (↑(M₁.1 X) : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (φ.app X) :
          (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
        (x + y) =
      HAdd.hAdd (α := (↑(M₂.1 X) : Type v)) (β := (↑(M₂.1 X) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (φ.app X) :
              (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
            x :
          (↑(M₂.presheaf.obj X) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (φ.app X) :
              (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
            y :
          (↑(M₂.presheaf.obj X) : Type v))

Tactic:
simp +instances
-- 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 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
φ : M₁.presheaf ⟶ M₂.presheaf
hφ :
  ∀ (X : Cᵒᵖ) (r : (↑(R.obj X) : Type u)) (m : (↑(M₁.obj X) : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (φ.app X) :
          (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
        (r • m) =
      HSMul.hSMul (β := (↑(M₂.presheaf.obj X) : Type v)) r
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (φ.app X) :
              (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
            m :
          (↑(M₂.presheaf.obj X) : Type v))
X Y : Cᵒᵖ
f : X ⟶ Y
x : (↑(M₁.obj X) : Type v)
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom
            (M₁.map f ≫
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                (ModuleCat.ofHom
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                            (CC := AddCommGrpCat.carrier) (φ.app Y)) :
                        (a : (↑(M₁.presheaf.obj Y) : Type v)) → (↑(M₂.presheaf.obj Y) : Type v)),
                    map_add' := ⋯, map_smul' := ⋯ })) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                {
                  toFun :=
                    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                          (CC := AddCommGrpCat.carrier) (φ.app X)) :
                      (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v)),
                  map_add' := ⋯, map_smul' := ⋯ } ≫
              M₂.map f) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))

Tactic:
CategoryTheory.congr_fun (φ.naturality f) x

Premises used: CategoryTheory.congr_fun, CategoryTheory.NatTrans.naturality
-- 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 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
φ : M₁.presheaf ⟶ M₂.presheaf
hφ :
  ∀ (X : Cᵒᵖ) (r : (↑(R.obj X) : Type u)) (m : (↑(M₁.obj X) : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (φ.app X) :
          (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
        (r • m) =
      HSMul.hSMul (β := (↑(M₂.presheaf.obj X) : Type v)) r
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (φ.app X) :
              (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
            m :
          (↑(M₂.presheaf.obj X) : Type v))
X Y : Cᵒᵖ
f : X ⟶ Y
x : (↑(M₁.obj X) : Type v)
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom
            (M₁.map f ≫
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                (ModuleCat.ofHom
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                            (CC := AddCommGrpCat.carrier) (φ.app Y)) :
                        (a : (↑(M₁.presheaf.obj Y) : Type v)) → (↑(M₂.presheaf.obj Y) : Type v)),
                    map_add' := ⋯, map_smul' := ⋯ })) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                {
                  toFun :=
                    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                          (CC := AddCommGrpCat.carrier) (φ.app X)) :
                      (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v)),
                  map_add' := ⋯, map_smul' := ⋯ } ≫
              M₂.map f) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))

Tactic:
exact CategoryTheory.congr_fun (φ.naturality f) x

Premises used: CategoryTheory.congr_fun, CategoryTheory.NatTrans.naturality
-- 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₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
X : Cᵒᵖ
⊢ Eq.{v + 1} (α := M₁.obj X ⟶ M₂.obj X) (Hom.app 0 X) 0

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 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
X Y : Cᵒᵖ
h : X ⟶ Y
hf :
  ∀ (x : (↑(M₁.obj X) : Type v)),
    Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
      ((ModuleCat.Hom.hom (M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (-f.app Y)) :
            (a : (↑(M₁.obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
      ((ModuleCat.Hom.hom ((-f.app X) ≫ M₂.map h) :
            (a : (↑(M₁.obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
⊢ M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (-f.app Y) = (-f.app X) ≫ M₂.map h

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 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
X Y : Cᵒᵖ
h : X ⟶ Y
x : (↑(M₁.obj X) : Type v)
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom (M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (-f.app Y)) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom ((-f.app X) ≫ M₂.map h) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))

Tactic:
simp [← naturality_apply]

Premises used: PresheafOfModules.naturality_apply
-- 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 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f g : M₁ ⟶ M₂
X Y : Cᵒᵖ
h : X ⟶ Y
hf :
  ∀ (x : (↑(M₁.obj X) : Type v)),
    Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
      ((ModuleCat.Hom.hom (M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (f.app Y + g.app Y)) :
            (a : (↑(M₁.obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
      ((ModuleCat.Hom.hom ((f.app X + g.app X) ≫ M₂.map h) :
            (a : (↑(M₁.obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
⊢ M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (f.app Y + g.app Y) =
    (f.app X + g.app X) ≫ M₂.map h

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 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f g : M₁ ⟶ M₂
X Y : Cᵒᵖ
h : X ⟶ Y
x : (↑(M₁.obj X) : Type v)
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom (M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (f.app Y + g.app Y)) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
    ((ModuleCat.Hom.hom ((f.app X + g.app X) ≫ M₂.map h) :
          (a : (↑(M₁.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).obj (M₂.obj Y)) : Type v))

Tactic:
simp [← naturality_apply]

Premises used: PresheafOfModules.naturality_apply