awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ (X : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((F ⋙ evaluation R X) ⋙
              forget (ModuleCat.{v, u} (↑(R.obj X) : Type u)) (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)).sections :
        Type (max u₂ v))
X : Cᵒᵖ
⊢ PreservesLimit F (evaluation R X)

Tactic:
preservesLimit_of_preserves_limit_cone (isLimitLimitCone F) (limit.isLimit _)

Premises used: PresheafOfModules.isLimitLimitCone, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ (X : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((F ⋙ evaluation R X) ⋙
              forget (ModuleCat.{v, u} (↑(R.obj X) : Type u)) (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)).sections :
        Type (max u₂ v))
⊢ PreservesLimit F (toPresheaf R)

Tactic:
preservesLimit_of_preserves_limit_cone (isLimitLimitCone F)
    (Limits.evaluationJointlyReflectsLimits _
      (fun X => isLimitOfPreserves (evaluation R X ⋙ forget₂ _ AddCommGrpCat)
        (isLimitLimitCone F)))

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsLimits, PresheafOfModules.evaluation, ModuleCat, CategoryTheory.Functor.comp, PresheafOfModules.isLimitLimitCone, CategoryTheory.forget₂, AddCommGrpCat, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CategoryTheory.Limits.isLimitOfPreserves, RingCat.carrier, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
⊢ HasFiniteLimits (PresheafOfModules.{v, v₁, u₁, u} R)

Tactic:
⟨fun _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteLimits.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
M₁ M₂ M₃ M₄ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
X : Cᵒᵖ
m₁ : (↑(M₁.obj X) : Type u)
m₂ : (↑(M₂.obj X) : Type u)
⊢ Eq (α :=
    (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 X)))).obj
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj X) : Type u)) (M₁.obj X)
            (M₂.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 := M₁.obj X)
              (Iso.inv (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 X))) ⋯ (M₁.obj X))) :
            (a : (↑(M₁.obj X) : Type u)) →
              (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 X)))).obj (M₁.obj X)) : Type u))
          m₁ ⊗ₜ[(↑(R.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 := M₂.obj X)
              (Iso.inv (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 X))) ⋯ (M₂.obj X))) :
            (a : (↑(M₂.obj X) : Type u)) →
              (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 X)))).obj (M₂.obj X)) : Type u))
          m₂ :
      TensorProduct (↑(R.obj X) : Type u) (↑(M₁.obj X) : Type u) (↑(M₂.obj X) : Type u))
    (m₁ ⊗ₜ[(↑(R.obj X) : Type u)] m₂ :
      TensorProduct (↑(R.obj X) : Type u) (↑(M₁.obj X) : Type u) (↑(M₂.obj X) : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X₁ Y₁ X₂ Y₂ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
h :
  ∀ (X : Cᵒᵖ),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂).obj X ⟶
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₁ Y₂).obj X)
      (Hom.app (x ⊗ₘ x_1) X) (Hom.app (x ▷ X₂ ≫ Y₁ ◁ x_1) X)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂ ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₁ Y₂)
    (x ⊗ₘ x_1) (x ▷ X₂ ≫ Y₁ ◁ x_1)

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X₁ Y₁ X₂ Y₂ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
X : Cᵒᵖ
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂).obj X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₁ Y₂).obj X)
    (Hom.app (x ⊗ₘ x_1) X) (Hom.app (x ▷ X₂ ≫ Y₁ ◁ x_1) X)

Tactic:
apply tensorHom_def

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
x x_1 :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
h : ∀ (X : Cᵒᵖ), Hom.app (𝟙 x ⊗ₘ 𝟙 x_1) X = Hom.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)) X
⊢ 𝟙 x ⊗ₘ 𝟙 x_1 = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
x x_1 :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
X : Cᵒᵖ
⊢ Hom.app (𝟙 x ⊗ₘ 𝟙 x_1) X = Hom.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)) X

