awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A : C
inst_2 : ComonObj A
⊢ Eq.{v + 1} (α := A ⟶ A) (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A A) Δ (snd A A))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A A) (lift (𝟙 A) (𝟙 A)) (snd A A))

Tactic:
simpa using counit_comul A =≫ snd _ _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.snd, CategoryTheory.ComonObj.counit_comul
-- 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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
w :
  ∀ (x : J),
    Eq (α := (tensorObj (𝒞 := category) X Y).obj x ⟶ X.obj x)
      (NatTrans.app { app := fun (x : J) ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ } x)
      (NatTrans.app
        (X ◁
            IsTerminal.from
              (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
                fun (x : J) ↦
                isLimitChangeEmptyCone C isTerminalTensorUnit
                  (mapCone (obj (evaluation J C) x)
                    (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
                  (Iso.refl (Cone.pt.{0, v_2, 0, u_2} (asEmptyCone (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))))
              Y ≫
          Iso.hom (ρ_ X))
        x)
⊢ Eq (α := tensorObj (𝒞 := category) X Y ⟶ X) { app := fun (x : J) ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ }
    (X ◁
        IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
            fun (x : J) ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit
              (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
              (Iso.refl (Cone.pt.{0, v_2, 0, u_2} (asEmptyCone (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))))
          Y ≫
      Iso.hom (ρ_ X))

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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
x : J
w :
  Eq.{v_2 + 1} (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (X.obj x) (Y.obj x) ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) (X.obj x) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
    (X.obj x ◁ IsTerminal.from isTerminalTensorUnit (Y.obj x))
    (X.obj x ◁
      NatTrans.app
        (IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
            fun (x : J) ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit
              (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
              (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
          Y)
        x)
⊢ Eq (α := (tensorObj (𝒞 := category) X Y).obj x ⟶ X.obj x)
    (NatTrans.app { app := fun (x : J) ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ } x)
    (NatTrans.app
      (X ◁
          IsTerminal.from
            (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
              fun (x : J) ↦
              isLimitChangeEmptyCone C isTerminalTensorUnit
                (mapCone (obj (evaluation J C) x)
                  (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
                (Iso.refl (Cone.pt.{0, v_2, 0, u_2} (asEmptyCone (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))))
            Y ≫
        Iso.hom (ρ_ X))
      x)

Tactic:
simp only [Monoidal.tensorObj_obj, fst_def, asEmptyCone_pt, NatTrans.comp_app,
      Monoidal.tensorUnit_obj, Monoidal.whiskerLeft_app, Monoidal.rightUnitor_hom_app,
      Iso.cancel_iso_hom_right]

Premises used: CategoryTheory.Limits.asEmptyCone_pt, CategoryTheory.Monoidal.tensorUnit_obj, CategoryTheory.Monoidal.tensorObj_obj, CategoryTheory.Monoidal.rightUnitor_hom_app, CategoryTheory.Iso.cancel_iso_hom_right, CategoryTheory.NatTrans.comp_app, CategoryTheory.SemiCartesianMonoidalCategory.fst_def, CategoryTheory.Monoidal.whiskerLeft_app
-- 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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
x : J
w :
  Eq.{v_2 + 1} (α := Y.obj x ⟶ tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (IsTerminal.from isTerminalTensorUnit (Y.obj x))
    (NatTrans.app
      (IsTerminal.from
        (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
          fun (x : J) ↦
          isLimitChangeEmptyCone C isTerminalTensorUnit
            (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
            (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
        Y)
      x)
⊢ Eq.{v_2 + 1} (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (X.obj x) (Y.obj x) ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) (X.obj x) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
    (X.obj x ◁ IsTerminal.from isTerminalTensorUnit (Y.obj x))
    (X.obj x ◁
      NatTrans.app
        (IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
            fun (x : J) ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit
              (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
              (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
          Y)
        x)

Tactic:
congr
-- 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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
x : J
⊢ Eq.{v_2 + 1} (α := Y.obj x ⟶ tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (IsTerminal.from isTerminalTensorUnit (Y.obj x))
    (NatTrans.app
      (IsTerminal.from
        (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
          fun (x : J) ↦
          isLimitChangeEmptyCone C isTerminalTensorUnit
            (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
            (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
        Y)
      x)

Tactic:
subsingleton
-- 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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
w :
  ∀ (x : J),
    Eq (α := (tensorObj (𝒞 := category) X Y).obj x ⟶ Y.obj x)
      (NatTrans.app { app := fun (x : J) ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ } x)
      (NatTrans.app
        (IsTerminal.from
              (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
                fun (x : J) ↦
                isLimitChangeEmptyCone C isTerminalTensorUnit
                  (mapCone (obj (evaluation J C) x)
                    (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
                  (Iso.refl (Cone.pt.{0, v_2, 0, u_2} (asEmptyCone (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))))
              X ▷
            Y ≫
          Iso.hom (λ_ Y))
        x)
⊢ Eq (α := tensorObj (𝒞 := category) X Y ⟶ Y) { app := fun (x : J) ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ }
    (IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
            fun (x : J) ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit
              (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
              (Iso.refl (Cone.pt.{0, v_2, 0, u_2} (asEmptyCone (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))))
          X ▷
        Y ≫
      Iso.hom (λ_ Y))

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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
x : J
w :
  Eq.{v_2 + 1} (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (X.obj x) (Y.obj x) ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (Y.obj x))
    (IsTerminal.from isTerminalTensorUnit (X.obj x) ▷ Y.obj x)
    (NatTrans.app
        (IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
            fun (x : J) ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit
              (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
              (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
          X)
        x ▷
      Y.obj x)
⊢ Eq (α := (tensorObj (𝒞 := category) X Y).obj x ⟶ Y.obj x)
    (NatTrans.app { app := fun (x : J) ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ } x)
    (NatTrans.app
      (IsTerminal.from
            (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
              fun (x : J) ↦
              isLimitChangeEmptyCone C isTerminalTensorUnit
                (mapCone (obj (evaluation J C) x)
                  (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
                (Iso.refl (Cone.pt.{0, v_2, 0, u_2} (asEmptyCone (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))))
            X ▷
          Y ≫
        Iso.hom (λ_ Y))
      x)

Tactic:
simp only [Monoidal.tensorObj_obj, snd_def, asEmptyCone_pt, NatTrans.comp_app,
      Monoidal.tensorUnit_obj, Monoidal.whiskerRight_app, Monoidal.leftUnitor_hom_app,
      Iso.cancel_iso_hom_right]

Premises used: CategoryTheory.Monoidal.leftUnitor_hom_app, CategoryTheory.Limits.asEmptyCone_pt, CategoryTheory.Monoidal.whiskerRight_app, CategoryTheory.Monoidal.tensorUnit_obj, CategoryTheory.Monoidal.tensorObj_obj, CategoryTheory.Iso.cancel_iso_hom_right, CategoryTheory.NatTrans.comp_app, CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- 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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
x : J
w :
  Eq.{v_2 + 1} (α := X.obj x ⟶ tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (IsTerminal.from isTerminalTensorUnit (X.obj x))
    (NatTrans.app
      (IsTerminal.from
        (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
          fun (x : J) ↦
          isLimitChangeEmptyCone C isTerminalTensorUnit
            (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
            (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
        X)
      x)
⊢ Eq.{v_2 + 1} (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (X.obj x) (Y.obj x) ⟶
      tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (Y.obj x))
    (IsTerminal.from isTerminalTensorUnit (X.obj x) ▷ Y.obj x)
    (NatTrans.app
        (IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
            fun (x : J) ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit
              (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
              (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
          X)
        x ▷
      Y.obj x)

Tactic:
congr
-- 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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
x : J
⊢ Eq.{v_2 + 1} (α := X.obj x ⟶ tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (IsTerminal.from isTerminalTensorUnit (X.obj x))
    (NatTrans.app
      (IsTerminal.from
        (evaluationJointlyReflectsLimits (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)))
          fun (x : J) ↦
          isLimitChangeEmptyCone C isTerminalTensorUnit
            (mapCone (obj (evaluation J C) x) (asEmptyCone ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))))
            (Iso.refl (tensorUnit.{v_2, u_2} C (𝒞 := inst_1))))
        X)
      x)

Tactic:
subsingleton
-- 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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
j : J
⊢ (pair X Y ⋙ obj (evaluation J C) j).obj { as := WalkingPair.left : Discrete WalkingPair } ≅
    obj.{0, v_2, 0, u_2} (pair (X.obj j) (Y.obj j)) { as := WalkingPair.left : Discrete WalkingPair }

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.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
X Y : Functor.{v_1, v_2, u_1, u_2} J C
j : J
⊢ (pair X Y ⋙ obj (evaluation J C) j).obj { as := WalkingPair.right : Discrete WalkingPair } ≅
    obj.{0, v_2, 0, u_2} (pair (X.obj j) (Y.obj j)) { as := WalkingPair.right : Discrete WalkingPair }

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- 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
j : J
⊢ (tensorObj (𝒞 := category) F₁ F₂).obj j = tensorObj.{v_2, u_2} (𝒞 := inst_1) (F₁.obj j) (F₂.obj j)

Tactic:
rfl

Premises used: rfl
-- 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
j j' : J
f : j ⟶ j'
⊢ (tensorObj (𝒞 := category) F₁ F₂).map f = F₁.map f ⊗ₘ F₂.map f

Tactic:
rfl

Premises used: rfl
-- 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
j : J
⊢ Eq (α := (tensorObj (𝒞 := category) F₁ F₂).obj j ⟶ F₁.obj j) (NatTrans.app (fst F₁ F₂) j) (fst (F₁.obj j) (F₂.obj j))

Tactic:
rfl

Premises used: rfl
-- 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
j : J
⊢ Eq (α := (tensorObj (𝒞 := category) F₁ F₂).obj j ⟶ F₂.obj j) (NatTrans.app (snd F₁ F₂) j) (snd (F₁.obj j) (F₂.obj j))

Tactic:
rfl

Premises used: rfl
-- 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 : Functor.{v_1, v_2, u_1, u_2} J C
j : J
⊢ Eq (α := (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j ⟶ F.obj j)
    (NatTrans.app (Iso.hom (λ_ F)) j) (Iso.hom (λ_ (F.obj j)))

Tactic:
rfl

Premises used: rfl
-- 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 : Functor.{v_1, v_2, u_1, u_2} J C
j : J
rw :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
      (NatTrans.app (Iso.inv (λ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j)
      (Iso.hom (λ_ (F.obj j))) =
    CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
      (Iso.inv (λ_ (F.obj j))) (Iso.hom (λ_ (F.obj j)))
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
      (NatTrans.app (Iso.inv (λ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j)
      (Iso.hom (λ_ (F.obj j))) =
    𝟙 (F.obj j)
rw₂ :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)) (F.obj j))
      (NatTrans.app (Iso.inv (λ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j)
      (NatTrans.app (Iso.hom (λ_ F)) j) =
    𝟙 (F.obj j)
rw₃ rw₄ : Eq.{v_2 + 1} (α := F.obj j ⟶ F.obj j) (𝟙 (F.obj j)) (𝟙 (F.obj j))
⊢ Eq (α := F.obj j ⟶ (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category)) F).obj j)
    (NatTrans.app (Iso.inv (λ_ F)) j) (Iso.inv (λ_ (F.obj j)))

Tactic:
rw [← cancel_mono ((λ_ (F.obj j)).hom), Iso.inv_hom_id, ← leftUnitor_hom_app,
    Iso.inv_hom_id_app]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Functor.Monoidal.leftUnitor_hom_app, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj
-- 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 : Functor.{v_1, v_2, u_1, u_2} J C
j : J
⊢ Eq (α := (tensorObj (𝒞 := category) F ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))).obj j ⟶ F.obj j)
    (NatTrans.app (Iso.hom (ρ_ F)) j) (Iso.hom (ρ_ (F.obj j)))

Tactic:
rfl

Premises used: rfl
-- 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 : Functor.{v_1, v_2, u_1, u_2} J C
j : J
rw :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj j) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
      (NatTrans.app (Iso.inv (ρ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) F ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))).obj j)
      (Iso.hom (ρ_ (F.obj j))) =
    CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj j) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
      (Iso.inv (ρ_ (F.obj j))) (Iso.hom (ρ_ (F.obj j)))
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj j) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
      (NatTrans.app (Iso.inv (ρ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) F ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))).obj j)
      (Iso.hom (ρ_ (F.obj j))) =
    𝟙 (F.obj j)
rw₂ :
  CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj j) (tensorUnit.{v_2, u_2} C (𝒞 := inst_1)))
      (NatTrans.app (Iso.inv (ρ_ F)) j :
        F.obj j ⟶ (tensorObj (𝒞 := category) F ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))).obj j)
      (NatTrans.app (Iso.hom (ρ_ F)) j) =
    𝟙 (F.obj j)
rw₃ rw₄ : Eq.{v_2 + 1} (α := F.obj j ⟶ F.obj j) (𝟙 (F.obj j)) (𝟙 (F.obj j))
⊢ Eq (α := F.obj j ⟶ (tensorObj (𝒞 := category) F ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} J C)) (𝒞 := category))).obj j)
    (NatTrans.app (Iso.inv (ρ_ F)) j) (Iso.inv (ρ_ (F.obj j)))

Tactic:
rw [← cancel_mono ((ρ_ (F.obj j)).hom), Iso.inv_hom_id, ← rightUnitor_hom_app,
    Iso.inv_hom_id_app]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.hom, CategoryTheory.Functor.Monoidal.rightUnitor_hom_app, CategoryTheory.Functor.obj
-- 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₂ F₂' : Functor.{v_1, v_2, u_1, u_2} J C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ Eq (α := (tensorObj (𝒞 := category) F₁ F₂).obj j ⟶ F₁'.obj j) (NatTrans.app (f ⊗ₘ g) j ≫ fst (F₁'.obj j) (F₂'.obj j))
    (fst (F₁.obj j) (F₂.obj j) ≫ f.app 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₂ F₂' : Functor.{v_1, v_2, u_1, u_2} J C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ Eq (α := (tensorObj (𝒞 := category) F₁ F₂).obj j ⟶ F₂'.obj j) (NatTrans.app (f ⊗ₘ g) j ≫ snd (F₁'.obj j) (F₂'.obj j))
    (snd (F₁.obj j) (F₂.obj j) ≫ g.app 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
g : F₂ ⟶ F₂'
j : J
⊢ Eq (α := (tensorObj (𝒞 := category) F₁ F₂).obj j ⟶ F₁.obj j) (NatTrans.app (F₁ ◁ g) j ≫ fst (F₁.obj j) (F₂'.obj j))
    (fst (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
g : F₂ ⟶ F₂'
j : J
⊢ Eq (α := (tensorObj (𝒞 := category) F₁ F₂).obj j ⟶ F₂'.obj j) (NatTrans.app (F₁ ◁ g) j ≫ snd (F₁.obj j) (F₂'.obj j))
    (snd (F₁.obj j) (F₂.obj j) ≫ g.app 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₁' : 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 ≫ fst (F₁'.obj j) (F₂.obj j))
    (fst (F₁.obj j) (F₂.obj j) ≫ f.app j)

Tactic:
simp