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₂ : 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
-- 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ᵒᵖ
⊢ (-f).app X = -f.app X

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 g : M₁ ⟶ M₂
X : Cᵒᵖ
⊢ (f + g).app X = f.app X + g.app X

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 g : M₁ ⟶ M₂
X : Cᵒᵖ
⊢ (f - g).app X = f.app X - g.app X

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
a b c : M₁ ⟶ M₂
h : ∀ (X : Cᵒᵖ), (a + b + c).app X = (a + (b + c)).app X
⊢ a + b + c = a + (b + c)

Tactic:
ext1
-- 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
a b c : M₁ ⟶ M₂
X : Cᵒᵖ
⊢ (a + b + c).app X = (a + (b + c)).app X

Tactic:
simp only [add_app, add_assoc]

Premises used: PresheafOfModules.add_app, add_assoc
-- 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
a : M₁ ⟶ M₂
h : ∀ (X : Cᵒᵖ), (0 + a).app X = a.app X
⊢ 0 + a = a

Tactic:
ext1
-- 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
a : M₁ ⟶ M₂
X : Cᵒᵖ
⊢ (0 + a).app X = a.app X

Tactic:
simp only [add_app, zero_app, zero_add]

Premises used: PresheafOfModules.add_app, zero_add, PresheafOfModules.zero_app
-- 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
a : M₁ ⟶ M₂
h : ∀ (X : Cᵒᵖ), (a + 0).app X = a.app X
⊢ a + 0 = a

Tactic:
ext1
-- 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
a : M₁ ⟶ M₂
X : Cᵒᵖ
⊢ (a + 0).app X = a.app X

Tactic:
simp only [add_app, zero_app, add_zero]

Premises used: PresheafOfModules.add_app, add_zero, PresheafOfModules.zero_app
-- 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
a b : M₁ ⟶ M₂
h : ∀ (X : Cᵒᵖ), (a - b).app X = (a + -b).app X
⊢ a - b = a + -b

Tactic:
ext1
-- 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
a b : M₁ ⟶ M₂
X : Cᵒᵖ
⊢ (a - b).app X = (a + -b).app X

Tactic:
simp only [add_app, sub_app, neg_app, sub_eq_add_neg]

Premises used: PresheafOfModules.add_app, sub_eq_add_neg, PresheafOfModules.neg_app, PresheafOfModules.sub_app
-- 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
a : M₁ ⟶ M₂
h : ∀ (X : Cᵒᵖ), (-a + a).app X = Hom.app 0 X
⊢ -a + a = 0

Tactic:
ext1
-- 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
a : M₁ ⟶ M₂
X : Cᵒᵖ
⊢ (-a + a).app X = Hom.app 0 X

Tactic:
simp only [add_app, neg_app, neg_add_cancel, zero_app]

Premises used: PresheafOfModules.add_app, PresheafOfModules.neg_app, neg_add_cancel, PresheafOfModules.zero_app
-- 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
a b : M₁ ⟶ M₂
h : ∀ (X : Cᵒᵖ), (a + b).app X = (b + a).app X
⊢ a + b = b + a

Tactic:
ext1
-- 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
a b : M₁ ⟶ M₂
X : Cᵒᵖ
⊢ a.app X + b.app X = b.app X + a.app X

Tactic:
apply add_comm

