awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X)
j j' : Under.{v₁, u₁} (op X)
φ : j ⟶ j'
dsimp :
  Eq (α := M ⟶ @EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j'.right))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j.right))
        (curry (g.app (op (Over.mk j.hom.unop))) : M ⟶ F.obj j.right ⟹ G.obj j.right)
        (eHomWhiskerLeft A (F.obj j.right) (G.map (Under.Hom.right φ)) :
          Quiver.Hom (V := A) (@EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j.right))
            (@EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j'.right))) :
      M ⟶ @EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j'.right))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j'.right) (G.obj j'.right))
        (curry (g.app (op (Over.mk j'.hom.unop))) : M ⟶ F.obj j'.right ⟹ G.obj j'.right)
        (eHomWhiskerRight A (F.map (Under.Hom.right φ)) (G.obj j'.right) :
          Quiver.Hom (V := A) (@EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j'.right) (G.obj j'.right))
            (@EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j'.right))) :
      M ⟶ @EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j'.right))
⊢ Eq (α :=
    unop (op M) ⟶ Functor.obj (Functor.obj (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) (op j)) j')
    ((fun (j : Under.{v₁, u₁} (op X)) ↦
          (curry (g.app (op (Over.mk j.hom.unop))) :
            unop (op M) ⟶ unop ((Under.forget (op X) ⋙ F).op.obj (op j)) ⟹ (Under.forget (op X) ⋙ G).obj j))
        j ≫
      Functor.map (Functor.obj (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) (op j)) φ)
    ((fun (j : Under.{v₁, u₁} (op X)) ↦
          (curry (g.app (op (Over.mk j.hom.unop))) :
            unop (op M) ⟶ unop ((Under.forget (op X) ⋙ F).op.obj (op j)) ⟹ (Under.forget (op X) ⋙ G).obj j))
        j' ≫
      NatTrans.app (Functor.map (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) φ.op) j')

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X)
j j' : Under.{v₁, u₁} (op X)
φ : j ⟶ j'
rw :
  Eq (α := M ⟶ @EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j'.right))
    (curry (g.app (op (Over.mk j.hom.unop)) ≫ G.map (Under.Hom.right φ)) : M ⟶ F.obj j.right ⟹ G.obj j'.right)
    (curry (F.map (Under.Hom.right φ) ▷ M ≫ g.app (op (Over.mk j'.hom.unop))) : M ⟶ F.obj j.right ⟹ G.obj j'.right)
⊢ Eq (α := M ⟶ @EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j'.right))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j.right))
        (curry (g.app (op (Over.mk j.hom.unop))) : M ⟶ F.obj j.right ⟹ G.obj j.right)
        (eHomWhiskerLeft A (F.obj j.right) (G.map (Under.Hom.right φ)) :
          Quiver.Hom (V := A) (@EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j.right))
            (@EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j'.right))) :
      M ⟶ @EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j'.right))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j'.right) (G.obj j'.right))
        (curry (g.app (op (Over.mk j'.hom.unop))) : M ⟶ F.obj j'.right ⟹ G.obj j'.right)
        (eHomWhiskerRight A (F.map (Under.Hom.right φ)) (G.obj j'.right) :
          Quiver.Hom (V := A) (@EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j'.right) (G.obj j'.right))
            (@EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j'.right))) :
      M ⟶ @EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j'.right))

Tactic:
rw [enrichedOrdinaryCategorySelf_eHomWhiskerRight,
        enrichedOrdinaryCategorySelf_eHomWhiskerLeft,
        curry_pre_app, ← curry_natural_right]

Premises used: CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerRight, CategoryTheory.MonoidalClosed.curry_pre_app, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerLeft, CategoryTheory.MonoidalClosed.curry_natural_right
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X)
j j' : Under.{v₁, u₁} (op X)
φ : j ⟶ j'
e_a :
  Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj j.right) M ⟶ G.obj j'.right)
    (g.app (op (Over.mk j.hom.unop)) ≫ G.map (Under.Hom.right φ) :
      tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj j.right) M ⟶ G.obj j'.right)
    (F.map (Under.Hom.right φ) ▷ M ≫ g.app (op (Over.mk j'.hom.unop)) :
      tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj j.right) M ⟶ G.obj j'.right)
⊢ Eq (α := M ⟶ @EnrichedCategory.Hom.{v₃, u₃, u₃} _ inst_1 inst_2 _ _ (F.obj j.right) (G.obj j'.right))
    (curry (g.app (op (Over.mk j.hom.unop)) ≫ G.map (Under.Hom.right φ)) : M ⟶ F.obj j.right ⟹ G.obj j'.right)
    (curry (F.map (Under.Hom.right φ) ▷ M ≫ g.app (op (Over.mk j'.hom.unop))) : M ⟶ F.obj j.right ⟹ G.obj j'.right)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X)
j j' : Under.{v₁, u₁} (op X)
φ : j ⟶ j'
⊢ ((Under.Hom.right φ).unop ≫ (Over.mk j.hom.unop).hom).op = (Over.mk j'.hom.unop).hom.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X)
j j' : Under.{v₁, u₁} (op X)
φ : j ⟶ j'
α : Over.mk j'.hom.unop ⟶ Over.mk j.hom.unop := Over.homMk (Under.Hom.right φ).unop ⋯
⊢ Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj j.right) M ⟶ G.obj j'.right)
    (g.app (op (Over.mk j.hom.unop)) ≫ G.map (Under.Hom.right φ) :
      tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj j.right) M ⟶ G.obj j'.right)
    (F.map (Under.Hom.right φ) ▷ M ≫ g.app (op (Over.mk j'.hom.unop)) :
      tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj j.right) M ⟶ G.obj j'.right)

Tactic:
simpa using (g.naturality α.op).symm

Premises used: Quiver.Hom.op, CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M)).obj (op X)
dsimp :
  end_.lift
      (fun (j : Under.{v₁, u₁} (op X)) ↦
        curry (uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk j.hom))))
      ⋯ =
    f
⊢ (fun (g : (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X)) ↦
        (end_.lift (fun (j : Under.{v₁, u₁} (op X)) ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯ :
          unop (op M) ⟶ end_ (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G))))
      ((fun (f : (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M)).obj (op X)) ↦
          ({
              app := fun (j : (Over.{v₁, u₁} (unop (op X)))ᵒᵖ) ↦
                uncurry
                  (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)),
              naturality := ⋯ } :
            NatTrans
              (Functor.op (Over.forget (unop (op X))) ⋙
                tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M))
              (Functor.op (Over.forget (unop (op X))) ⋙ G)))
        f) =
    f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M)).obj (op X)
h :
  ∀ (j : Under.{v₁, u₁} (op X)),
    CategoryStruct.comp (Y := end_ (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)))
        (end_.lift
          (fun (j : Under.{v₁, u₁} (op X)) ↦
            curry (uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk j.hom))))
          ⋯)
        (end_.π (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) j) =
      f ≫ end_.π (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) j
⊢ end_.lift
      (fun (j : Under.{v₁, u₁} (op X)) ↦
        curry (uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk j.hom))))
      ⋯ =
    f

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M)).obj (op X)
j : Under.{v₁, u₁} (op X)
h :
  CategoryStruct.comp (Y := end_ (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)))
      (end_.lift
        (fun (j : Under.{v₁, u₁} (op X)) ↦
          curry (uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk j.hom))))
        ⋯)
      (end_.π (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) j) =
    f ≫ end_.π (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) j
⊢ CategoryStruct.comp (Y := end_ (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)))
      (end_.lift
        (fun (j : Under.{v₁, u₁} (op X)) ↦
          curry (uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk j.hom))))
        ⋯)
      (end_.π (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) j) =
    f ≫ end_.π (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M)).obj (op X)
j : Under.{v₁, u₁} (op X)
h :
  f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk j.hom) =
    f ≫ end_.π (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) j
⊢ CategoryStruct.comp (Y := end_ (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)))
      (end_.lift
        (fun (j : Under.{v₁, u₁} (op X)) ↦
          curry (uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk j.hom))))
        ⋯)
      (end_.π (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) j) =
    f ≫ end_.π (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) j

Tactic:
simp only [curry_uncurry, end_.lift_π]

Premises used: CategoryTheory.Limits.end_.lift_π, CategoryTheory.MonoidalClosed.curry_uncurry
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M)).obj (op X)
j : Under.{v₁, u₁} (op X)
⊢ f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk j.hom) =
    f ≫ end_.π (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) j

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X)
dsimp :
  {
      app := fun (j : (Over.{v₁, u₁} X)ᵒᵖ) ↦
        uncurry
          (CategoryStruct.comp (Y := enrichedHom A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G))
            (end_.lift (fun (j : Under.{v₁, u₁} (op X)) ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯)
            (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op))),
      naturality := ⋯ } =
    g