Tactic:
apply id_tensorHom_id

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom_id
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X₁ Y₁ Z₁ X₂ Y₂ Z₂ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
x_2 : Y₁ ⟶ Z₁
x_3 : Y₂ ⟶ Z₂
h :
  ∀ (X : Cᵒᵖ),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂).obj X ⟶
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Z₁ Z₂).obj X)
      (Hom.app ((x ⊗ₘ x_1) ≫ (x_2 ⊗ₘ x_3)) X) (Hom.app (x ≫ x_2 ⊗ₘ x_1 ≫ x_3) X)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂ ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Z₁ Z₂)
    ((x ⊗ₘ x_1) ≫ (x_2 ⊗ₘ x_3)) (x ≫ x_2 ⊗ₘ x_1 ≫ x_3)

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X₁ Y₁ Z₁ X₂ Y₂ Z₂ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
x_2 : Y₁ ⟶ Z₁
x_3 : Y₂ ⟶ Z₂
X : Cᵒᵖ
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂).obj X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Z₁ Z₂).obj X)
    (Hom.app ((x ⊗ₘ x_1) ≫ (x_2 ⊗ₘ x_3)) X) (Hom.app (x ≫ x_2 ⊗ₘ x_1 ≫ x_3) X)

Tactic:
apply tensorHom_comp_tensorHom

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
M₁ M₂ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
h : ∀ (X : Cᵒᵖ), Hom.app (M₁ ◁ 𝟙 M₂) X = Hom.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) M₁ M₂)) X
⊢ M₁ ◁ 𝟙 M₂ = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) M₁ M₂)

Tactic:
ext1 X
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
M₁ M₂ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
X : Cᵒᵖ
⊢ Hom.app (M₁ ◁ 𝟙 M₂) X = Hom.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) M₁ M₂)) X

Tactic:
apply MonoidalCategory.whiskerLeft_id (C := ModuleCat (R.obj X))

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_id
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
x x_1 :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
h : ∀ (X : Cᵒᵖ), Hom.app (𝟙 x ▷ x_1) X = Hom.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)) X
⊢ 𝟙 x ▷ x_1 = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)

Tactic:
ext1 X
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
x x_1 :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
X : Cᵒᵖ
⊢ Hom.app (𝟙 x ▷ x_1) X = Hom.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)) X

Tactic:
apply MonoidalCategory.id_whiskerRight (C := ModuleCat (R.obj X))

Premises used: CategoryTheory.MonoidalCategory.id_whiskerRight
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X₁ X₂ X₃ Y₁ Y₂ Y₃ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
x_2 : X₃ ⟶ Y₃
h :
  ∀ (X : Cᵒᵖ),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂)
              X₃).obj
          X ⟶
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₁
              (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₂ Y₃)).obj
          X)
      (Hom.app (((x ⊗ₘ x_1) ⊗ₘ x_2) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)) X) (Hom.app (Iso.hom (α_ X₁ X₂ X₃) ≫ (x ⊗ₘ x_1 ⊗ₘ x_2)) X)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂)
        X₃ ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₁
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₂ Y₃))
    (((x ⊗ₘ x_1) ⊗ₘ x_2) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)) (Iso.hom (α_ X₁ X₂ X₃) ≫ (x ⊗ₘ x_1 ⊗ₘ x_2))

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X₁ X₂ X₃ Y₁ Y₂ Y₃ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
x_2 : X₃ ⟶ Y₃
X : Cᵒᵖ
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X₁ X₂)
            X₃).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₁
            (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y₂ Y₃)).obj
        X)
    (Hom.app (((x ⊗ₘ x_1) ⊗ₘ x_2) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)) X) (Hom.app (Iso.hom (α_ X₁ X₂ X₃) ≫ (x ⊗ₘ x_1 ⊗ₘ x_2)) X)

Tactic:
apply associator_naturality

