awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : CartesianMonoidalCategory.{v_2, u_2} C
F₁ F₁' : Functor.{v_1, v_2, u_1, u_2} J C
f : F₁ ⟶ F₁'
F₂ : Functor.{v_1, v_2, u_1, u_2} J C
j : J
⊢ Eq (α := (tensorObj (𝒞 := category) F₁ F₂).obj j ⟶ F₂.obj j) (NatTrans.app (f ▷ F₂) j ≫ snd (F₁'.obj j) (F₂.obj j))
    (snd (F₁.obj j) (F₂.obj j))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : CartesianMonoidalCategory.{v_2, u_2} C
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} J C
j : J
⊢ Eq (α :=
    (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) F₁ F₂) F₃).obj j ⟶
      (tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j)
    (NatTrans.app (Iso.hom (α_ F₁ F₂ F₃)) j) (Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : CartesianMonoidalCategory.{v_2, u_2} C
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} J C
j : J
rw :
  Eq (α :=
    (tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₁.obj j) (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₂.obj j) (F₃.obj j)))
    (NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
    (Iso.inv (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))
rw₁ :
  NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j ≫ Iso.hom (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)) =
    𝟙 ((tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j)
rw₂ :
  NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j ≫ NatTrans.app (Iso.hom (α_ F₁ F₂ F₃)) j =
    𝟙 ((tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j)
rw₃ rw₄ :
  Eq.{v_2 + 1} (α :=
    (tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₁.obj j) (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₂.obj j) (F₃.obj j)))
    (𝟙 ((tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j))
    (𝟙 ((tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j))
⊢ Eq (α :=
    (tensorObj (𝒞 := category) F₁ (tensorObj (𝒞 := category) F₂ F₃)).obj j ⟶
      (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) F₁ F₂) F₃).obj j)
    (NatTrans.app (Iso.inv (α_ F₁ F₂ F₃)) j) (Iso.inv (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)))

Tactic:
rw [← cancel_mono ((α_ _ _ _).hom), Iso.inv_hom_id, ← associator_hom_app, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Functor.Monoidal.associator_hom_app, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
K : Type u_5
inst_6 : Category.{v_5, u_5} K
inst_7 : HasColimitsOfShape.{v_5, u_5, v_2, u_2} K C
inst_8 : ∀ (X : C), PreservesColimitsOfShape.{v_5, u_5, v_2, v_2, u_2, u_2} K (tensorLeft X)
F : Functor.{v_1, v_2, u_1, u_2} J C
x : ∀ (k : J), PreservesColimitsOfShape K (tensorLeft F ⋙ obj (evaluation J C) k)
⊢ PreservesColimitsOfShape K (tensorLeft F)

Tactic:
apply preservesColimitsOfShape_of_evaluation

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_evaluation
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
K : Type u_5
inst_6 : Category.{v_5, u_5} K
inst_7 : HasColimitsOfShape.{v_5, u_5, v_2, u_2} K C
inst_8 : ∀ (X : C), PreservesColimitsOfShape.{v_5, u_5, v_2, v_2, u_2, u_2} K (tensorLeft X)
F : Functor.{v_1, v_2, u_1, u_2} J C
k : J
x :
  ∀ (this : tensorLeft F ⋙ obj (evaluation J C) k ≅ obj (evaluation J C) k ⋙ tensorLeft (F.obj k)),
    PreservesColimitsOfShape K (tensorLeft F ⋙ obj (evaluation J C) k)
⊢ PreservesColimitsOfShape K (tensorLeft F ⋙ obj (evaluation J C) k)

Tactic:
haveI : tensorLeft F ⋙ (evaluation J C).obj k ≅ (evaluation J C).obj k ⋙ tensorLeft (F.obj k) :=
    NatIso.ofComponents (fun _ ↦ Iso.refl _)
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
K : Type u_5
inst_6 : Category.{v_5, u_5} K
inst_7 : HasColimitsOfShape.{v_5, u_5, v_2, u_2} K C
inst_8 : ∀ (X : C), PreservesColimitsOfShape.{v_5, u_5, v_2, v_2, u_2, u_2} K (tensorLeft X)
F : Functor.{v_1, v_2, u_1, u_2} J C
k : J
this : tensorLeft F ⋙ obj (evaluation J C) k ≅ obj (evaluation J C) k ⋙ tensorLeft (F.obj k)
⊢ PreservesColimitsOfShape K (tensorLeft F ⋙ obj (evaluation J C) k)

Tactic:
preservesColimitsOfShape_of_natIso this.symm

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_natIso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
K : Type u_5
inst_6 : Category.{v_5, u_5} K
inst_7 : HasColimitsOfShape.{v_5, u_5, v_2, u_2} K C
inst_8 : ∀ (X : C), PreservesColimitsOfShape.{v_5, u_5, v_2, v_2, u_2, u_2} K (tensorLeft X)
F : Functor.{v_1, v_2, u_1, u_2} J C
k : J
this : tensorLeft F ⋙ obj (evaluation J C) k ≅ obj (evaluation J C) k ⋙ tensorLeft (F.obj k)
⊢ PreservesColimitsOfShape K (tensorLeft F ⋙ obj (evaluation J C) k)

Tactic:
exact preservesColimitsOfShape_of_natIso this.symm

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_natIso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_3, v_2, u_3, u_2} D C
H : Functor.{v_2, v_4, u_2, u_4} C E
inst_6 : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
dsimp :
  Eq (α :=
    H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ⟶
      tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
    (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y))
    (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f)))
