awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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

Tactic:
apply pentagon

Premises used: CategoryTheory.MonoidalCategory.pentagon
-- 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ᵒᵖ),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
              (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)))
              x_1).obj
          X ⟶
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1).obj X)
      (Hom.app
        (Iso.hom
            (α_ 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))
              x_1) ≫
          x ◁ Iso.hom (λ_ x_1))
        X)
      (Hom.app (Iso.hom (ρ_ x) ▷ x_1) X)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
        (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)))
        x_1 ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)
    (Iso.hom
        (α_ 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))
          x_1) ≫
      x ◁ Iso.hom (λ_ x_1))
    (Iso.hom (ρ_ 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ᵒᵖ
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
            (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)))
            x_1).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1).obj X)
    (Hom.app
      (Iso.hom
          (α_ 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))
            x_1) ≫
        x ◁ Iso.hom (λ_ x_1))
      X)
    (Hom.app (Iso.hom (ρ_ x) ▷ x_1) X)

Tactic:
apply triangle

Premises used: CategoryTheory.MonoidalCategory.triangle
-- 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 :
  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_3 : x_1 ⟶ x_2
h :
  ∀ (X : Cᵒᵖ),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1).obj X ⟶
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x).obj X)
      (Hom.app (x ◁ x_3 ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) ⋯)) X)
      (Hom.app (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) ⋯) ≫ x_3 ▷ x) X)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1 ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x)
    (x ◁ x_3 ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) ⋯))
    (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) ⋯) ≫ x_3 ▷ x)

Tactic:
ext : 1
-- 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 :
  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_3 : x_1 ⟶ x_2
X : Cᵒᵖ
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1).obj X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x).obj X)
    (Hom.app (x ◁ x_3 ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) ⋯)) X)
    (Hom.app (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) ⋯) ≫ x_3 ▷ x) X)

Tactic:
ModuleCat.MonoidalCategory.tensor_ext (fun _ _ ↦ rfl)

Premises used: ModuleCat.MonoidalCategory.tensor_ext, 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 x_1 x_2 :
  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_3 : x_1 ⟶ x_2
X : Cᵒᵖ
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1).obj X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x).obj X)
    (Hom.app (x ◁ x_3 ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) ⋯)) X)
    (Hom.app (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) ⋯) ≫ x_3 ▷ x) X)

Tactic:
exact ModuleCat.MonoidalCategory.tensor_ext (fun _ _ ↦ rfl)

Premises used: ModuleCat.MonoidalCategory.tensor_ext, 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 :
  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 :
  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_1 : Cᵒᵖ),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X x_1).obj X_1 ⟶
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 Y).obj X_1)
      (Hom.app (x ▷ x_1 ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (Y.obj X) (x_1.obj X)) ⋯)) X_1)
      (Hom.app (Iso.hom (isoMk (fun (X_2 : Cᵒᵖ) ↦ β_ (X.obj X_2) (x_1.obj X_2)) ⋯) ≫ x_1 ◁ x) X_1)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X x_1 ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 Y)
    (x ▷ x_1 ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (Y.obj X) (x_1.obj X)) ⋯))
    (Iso.hom (isoMk (fun (X_1 : Cᵒᵖ) ↦ β_ (X.obj X_1) (x_1.obj X_1)) ⋯) ≫ x_1 ◁ x)

Tactic:
ext : 1
-- 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 :
  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_1 : Cᵒᵖ
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X x_1).obj X_1 ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 Y).obj X_1)
    (Hom.app (x ▷ x_1 ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (Y.obj X) (x_1.obj X)) ⋯)) X_1)
    (Hom.app (Iso.hom (isoMk (fun (X_2 : Cᵒᵖ) ↦ β_ (X.obj X_2) (x_1.obj X_2)) ⋯) ≫ x_1 ◁ x) X_1)

Tactic:
ModuleCat.MonoidalCategory.tensor_ext (fun _ _ ↦ rfl)

Premises used: ModuleCat.MonoidalCategory.tensor_ext, 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 :
  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 :
  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_1 : Cᵒᵖ
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X x_1).obj X_1 ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 Y).obj X_1)
    (Hom.app (x ▷ x_1 ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (Y.obj X) (x_1.obj X)) ⋯)) X_1)
    (Hom.app (Iso.hom (isoMk (fun (X_2 : Cᵒᵖ) ↦ β_ (X.obj X_2) (x_1.obj X_2)) ⋯) ≫ x_1 ◁ x) X_1)

Tactic:
exact ModuleCat.MonoidalCategory.tensor_ext (fun _ _ ↦ rfl)

Premises used: ModuleCat.MonoidalCategory.tensor_ext, 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 x_1 x_2 :
  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ᵒᵖ),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)
              x_2).obj
          X ⟶
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1
              (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x)).obj
          X)
      (Hom.app
        (Iso.hom (α_ x x_1 x_2) ≫
          Iso.hom
              (isoMk
                (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2).obj X))
                ⋯) ≫
            Iso.hom (α_ x_1 x_2 x))
        X)
      (Hom.app
        (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) ⋯) ▷ x_2 ≫
          Iso.hom (α_ x_1 x x_2) ≫ x_1 ◁ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) ⋯))
        X)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)
        x_2 ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x))
    (Iso.hom (α_ x x_1 x_2) ≫
      Iso.hom
          (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2).obj X))
            ⋯) ≫
        Iso.hom (α_ x_1 x_2 x))
    (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) ⋯) ▷ x_2 ≫
      Iso.hom (α_ x_1 x x_2) ≫ x_1 ◁ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) ⋯))

Tactic:
ext : 1
-- 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 :
  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ᵒᵖ
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)
            x_2).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1
            (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x)).obj
        X)
    (Hom.app
      (Iso.hom (α_ x x_1 x_2) ≫
        Iso.hom
            (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2).obj X))
              ⋯) ≫
          Iso.hom (α_ x_1 x_2 x))
      X)
    (Hom.app
      (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) ⋯) ▷ x_2 ≫
        Iso.hom (α_ x_1 x x_2) ≫ x_1 ◁ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) ⋯))
      X)

Tactic:
apply hexagon_forward (C := ModuleCat (R.obj _))

Premises used: CategoryTheory.BraidedCategory.hexagon_forward
-- 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 :
  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ᵒᵖ),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x
              (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2)).obj
          X ⟶
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory)
              (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x) x_1).obj
          X)
      (Hom.app
        (Iso.inv (α_ x x_1 x_2) ≫
          Iso.hom
              (isoMk
                (fun (X : Cᵒᵖ) ↦ β_ ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1).obj X) (x_2.obj X))
                ⋯) ≫
            Iso.inv (α_ x_2 x x_1))
        X)
      (Hom.app
        (x ◁ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x_1.obj X) (x_2.obj X)) ⋯) ≫
          Iso.inv (α_ x x_2 x_1) ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) ⋯) ▷ x_1)
        X)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2) ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x)
        x_1)
    (Iso.inv (α_ x x_1 x_2) ≫
      Iso.hom
          (isoMk (fun (X : Cᵒᵖ) ↦ β_ ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1).obj X) (x_2.obj X))
            ⋯) ≫
        Iso.inv (α_ x_2 x x_1))
    (x ◁ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x_1.obj X) (x_2.obj X)) ⋯) ≫
      Iso.inv (α_ x x_2 x_1) ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) ⋯) ▷ x_1)

Tactic:
ext : 1
-- 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 :
  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ᵒᵖ
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x
            (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x_2)).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_2 x)
            x_1).obj
        X)
    (Hom.app
      (Iso.inv (α_ x x_1 x_2) ≫
        Iso.hom
            (isoMk (fun (X : Cᵒᵖ) ↦ β_ ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1).obj X) (x_2.obj X))
              ⋯) ≫
          Iso.inv (α_ x_2 x x_1))
      X)
    (Hom.app
      (x ◁ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x_1.obj X) (x_2.obj X)) ⋯) ≫
        Iso.inv (α_ x x_2 x_1) ≫ Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_2.obj X)) ⋯) ▷ x_1)
      X)

Tactic:
apply hexagon_reverse (C := ModuleCat (R.obj _))

Premises used: CategoryTheory.BraidedCategory.hexagon_reverse
-- 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
        (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x)
          (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) ⋯))
          (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x_1.obj X) (x.obj X)) ⋯)))
        X =
      Hom.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)) X
⊢ CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x)
      (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) ⋯))
      (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x_1.obj X) (x.obj X)) ⋯)) =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)

Tactic:
ext : 1
-- 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
      (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x_1 x)
        (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x.obj X) (x_1.obj X)) ⋯))
        (Iso.hom (isoMk (fun (X : Cᵒᵖ) ↦ β_ (x_1.obj X) (x.obj X)) ⋯)))
      X =
    Hom.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) x x_1)) X

Tactic:
apply SymmetricCategory.symmetry (C := ModuleCat (R.obj _))

Premises used: CategoryTheory.SymmetricCategory.symmetry
-- 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ᵒᵖ
⊢ (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) M₁ M₂).obj X =
    MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj X) : Type u)) (M₁.obj X) (M₂.obj X)

Tactic:
rfl

Premises used: 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
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))
f : M₂ ⟶ M₃
X : Cᵒᵖ
⊢ Hom.app (M₁ ◁ f) X = M₁.obj X ◁ f.app X

Tactic:
rfl

Premises used: LinearMap.lTensor, 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
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))
f : 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ᵒᵖ
⊢ Hom.app (f ▷ M₃) X = f.app X ▷ M₃.obj X

Tactic:
rfl

Premises used: rfl, LinearMap.rTensor
-- 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))
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X : Cᵒᵖ
⊢ Hom.app (f ⊗ₘ g) X = f.app X ⊗ₘ g.app X

Tactic:
rfl

Premises used: 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
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 (Iso.hom (λ_ M₁)) X = Iso.hom (λ_ (M₁.obj X))

Tactic:
rfl

Premises used: rfl