awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Functor.{v, v', u, v' + 1} Cᵒᵖ (Type v')
this : IsLimit (S.op.map P).pullbackCone ≃ Function.Bijective (S.op.map P).pullbackCone.toPullbackObj
⊢ S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P)

Tactic:
⟨fun h ↦ this h.isLimit, fun h ↦ Square.IsPullback.mk _ (this.symm h)⟩

Premises used: CategoryTheory.Square.IsPullback.mk, CategoryTheory.Square.IsPullback.isLimit, CategoryTheory.Square.op, CategoryTheory.Square.map, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare, Iff.intro, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Functor.{v, v', u, v' + 1} Cᵒᵖ (Type v')
this : IsLimit (S.op.map P).pullbackCone ≃ Function.Bijective (S.op.map P).pullbackCone.toPullbackObj
⊢ S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P)

Tactic:
exact ⟨fun h ↦ this h.isLimit, fun h ↦ Square.IsPullback.mk _ (this.symm h)⟩
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Functor.{v, v', u, v' + 1} Cᵒᵖ (Type v')
h rwa rwa₁ rwa₂ rwa₃ : S.SheafCondition P
⊢ Function.Bijective (S.toPullbackObj P)

Tactic:
rwa [← sheafCondition_iff_bijective_toPullbackObj]

Premises used: CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_bijective_toPullbackObj
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Functor.{v, v', u, v' + 1} Cᵒᵖ (Type v')
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ :
  Eq (α := (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₂₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
        x :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₂₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
        y :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
h₂ :
  Eq (α := (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₃₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
        x :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₃₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
        y :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
a :
  (↑(S.toPullbackObj P x) : P.obj (op S.X₂) × P.obj (op S.X₃)).1 =
    (↑(S.toPullbackObj P y) : P.obj (op S.X₂) × P.obj (op S.X₃)).1
a₁ :
  (↑(S.toPullbackObj P x) : P.obj (op S.X₂) × P.obj (op S.X₃)).2 =
    (↑(S.toPullbackObj P y) : P.obj (op S.X₂) × P.obj (op S.X₃)).2
⊢ S.toPullbackObj P x = S.toPullbackObj P y

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Functor.{v, v', u, v' + 1} Cᵒᵖ (Type v')
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ :
  Eq (α := (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₂₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
        x :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₂₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
        y :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
h₂ :
  Eq (α := (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₃₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
        x :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₃₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
        y :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
⊢ (↑(S.toPullbackObj P x) : P.obj (op S.X₂) × P.obj (op S.X₃)).1 =
    (↑(S.toPullbackObj P y) : P.obj (op S.X₂) × P.obj (op S.X₃)).1

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Functor.{v, v', u, v' + 1} Cᵒᵖ (Type v')
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ :
  Eq (α := (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₂₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
        x :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₂₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
        y :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
h₂ :
  Eq (α := (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₃₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
        x :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₃₄.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
        y :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
⊢ (↑(S.toPullbackObj P x) : P.obj (op S.X₂) × P.obj (op S.X₃)).2 =
    (↑(S.toPullbackObj P y) : P.obj (op S.X₂) × P.obj (op S.X₃)).2

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Functor.{v, v', u, v' + 1} Cᵒᵖ (Type v')
h : S.SheafCondition P
u : P.obj (op S.X₂)
v : P.obj (op S.X₃)
huv :
  Eq (α := (fun (X : Type v') ↦ X) (P.obj (op S.X₁)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₁₂.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₂))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₁)))
        u :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₁)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₁₃.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₃))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₁)))
        v :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₁)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₂₄.op) :
        (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₂)))
      (h.glue u v huv) =
    u

Tactic:
PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst h.isLimit _

Premises used: CategoryTheory.Square.IsPullback.isLimit, Quiver.Hom.op, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.glue
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Functor.{v, v', u, v' + 1} Cᵒᵖ (Type v')
h : S.SheafCondition P
u : P.obj (op S.X₂)
v : P.obj (op S.X₃)
huv :
  Eq (α := (fun (X : Type v') ↦ X) (P.obj (op S.X₁)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₁₂.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₂))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₁)))
        u :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₁)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₁₃.op) :
          (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₃))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₁)))
        v :
      (fun (X : Type v') ↦ X) (P.obj (op S.X₁)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map S.f₃₄.op) :
        (a : (fun (X : Type v') ↦ X) (P.obj (op S.X₄))) → (fun (X : Type v') ↦ X) (P.obj (op S.X₃)))
      (h.glue u v huv) =
    v

Tactic:
PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd h.isLimit _

Premises used: CategoryTheory.Square.IsPullback.isLimit, Quiver.Hom.op, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.glue, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
A : Type u'
inst_2 : Category.{v, u'} A
F : Sheaf J A
rw : ∀ (X : Aᵒᵖ), S.SheafCondition (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda X)
⊢ S.SheafCondition (F.obj (P := Presheaf.IsSheaf J))

Tactic:
rw [sheafCondition_iff_comp_coyoneda]

Premises used: CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_comp_coyoneda
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
A : Type u'
inst_2 : Category.{v, u'} A
F : Sheaf J A
X : Aᵒᵖ
⊢ S.SheafCondition (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda X)

Tactic:
(Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff _ S.toSquare).1
    (S.isPushout.op.map
      (yoneda.obj ⟨_, (isSheaf_iff_isSheaf_of_type _ _).2 (F.property X.unop)⟩))

Premises used: Iff.mpr, CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition, CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushout, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, CategoryTheory.yoneda, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare, CategoryTheory.isSheaf_iff_isSheaf_of_type, CategoryTheory.Square.IsPullback.map, Iff.mp, CategoryTheory.Square.IsPushout.op, Opposite.unop, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
A : Type u'
inst_2 : Category.{v, u'} A
F : Sheaf J A
X : Aᵒᵖ
⊢ S.SheafCondition (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda X)

Tactic:
exact (Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff _ S.toSquare).1
    (S.isPushout.op.map
      (yoneda.obj ⟨_, (isSheaf_iff_isSheaf_of_type _ _).2 (F.property X.unop)⟩))

Premises used: Iff.mpr, CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushout, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.yoneda, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare, CategoryTheory.isSheaf_iff_isSheaf_of_type, CategoryTheory.Square.IsPullback.map, Iff.mp, CategoryTheory.Square.IsPushout.op, Opposite.unop, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
S : J.MayerVietorisSquare
simp :
  Mono (X := Functor.obj (presheafToSheaf J AddCommGrpCat) (Functor.obj yoneda S.X₁ ⋙ AddCommGrpCat.free))
    (-Functor.map (presheafToSheaf J AddCommGrpCat)
        (Functor.whiskerRight (Functor.map yoneda S.f₁₃) AddCommGrpCat.free))
⊢ Mono (X := Functor.obj (presheafToSheaf J AddCommGrpCat) (Functor.obj yoneda S.X₁ ⋙ AddCommGrpCat.free))
    (CategoryStruct.comp (Y :=
      Functor.obj (presheafToSheaf J AddCommGrpCat) (Functor.obj yoneda S.X₂ ⋙ AddCommGrpCat.free) ⊞
        Functor.obj (presheafToSheaf J AddCommGrpCat) (Functor.obj yoneda S.X₃ ⋙ AddCommGrpCat.free))
      (biprod.lift
        (Functor.map (presheafToSheaf J AddCommGrpCat)
          (Functor.whiskerRight (Functor.map yoneda S.f₁₂) AddCommGrpCat.free))
        (-Functor.map (presheafToSheaf J AddCommGrpCat)
            (Functor.whiskerRight (Functor.map yoneda S.f₁₃) AddCommGrpCat.free)))
      biprod.snd)

Tactic:
simp only [biprod.lift_snd]

Premises used: CategoryTheory.Limits.biprod.lift_snd
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
S : J.MayerVietorisSquare
⊢ Mono (X := Functor.obj (presheafToSheaf J AddCommGrpCat) (Functor.obj yoneda S.X₁ ⋙ AddCommGrpCat.free))
    (-Functor.map (presheafToSheaf J AddCommGrpCat)
        (Functor.whiskerRight (Functor.map yoneda S.f₁₃) AddCommGrpCat.free))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
S : J.MayerVietorisSquare
⊢ Mono (S.shortComplex.f ≫ biprod.snd)

Tactic:
have : Mono (S.shortComplex.f ≫ biprod.snd) := by
    dsimp
    simp only [biprod.lift_snd]
    infer_instance
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
S : J.MayerVietorisSquare
this : Mono (S.shortComplex.f ≫ biprod.snd)
⊢ Mono S.shortComplex.f

Tactic:
mono_of_mono _ biprod.snd

Premises used: CategoryTheory.Limits.biprod.snd, CategoryTheory.mono_of_mono
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
S : J.MayerVietorisSquare
this : Mono (S.shortComplex.f ≫ biprod.snd)
⊢ Mono S.shortComplex.f

Tactic:
exact mono_of_mono _ biprod.snd

Premises used: CategoryTheory.Limits.biprod.snd, CategoryTheory.mono_of_mono
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
S : J.MayerVietorisSquare
⊢ Epi S.shortComplex.g

Tactic:
(S.shortComplex.exact_and_epi_g_iff_g_is_cokernel.2
    ⟨S.isPushoutAddCommGrpFreeSheaf.isColimitCokernelCofork⟩).2

Premises used: Iff.mpr, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex, CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_cokernel, Nonempty.intro, And.right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf, CategoryTheory.Square.IsPushout.isColimitCokernelCofork
-- Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
S : J.MayerVietorisSquare
⊢ S.shortComplex.Exact

Tactic:
ShortComplex.exact_of_g_is_cokernel _
    S.isPushoutAddCommGrpFreeSheaf.isColimitCokernelCofork

Premises used: CategoryTheory.ShortComplex.exact_of_g_is_cokernel, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf, CategoryTheory.Square.IsPushout.isColimitCokernelCofork
-- 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 j' : (Over.{v₁, u₁} (unop (op X)))ᵒᵖ
φ : j ⟶ j'
dsimp :
  Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op (unop j).left)) M ⟶ G.obj (op (unop j').left))
    ((F.map (Over.Hom.left φ.unop).op ⊗ₘ 𝟙 M) ≫
      uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op)))
    (uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)) ≫
      G.map (Over.Hom.left φ.unop).op)
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙
            tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)).obj
        j ⟶
      (Functor.op (Over.forget (unop (op X))) ⋙ G).obj j')
    ((Functor.op (Over.forget (unop (op X))) ⋙
            tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)).map
        φ ≫
      uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op)))
    (uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)) ≫
      (Functor.op (Over.forget (unop (op X))) ⋙ G).map φ)

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 j' : (Over.{v₁, u₁} (unop (op X)))ᵒᵖ
φ : j ⟶ j'
rw :
  Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op (unop j).left)) M ⟶ G.obj (op (unop j').left))
    (uncurry
      (f ≫
        CategoryStruct.comp (Y := F.obj (op (unop j').left) ⟹ G.obj (op (unop j').left))
          (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op))
          (eHomWhiskerRight A (F.map (Over.Hom.left φ.unop).op) (G.obj (op (unop j').left)))))
    (uncurry
      (f ≫
        CategoryStruct.comp (Y := F.obj (op (unop j).left) ⟹ G.obj (op (unop j).left))
          (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op))
          (eHomWhiskerLeft A (F.obj (op (unop j).left)) (G.map (Over.Hom.left φ.unop).op))))
⊢ Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op (unop j).left)) M ⟶ G.obj (op (unop j').left))
    ((F.map (Over.Hom.left φ.unop).op ⊗ₘ 𝟙 M) ≫
      uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op)))
    (uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)) ≫
      G.map (Over.Hom.left φ.unop).op)

Tactic:
rw [tensorHom_id, ← uncurry_natural_right, ← uncurry_pre_app, Category.assoc,
          Category.assoc, ← enrichedOrdinaryCategorySelf_eHomWhiskerRight,
          ← enrichedOrdinaryCategorySelf_eHomWhiskerLeft]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalClosed.uncurry_natural_right, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerRight, CategoryTheory.MonoidalClosed.uncurry_pre_app, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerLeft, CategoryTheory.MonoidalCategory.tensorHom_id
-- 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 j' : (Over.{v₁, u₁} (unop (op X)))ᵒᵖ
φ : j ⟶ j'
e_a :
  Eq (α :=
    enrichedHom A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) ⟶
      F.obj (op (unop j).left) ⟹ G.obj (op (unop j').left))
    (CategoryStruct.comp (Y := F.obj (op (unop j').left) ⟹ G.obj (op (unop j').left))
      (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op))
      (eHomWhiskerRight A (F.map (Over.Hom.left φ.unop).op) (G.obj (op (unop j').left))))
    (CategoryStruct.comp (Y := F.obj (op (unop j).left) ⟹ G.obj (op (unop j).left))
      (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op))
      (eHomWhiskerLeft A (F.obj (op (unop j).left)) (G.map (Over.Hom.left φ.unop).op)))
⊢ Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op (unop j).left)) M ⟶ G.obj (op (unop j').left))
    (uncurry
      (f ≫
        CategoryStruct.comp (Y := F.obj (op (unop j').left) ⟹ G.obj (op (unop j').left))
          (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op))
          (eHomWhiskerRight A (F.map (Over.Hom.left φ.unop).op) (G.obj (op (unop j').left)))))
    (uncurry
      (f ≫
        CategoryStruct.comp (Y := F.obj (op (unop j).left) ⟹ G.obj (op (unop j).left))
          (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op))
          (eHomWhiskerLeft A (F.obj (op (unop j).left)) (G.map (Over.Hom.left φ.unop).op))))

Tactic:
congr 2
-- 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 j' : (Over.{v₁, u₁} (unop (op X)))ᵒᵖ
φ : j ⟶ j'
⊢ Eq.{v₁ + 1} (α := unop (Under.right.{v₁, u₁} (X := op X) (Under.mk (unop j').hom.op)) ⟶ unop (op X))
    (Quiver.Hom.unop (Under.hom (Under.mk (unop j).hom.op) ≫ (Over.Hom.left φ.unop).op))
    (Quiver.Hom.unop (Under.hom (Under.mk (unop j').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
f : (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M)).obj (op X)
j j' : (Over.{v₁, u₁} (unop (op X)))ᵒᵖ
φ : j ⟶ j'
⊢ Eq (α :=
    enrichedHom A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) ⟶
      F.obj (op (unop j).left) ⟹ G.obj (op (unop j').left))
    (CategoryStruct.comp (Y := F.obj (op (unop j').left) ⟹ G.obj (op (unop j').left))
      (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op))
      (eHomWhiskerRight A (F.map (Over.Hom.left φ.unop).op) (G.obj (op (unop j').left))))
    (CategoryStruct.comp (Y := F.obj (op (unop j).left) ⟹ G.obj (op (unop j).left))
      (enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op))
      (eHomWhiskerLeft A (F.obj (op (unop j).left)) (G.map (Over.Hom.left φ.unop).op)))

Tactic:
exact (enrichedHom_condition A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)
          (i := Under.mk j.unop.hom.op) (j := Under.mk j'.unop.hom.op)
            (Under.homMk φ.unop.left.op (Quiver.Hom.unop_inj (by simp)))).symm

Premises used: CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition, CategoryTheory.Under.homMk, Quiver.Hom.op, CategoryTheory.Over.Hom.left, CategoryTheory.Functor.comp, Quiver.Hom.unop, CategoryTheory.Under.forget, Quiver.Hom.unop_inj, Opposite.op, Eq.symm