Premises used: CategoryTheory.MonoidalCategory.associator_naturality
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X Y :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X ⟶ Y
h :
  ∀ (X_1 : Cᵒᵖ),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
              ((𝟙_
                  (PresheafOfModules
                    (R ⋙
                      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                        (CD := RingCat.carrier))))
                (𝒞 := instCategory))
              X).obj
          X_1 ⟶
        Y.obj X_1)
      (Hom.app
        ((𝟙_
                (PresheafOfModules
                  (R ⋙
                    forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                      (CD := RingCat.carrier))))
              (𝒞 := instCategory) ◁
            x ≫
          Iso.hom (λ_ Y))
        X_1)
      (Hom.app (Iso.hom (λ_ X) ≫ x) X_1)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
        ((𝟙_
            (PresheafOfModules
              (R ⋙
                forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                  RingCat.carrier))))
          (𝒞 := instCategory))
        X ⟶
      Y)
    ((𝟙_
            (PresheafOfModules
              (R ⋙
                forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                  RingCat.carrier))))
          (𝒞 := instCategory) ◁
        x ≫
      Iso.hom (λ_ Y))
    (Iso.hom (λ_ X) ≫ x)

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X Y :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X ⟶ Y
X_1 : Cᵒᵖ
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
            ((𝟙_
                (PresheafOfModules
                  (R ⋙
                    forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                      (CD := RingCat.carrier))))
              (𝒞 := instCategory))
            X).obj
        X_1 ⟶
      Y.obj X_1)
    (Hom.app
      ((𝟙_
              (PresheafOfModules
                (R ⋙
                  forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                    (CD := RingCat.carrier))))
            (𝒞 := instCategory) ◁
          x ≫
        Iso.hom (λ_ Y))
      X_1)
    (Hom.app (Iso.hom (λ_ X) ≫ x) X_1)

Tactic:
apply leftUnitor_naturality

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_naturality
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X Y :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X ⟶ Y
h :
  ∀ (X_1 : Cᵒᵖ),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X
              ((𝟙_
                  (PresheafOfModules
                    (R ⋙
                      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                        (CD := RingCat.carrier))))
                (𝒞 := instCategory))).obj
          X_1 ⟶
        Y.obj X_1)
      (Hom.app
        (x ▷
            (𝟙_
                (PresheafOfModules
                  (R ⋙
                    forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                      (CD := RingCat.carrier))))
              (𝒞 := instCategory) ≫
          Iso.hom (ρ_ Y))
        X_1)
      (Hom.app (Iso.hom (ρ_ X) ≫ x) X_1)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X
        ((𝟙_
            (PresheafOfModules
              (R ⋙
                forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                  RingCat.carrier))))
          (𝒞 := instCategory)) ⟶
      Y)
    (x ▷
        (𝟙_
            (PresheafOfModules
              (R ⋙
                forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                  RingCat.carrier))))
          (𝒞 := instCategory) ≫
      Iso.hom (ρ_ Y))
    (Iso.hom (ρ_ X) ≫ x)

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
X Y :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : X ⟶ Y
X_1 : Cᵒᵖ
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X
            ((𝟙_
                (PresheafOfModules
                  (R ⋙
                    forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                      (CD := RingCat.carrier))))
              (𝒞 := instCategory))).obj
        X_1 ⟶
      Y.obj X_1)
    (Hom.app
      (x ▷
          (𝟙_
              (PresheafOfModules
                (R ⋙
                  forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                    (CD := RingCat.carrier))))
            (𝒞 := instCategory) ≫
        Iso.hom (ρ_ Y))
      X_1)
    (Hom.app (Iso.hom (ρ_ X) ≫ x) X_1)

Tactic:
apply rightUnitor_naturality

Premises used: CategoryTheory.MonoidalCategory.rightUnitor_naturality
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
x x_1 x_2 x_3 :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
h :
  ∀ (X : Cᵒᵖ),
    Hom.app
        (Iso.hom (α_ x x_1 x_2) ▷ x_3 ≫
          Iso.hom (α_ x (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2) x_3) ≫
            x ◁ Iso.hom (α_ x_1 x_2 x_3))
        X =
      (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1) x_2 x_3) ≫
            Iso.hom (α_ x x_1 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x_3))).app
        X
⊢ Iso.hom (α_ x x_1 x_2) ▷ x_3 ≫
      Iso.hom (α_ x (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2) x_3) ≫ x ◁ Iso.hom (α_ x_1 x_2 x_3) =
    Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1) x_2 x_3) ≫
      Iso.hom (α_ x x_1 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x_3))

Tactic:
ext1