⊢ (tensorObj (𝒞 := category) F G ⋙ H).map f ≫
      Iso.hom
        ((fun (X : D) ↦
            (prodComparisonIso H (F.obj X) (G.obj X) :
              H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ≅
                tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj X)) (H.obj (G.obj X))))
          Y) =
    Iso.hom
        ((fun (X : D) ↦
            (prodComparisonIso H (F.obj X) (G.obj X) :
              H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ≅
                tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj X)) (H.obj (G.obj X))))
          X) ≫
      (tensorObj (𝒞 := category) (F ⋙ H) (G ⋙ H)).map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_3, v_2, u_3, u_2} D C
H : Functor.{v_2, v_4, u_2, u_4} C E
inst_6 : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
h_fst :
  Eq (α := H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ⟶ H.obj (F.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
      (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y))
      (fst (H.obj (F.obj Y)) (H.obj (G.obj Y))))
    (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
      (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f)))
      (fst (H.obj (F.obj Y)) (H.obj (G.obj Y))))
h_snd :
  Eq (α := H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ⟶ H.obj (G.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
      (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y))
      (snd (H.obj (F.obj Y)) (H.obj (G.obj Y))))
    (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
      (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f)))
      (snd (H.obj (F.obj Y)) (H.obj (G.obj Y))))
⊢ Eq (α :=
    H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ⟶
      tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
    (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y))
    (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_3, v_2, u_3, u_2} D C
H : Functor.{v_2, v_4, u_2, u_4} C E
inst_6 : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ Eq (α := H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ⟶ H.obj (F.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
      (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y))
      (fst (H.obj (F.obj Y)) (H.obj (G.obj Y))))
    (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
      (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f)))
      (fst (H.obj (F.obj Y)) (H.obj (G.obj Y))))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_3, v_2, u_3, u_2} D C
H : Functor.{v_2, v_4, u_2, u_4} C E
inst_6 : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ Eq (α := H.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X)) ⟶ H.obj (G.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
      (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y))
      (snd (H.obj (F.obj Y)) (H.obj (G.obj Y))))
    (CategoryStruct.comp (Y := tensorObj.{v_4, u_4} (𝒞 := inst_3) (H.obj (F.obj Y)) (H.obj (G.obj Y)))
      (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f)))
      (snd (H.obj (F.obj Y)) (H.obj (G.obj Y))))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_2, v, u_2, v + 1} Cᵒᵖ (Type v)
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y
⊢ Eq.{v + 1} (α := (tensorObj (𝒞 := category) F G).obj (Opposite.op I))
    (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
            Equiv.{v_2 + 1, v + 1} (I ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
              ((tensorObj (𝒞 := category) F G).obj (Opposite.op I))) :
          (a : I ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op I))
        (f ≫ g) :
      (tensorObj (𝒞 := category) F G).obj (Opposite.op I))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((tensorObj (𝒞 := category) F G).map f.op) :
          (a : (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op W))) →
            (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op I)))
        (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
                Equiv.{v_2 + 1, v + 1} (W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
                  ((tensorObj (𝒞 := category) F G).obj (Opposite.op W))) :
              (a : W ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op W))
            g :
          (tensorObj (𝒞 := category) F G).obj (Opposite.op W)) :
      (fun (X : Type v) ↦ X) ((tensorObj (𝒞 := category) F G).obj (Opposite.op I)))