Premises used: add_comm
-- 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
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
hf :
  ∀ (x : (↑(M₁.obj X) : Type v)),
    Eq (α := (↑(M₂.obj X) : Type v))
      ((ModuleCat.Hom.hom ((n • f).app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
        (↑(M₂.obj X) : Type v))
      ((ModuleCat.Hom.hom (n • f.app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
        (↑(M₂.obj X) : Type v))
⊢ (n • f).app X = n • f.app X

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₂ : PresheafOfModules.{v, v₁, u₁, u} R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : (↑(M₁.obj X) : Type v)
hf :
  Eq (α := (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) ((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).map (n • f)) :
          (a : (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₁) : Type v)) →
            (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₂) : Type v))
        x :
      (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
    ((ModuleCat.Hom.hom (n • f.app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
      (↑(M₂.obj X) : Type v))
⊢ Eq (α := (↑(M₂.obj X) : Type v))
    ((ModuleCat.Hom.hom ((n • f).app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
      (↑(M₂.obj X) : Type v))
    ((ModuleCat.Hom.hom (n • f.app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
      (↑(M₂.obj X) : Type v))

Tactic:
change (toPresheaf R ⋙ (evaluation _ _).obj X).map (n • f) x = _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.comp, CategoryTheory.Functor.map, HSMul.hSMul, PresheafOfModules.toPresheaf, CategoryTheory.evaluation, DFunLike.coe, 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₂ : PresheafOfModules.{v, v₁, u₁, u} R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : (↑(M₁.obj X) : Type v)
hf :
  Eq (α := (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (n • (toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).map f) :
          (a : (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₁) : Type v)) →
            (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₂) : Type v))
        x :
      (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
    ((ModuleCat.Hom.hom (n • f.app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
      (↑(M₂.obj X) : Type v))
⊢ Eq (α := (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) ((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).map (n • f)) :
          (a : (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₁) : Type v)) →
            (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₂) : Type v))
        x :
      (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
    ((ModuleCat.Hom.hom (n • f.app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
      (↑(M₂.obj X) : Type v))

Tactic:
rw [Functor.map_zsmul]

Premises used: CategoryTheory.Functor.map_zsmul
-- 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
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : (↑(M₁.obj X) : Type v)
⊢ Eq (α := (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (n • (toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).map f) :
          (a : (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₁) : Type v)) →
            (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₂) : Type v))
        x :
      (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
    ((ModuleCat.Hom.hom (n • f.app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
      (↑(M₂.obj X) : Type v))

Tactic:
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 Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (x y : (↑(R.obj X) : 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))
        (x + y) =
      HAdd.hAdd (α :=
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj
              (ModuleCat.of (↑(R.obj Y) : Type u) (↑(R.obj Y) : Type u))) :
          Type u))
        (β :=
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj
              (ModuleCat.of (↑(R.obj Y) : Type u) (↑(R.obj Y) : Type u))) :
          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))
            x :
          (↑(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))
            y :
          (↑(R.obj Y) : Type u))

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
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((unit R).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) ((unit R).map f) :
          (a : (↑((unit R).obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((unit R).obj Y)) : Type u))
        1 :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((unit R).obj Y)) : Type u))
    (1 : (↑(R.obj Y) : Type u))

Tactic:
(R.map f).hom.map_one

Premises used: RingHom.map_one, CategoryTheory.Functor.map, RingCat.Hom.hom
-- 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
s : M.sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (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) (M.map f) :
        (a : (↑(M.obj X) : Type v)) →
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type v))
      ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X) =
    (↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) Y

Tactic:
s.2 f

Premises used: Subtype.property
-- 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
s t : M.sections
h h₁ :
  ∀ (x : Cᵒᵖ), (↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) x = (↑t : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) x
⊢ (↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) = (↑t : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j)

Tactic:
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
M : PresheafOfModules.{v, v₁, u₁, u} R
s t : M.sections
h :
  ∀ (X : Cᵒᵖ), (↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X = (↑t : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X
x : Cᵒᵖ
⊢ (↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) x = (↑t : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) x

Tactic:
apply h
-- 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 N P : PresheafOfModules.{v, v₁, u₁, u} R
f : M ⟶ N
g : N ⟶ P
s : M.sections
⊢ sectionsMap (f ≫ g) s = sectionsMap g (sectionsMap f s)

Tactic:
rfl

Premises used: PresheafOfModules.sectionsMap, 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 : PresheafOfModules.{v, v₁, u₁, u} R
s : M.sections
⊢ sectionsMap (𝟙 M) s = s

Tactic:
rfl

Premises used: PresheafOfModules.sectionsMk, PresheafOfModules.sectionsMap, rfl, PresheafOfModules.sections
-- 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
hf :
  Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
    ((ModuleCat.Hom.hom
            ((unit R).map f ≫
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                (ModuleCat.ofHom
                  ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj Y) : Type u) ℤ (↑(M.obj Y) : Type u)) :
                      (a : (↑(M.obj Y) : Type u)) →
                        (↑(R.obj Y) : Type u) →ₗ[(↑(R.obj Y) : Type u)] (↑(M.obj Y) : Type u))
                    ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) Y)))) :
          (a : (↑(R.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
        1 :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
    ((ModuleCat.Hom.hom
            (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)) ≫
              M.map f) :
          (a : (↑(R.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
        1 :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
⊢ (unit R).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
        (ModuleCat.ofHom
          ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj Y) : Type u) ℤ (↑(M.obj Y) : Type u)) :
              (a : (↑(M.obj Y) : Type u)) → (↑(R.obj Y) : Type u) →ₗ[(↑(R.obj Y) : Type u)] (↑(M.obj Y) : Type u))
            ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) Y))) =
    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)) ≫
      M.map f

Tactic:
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
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
M : PresheafOfModules R
s : M.sections
X Y : Cᵒᵖ
f : X ⟶ Y
hf :
  HSMul.hSMul (α := (↑(R.obj Y) : Type u))
      ((1 : (a : (↑((unit R).obj Y) : Type u)) → (↑(R.obj Y) : Type u))
          ((ModuleCat.Hom.hom ((unit R).map f) :
                (a : (↑(R.obj X) : Type u)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((unit R).obj Y)) : Type u))
              1 :
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((unit R).obj Y)) : Type u)) :
        (↑(R.obj Y) : Type u))
      ((↑s : (j : Cᵒᵖ) → (↑(M.obj j) : Type u)) Y) =
    (ModuleCat.Hom.hom (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 : (j : Cᵒᵖ) → (↑(M.obj j) : Type u)) X))
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
    ((ModuleCat.Hom.hom
            ((unit R).map f ≫
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                (ModuleCat.ofHom
                  ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj Y) : Type u) ℤ (↑(M.obj Y) : Type u)) :
                      (a : (↑(M.obj Y) : Type u)) →
                        (↑(R.obj Y) : Type u) →ₗ[(↑(R.obj Y) : Type u)] (↑(M.obj Y) : Type u))
                    ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) Y)))) :
          (a : (↑(R.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
        1 :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
    ((ModuleCat.Hom.hom
            (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)) ≫
              M.map f) :
          (a : (↑(R.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
        1 :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))

Tactic:
dsimp
-- 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
hf :
  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))
⊢ HSMul.hSMul (α := (↑(R.obj Y) : Type u))
      ((1 : (a : (↑((unit R).obj Y) : Type u)) → (↑(R.obj Y) : Type u))
          ((ModuleCat.Hom.hom ((unit R).map f) :
                (a : (↑(R.obj X) : Type u)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((unit R).obj Y)) : Type u))
              1 :
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((unit R).obj Y)) : Type u)) :
        (↑(R.obj Y) : Type u))
      ((↑s : (j : Cᵒᵖ) → (↑(M.obj j) : Type u)) Y) =
    (ModuleCat.Hom.hom (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 : (j : Cᵒᵖ) → (↑(M.obj j) : Type u)) X))

Tactic:
change R.map f 1 • s.eval Y = M.map f (1 • s.eval X)

Premises used: PresheafOfModules.map, CategoryTheory.ConcreteCategory.hom, PresheafOfModules.sections.eval, CategoryTheory.Functor.map, HSMul.hSMul, OfNat.ofNat, DFunLike.coe