⊢ (fun (f : (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M)).obj (op X)) ↦
        ({
            app := fun (j : (Over.{v₁, u₁} (unop (op X)))ᵒᵖ) ↦
              uncurry
                (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)),
            naturality := ⋯ } :
          NatTrans
            (Functor.op (Over.forget (unop (op X))) ⋙
              tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M))
            (Functor.op (Over.forget (unop (op X))) ⋙ G)))
      ((fun (g : (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X)) ↦
          (end_.lift (fun (j : Under.{v₁, u₁} (op X)) ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯ :
            unop (op M) ⟶ end_ (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G))))
        g) =
    g

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X)
w :
  ∀ (j : (Over.{v₁, u₁} X)ᵒᵖ),
    NatTrans.app
        {
          app := fun (j : (Over.{v₁, u₁} X)ᵒᵖ) ↦
            uncurry
              (CategoryStruct.comp (Y := enrichedHom A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G))
                (end_.lift (fun (j : Under.{v₁, u₁} (op X)) ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯)
                (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op))),
          naturality := ⋯ }
        j =
      g.app j
⊢ {
      app := fun (j : (Over.{v₁, u₁} X)ᵒᵖ) ↦
        uncurry
          (CategoryStruct.comp (Y := enrichedHom A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G))
            (end_.lift (fun (j : Under.{v₁, u₁} (op X)) ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯)
            (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op))),
      naturality := ⋯ } =
    g

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X)
j : (Over.{v₁, u₁} X)ᵒᵖ
w :
  uncurry
      (CategoryStruct.comp (Y := enrichedHom A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G))
        (end_.lift (fun (j : Under.{v₁, u₁} (op X)) ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯)
        (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op))) =
    g.app j