Tactic:
Prod.ext ?_ ?_

Premises used: Prod.ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_2, v, u_2, v + 1} Cᵒᵖ (Type v)
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y
refine_1 :
  Eq.{v + 1} (α := F.obj (Opposite.op I))
    (((h₁.homEquiv : Equiv.{v_2 + 1, v + 1} (I ⟶ X) (F.obj (Opposite.op I))) : (a : I ⟶ X) → F.obj (Opposite.op I))
        ((f ≫ g) ≫ fst X Y) :
      F.obj (Opposite.op I))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (Opposite.op W))) → (fun (X : Type v) ↦ X) (F.obj (Opposite.op I)))
        (((h₁.homEquiv : Equiv.{v_2 + 1, v + 1} (W ⟶ X) (F.obj (Opposite.op W))) : (a : W ⟶ X) → F.obj (Opposite.op W))
            (g ≫ fst X Y) :
          F.obj (Opposite.op W)) :
      (fun (X : Type v) ↦ X) (F.obj (Opposite.op I)))
⊢ Eq.{v + 1} (α := F.obj (Opposite.op I))
    (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
            Equiv.{v_2 + 1, v + 1} (I ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
              ((tensorObj (𝒞 := category) F G).obj (Opposite.op I))) :
          (a : I ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op I))
        (f ≫ g)).1
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((tensorObj (𝒞 := category) F G).map f.op) :
          (a : (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op W))) →
            (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op I)))
        (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
                Equiv.{v_2 + 1, v + 1} (W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
                  ((tensorObj (𝒞 := category) F G).obj (Opposite.op W))) :
              (a : W ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op W))
            g :
          (tensorObj (𝒞 := category) F G).obj (Opposite.op W))).1

Tactic:
change h₁.homEquiv ((f ≫ g) ≫ fst X Y) = F.map f.op (h₁.homEquiv (g ≫ fst X Y))

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.RepresentableBy.homEquiv, DFunLike.coe, CategoryTheory.SemiCartesianMonoidalCategory.fst
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_2, v, u_2, v + 1} Cᵒᵖ (Type v)
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y
⊢ Eq.{v + 1} (α := F.obj (Opposite.op I))
    (((h₁.homEquiv : Equiv.{v_2 + 1, v + 1} (I ⟶ X) (F.obj (Opposite.op I))) : (a : I ⟶ X) → F.obj (Opposite.op I))
        ((f ≫ g) ≫ fst X Y) :
      F.obj (Opposite.op I))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (Opposite.op W))) → (fun (X : Type v) ↦ X) (F.obj (Opposite.op I)))
        (((h₁.homEquiv : Equiv.{v_2 + 1, v + 1} (W ⟶ X) (F.obj (Opposite.op W))) : (a : W ⟶ X) → F.obj (Opposite.op W))
            (g ≫ fst X Y) :
          F.obj (Opposite.op W)) :
      (fun (X : Type v) ↦ X) (F.obj (Opposite.op I)))

Tactic:
simp [h₁.homEquiv_comp]

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_2, v, u_2, v + 1} Cᵒᵖ (Type v)
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y
refine_2 :
  Eq.{v + 1} (α := G.obj (Opposite.op I))
    (((h₂.homEquiv : Equiv.{v_2 + 1, v + 1} (I ⟶ Y) (G.obj (Opposite.op I))) : (a : I ⟶ Y) → G.obj (Opposite.op I))
        ((f ≫ g) ≫ snd X Y) :
      G.obj (Opposite.op I))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) :
          (a : (fun (X : Type v) ↦ X) (G.obj (Opposite.op W))) → (fun (X : Type v) ↦ X) (G.obj (Opposite.op I)))
        (((h₂.homEquiv : Equiv.{v_2 + 1, v + 1} (W ⟶ Y) (G.obj (Opposite.op W))) : (a : W ⟶ Y) → G.obj (Opposite.op W))
            (g ≫ snd X Y) :
          G.obj (Opposite.op W)) :
      (fun (X : Type v) ↦ X) (G.obj (Opposite.op I)))
⊢ Eq.{v + 1} (α := G.obj (Opposite.op I))
    (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
            Equiv.{v_2 + 1, v + 1} (I ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
              ((tensorObj (𝒞 := category) F G).obj (Opposite.op I))) :
          (a : I ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op I))
        (f ≫ g)).2
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((tensorObj (𝒞 := category) F G).map f.op) :
          (a : (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op W))) →
            (fun (X : Type v) ↦ X) ((F ⊗ G).obj (Opposite.op I)))
        (((Equiv.trans homEquivToProd (Equiv.prodCongr h₁.homEquiv h₂.homEquiv) :
                Equiv.{v_2 + 1, v + 1} (W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y)
                  ((tensorObj (𝒞 := category) F G).obj (Opposite.op W))) :
              (a : W ⟶ X ⊗ Y) → (F ⊗ G).obj (Opposite.op W))
            g :
          (tensorObj (𝒞 := category) F G).obj (Opposite.op W))).2

Tactic:
change h₂.homEquiv ((f ≫ g) ≫ snd X Y) = G.map f.op (h₂.homEquiv (g ≫ snd X Y))

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.SemiCartesianMonoidalCategory.snd, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.RepresentableBy.homEquiv, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
Goal:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
inst_3 : Category.{v_4, u_4} E
inst_4 : CartesianMonoidalCategory.{v_2, u_2} C
inst_5 : CartesianMonoidalCategory.{v_4, u_4} E
F G : Functor.{v_2, v, u_2, v + 1} Cᵒᵖ (Type v)
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) X Y
⊢ Eq.{v + 1} (α := G.obj (Opposite.op I))
    (((h₂.homEquiv : Equiv.{v_2 + 1, v + 1} (I ⟶ Y) (G.obj (Opposite.op I))) : (a : I ⟶ Y) → G.obj (Opposite.op I))
        ((f ≫ g) ≫ snd X Y) :
      G.obj (Opposite.op I))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) :
          (a : (fun (X : Type v) ↦ X) (G.obj (Opposite.op W))) → (fun (X : Type v) ↦ X) (G.obj (Opposite.op I)))
        (((h₂.homEquiv : Equiv.{v_2 + 1, v + 1} (W ⟶ Y) (G.obj (Opposite.op W))) : (a : W ⟶ Y) → G.obj (Opposite.op W))
            (g ≫ snd X Y) :
          G.obj (Opposite.op W)) :
      (fun (X : Type v) ↦ X) (G.obj (Opposite.op I)))

Tactic:
simp [h₂.homEquiv_comp]

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
F : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
α :
  (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
          GrpCat.carrier)).RepresentableBy
    X
⊢ HMul.hMul (α := (↑(F.obj (op X)) : Type w)) (β := (↑(F.obj (op X)) : Type w))
      ((((α.homEquiv :
                Equiv.{v + 1, w + 1} (X ⟶ X)
                  ((F ⋙
                        forget GrpCat (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                          GrpCat.carrier)).obj
                    (op X))) :
              (a : X ⟶ X) → ToType (F.obj (op X)))
            (𝟙 X))⁻¹ :
        ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
          (F.obj (op X)))
      (((α.homEquiv' (CD := GrpCat.carrier) (FD := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
              Equiv.{v + 1, w + 1} (X ⟶ X)
                (ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
                  (F.obj (op X)))) :
            (a : X ⟶ X) → ToType (F.obj (op X)))
          (𝟙 X) :
        ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
          (F.obj (op X))) =
    1

Tactic:
inv_mul_cancel (α.homEquiv (𝟙 X))

Premises used: inv_mul_cancel, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.RepresentableBy.homEquiv, DFunLike.coe