⊢ NatTrans.app
      {
        app := fun (j : (Over.{v₁, u₁} X)ᵒᵖ) ↦
          uncurry
            (CategoryStruct.comp (Y := enrichedHom A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G))
              (end_.lift (fun (j : Under.{v₁, u₁} (op X)) ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯)
              (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op))),
        naturality := ⋯ }
      j =
    g.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X)
j : (Over.{v₁, u₁} X)ᵒᵖ
w :
  g.app
      (op
        (Over.mk (Y := unop (Under.right.{v₁, u₁} (X := op X) (Under.mk (unop j).hom.op)))
          (Quiver.Hom.unop (Under.hom (Under.mk (unop j).hom.op))))) =
    g.app j
⊢ uncurry
      (CategoryStruct.comp (Y := enrichedHom A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G))
        (end_.lift (fun (j : Under.{v₁, u₁} (op X)) ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯)
        (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op))) =
    g.app j

Tactic:
simp only [uncurry_curry, end_.lift_π]

Premises used: CategoryTheory.MonoidalClosed.uncurry_curry, CategoryTheory.Limits.end_.lift_π
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
inst_4 : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X)
j : (Over.{v₁, u₁} X)ᵒᵖ
⊢ g.app
      (op
        (Over.mk (Y := unop (Under.right.{v₁, u₁} (X := op X) (Under.mk (unop j).hom.op)))
          (Quiver.Hom.unop (Under.hom (Under.mk (unop j).hom.op))))) =
    g.app j

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
X Y : C
f : X ⟶ Y
inst_4 : HasFunctorEnrichedHom A F G
y : (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M)).obj (op Y)
j : Over.{v₁, u₁} X
w :
  Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op j.left)) M ⟶ G.obj (op j.left))
    (uncurry
        (y ≫
          enrichedHomπ A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G)
            (Functor.obj (C := Under.{v₁, u₁} (op X)) (Under.map f.op) (Under.mk j.hom.op))) :
      tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op j.left)) M ⟶ G.obj (op j.left))
    (uncurry
        (y ≫
          enrichedHomπ A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G)
            (Under.mk (Y := op j.left) (f.op ≫ j.hom.op))) :
      tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op j.left)) M ⟶ G.obj (op j.left))
⊢ Eq.{v₃ + 1} (α :=
    (Functor.op (Over.forget X) ⋙ tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)).obj (op j) ⟶
      (Functor.op (Over.forget X) ⋙ G).obj (op j))
    (NatTrans.app
      ((functorEnrichedHomCoyonedaObjEquiv M F G X :
          (a : M ⟶ enrichedHom A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) →
            (Over.forget X).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget X).op ⋙ G)
        (y ≫
          precompEnrichedHom' A (Under.map f.op) (Iso.refl (Under.map f.op ⋙ Under.forget (op Y) ⋙ F))
            (Iso.refl (Under.map f.op ⋙ Under.forget (op Y) ⋙ G))))
      (op j))
    (NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).map f.op) :
          (a : (Over.forget Y).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget Y).op ⋙ G) →
            (Over.forget X).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget X).op ⋙ G)
        ((functorEnrichedHomCoyonedaObjEquiv M F G Y :
            (a : M ⟶ enrichedHom A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G)) →
              (Over.forget Y).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget Y).op ⋙ G)
          y))
      (op j))

Tactic:
simp [functorEnrichedHomCoyonedaObjEquiv, presheafHom]

Premises used: CategoryTheory.presheafHom, CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
X Y : C
f : X ⟶ Y
inst_4 : HasFunctorEnrichedHom A F G
y : (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M)).obj (op Y)
j : Over.{v₁, u₁} X
⊢ Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op j.left)) M ⟶ G.obj (op j.left))
    (uncurry
        (y ≫
          enrichedHomπ A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G)
            (Functor.obj (C := Under.{v₁, u₁} (op X)) (Under.map f.op) (Under.mk j.hom.op))) :
      tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op j.left)) M ⟶ G.obj (op j.left))
    (uncurry
        (y ≫
          enrichedHomπ A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G)
            (Under.mk (Y := op j.left) (f.op ≫ j.hom.op))) :
      tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op j.left)) M ⟶ G.obj (op j.left))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
hG : IsSheaf J G
inst_4 : HasFunctorEnrichedHom A F G
M : A
rw : Presieve.IsSheaf J (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G)
⊢ Presieve.IsSheaf.{v₃, v₁, u₁} J (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M))

Tactic:
rw [Presieve.isSheaf_iff_of_nat_equiv
    (functorEnrichedHomCoyonedaObjEquiv M F G)
    (fun _ _ _ _ ↦ functorEnrichedHomCoyonedaObjEquiv_naturality _ _)]

Premises used: CategoryTheory.Presieve.isSheaf_iff_of_nat_equiv, CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturality, CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv