awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Monoidal
inst_7 : G.Monoidal
α : F ⟶ G
X Y : C
h_fst :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ G.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
        (Iso.inv (Functor.Monoidal.μIso F X Y))
        (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
          (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y))))
      (fst (G.obj X) (G.obj Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
        (Iso.inv (Functor.Monoidal.μIso F X Y))
        (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
          (Iso.inv (Functor.Monoidal.μIso G X Y))))
      (fst (G.obj X) (G.obj Y)))
h_snd :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ G.obj Y)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
        (Iso.inv (Functor.Monoidal.μIso F X Y))
        (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
          (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y))))
      (snd (G.obj X) (G.obj Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
        (Iso.inv (Functor.Monoidal.μIso F X Y))
        (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
          (Iso.inv (Functor.Monoidal.μIso G X Y))))
      (snd (G.obj X) (G.obj Y)))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (Iso.inv (Functor.Monoidal.μIso F X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
        (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y))))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (Iso.inv (Functor.Monoidal.μIso F X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
        (Iso.inv (Functor.Monoidal.μIso G X Y))))

Tactic:
apply CartesianMonoidalCategory.hom_ext

Premises used: CategoryTheory.CartesianMonoidalCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Monoidal
inst_7 : G.Monoidal
α : F ⟶ G
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ G.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
        (Iso.inv (Functor.Monoidal.μIso F X Y))
        (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
          (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y))))
      (fst (G.obj X) (G.obj Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
        (Iso.inv (Functor.Monoidal.μIso F X Y))
        (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
          (Iso.inv (Functor.Monoidal.μIso G X Y))))
      (fst (G.obj X) (G.obj Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Monoidal
inst_7 : G.Monoidal
α : F ⟶ G
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ G.obj Y)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
        (Iso.inv (Functor.Monoidal.μIso F X Y))
        (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
          (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y))))
      (snd (G.obj X) (G.obj Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
        (Iso.inv (Functor.Monoidal.μIso F X Y))
        (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
          (Iso.inv (Functor.Monoidal.μIso G X Y))))
      (snd (G.obj X) (G.obj Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
C : Type u
inst : Category.{v, u} C
x : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C
h_map :
  autoParam
    (∀ (X Y : (↑chosenTerminal : Type u_1)) (f : X ⟶ Y),
      Functor.map
          (Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
            ((fun (F : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C) ↦ F.obj { down := { as := () } }) x))
          f =
        eqToHom ⋯ ≫ x.map f ≫ eqToHom ⋯)
    Functor.ext._auto_1
h_obj :
  ∀ (X : (↑chosenTerminal : Type u_1)),
    Functor.obj.{u_2, v, u_1, u}
        (Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
          ((fun (F : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C) ↦ F.obj { down := { as := () } }) x))
        X =
      x.obj X
⊢ Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
      ((fun (F : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C) ↦ F.obj { down := { as := () } }) x) =
    x

Tactic:
apply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
C : Type u
inst : Category.{v, u} C
x : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C
⊢ Functor.map
      (Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
        (x.obj { down := { as := () : Discrete Unit } : ULift.{u_1, 0} (ULiftHom (Discrete Unit)) }))
      { down := { down := { down := ⋯ } } } =
    x.map
      {
        down :=
          {
            down :=
              { down := ⋯ :
                PLift
                  ((ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }).as =
                    (ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }).as) } :
            ULift.{0, 0}
              (PLift
                ((ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }).as =
                  (ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }).as)) } :
        ULift.{u_2, 0}
          (ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit } ⟶
            ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }) }

Tactic:
(Functor.map_id _ _).symm

Premises used: CategoryTheory.Functor.map_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
C : Type u
inst : Category.{v, u} C
x : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C
⊢ Functor.map
      (Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
        (x.obj { down := { as := () : Discrete Unit } : ULift.{u_1, 0} (ULiftHom (Discrete Unit)) }))
      { down := { down := { down := ⋯ } } } =
    x.map
      {
        down :=
          {
            down :=
              { down := ⋯ :
                PLift
                  ((ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }).as =
                    (ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }).as) } :
            ULift.{0, 0}
              (PLift
                ((ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }).as =
                  (ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }).as)) } :
        ULift.{u_2, 0}
          (ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit } ⟶
            ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }) }

Tactic:
exact (Functor.map_id _ _).symm

Premises used: CategoryTheory.Functor.map_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
C : Type u
inst : Category.{v, u} C
x : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C
X : (↑chosenTerminal : Type u_1)
⊢ Functor.obj.{u_2, v, u_1, u}
      (Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
        ((fun (F : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C) ↦ F.obj { down := { as := () } }) x))
      X =
    x.obj X

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
X Y : Cat
x : BinaryFan X Y
x_1 : x.pt ⟶ of ((↑X : Type u_2) × (↑Y : Type u_2))
h1 : x_1 ≫ Functor.toCatHom (Prod.fst (↑X : Type u_2) (↑Y : Type u_2)) = x.fst
h2 : x_1 ≫ Functor.toCatHom (Prod.snd (↑X : Type u_2) (↑Y : Type u_2)) = x.snd
x_2 : (↑x.pt : Type u_2)
⊢ (x_1.toFunctor.obj x_2).1 =
    (Functor.obj (Hom.toFunctor ((fun (S : BinaryFan X Y) ↦ (S.fst.toFunctor.prod' S.snd.toFunctor).toCatHom) x)) x_2).1

Tactic:
simp [← h1]
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
X Y : Cat
x : BinaryFan X Y
x_1 : x.pt ⟶ of ((↑X : Type u_2) × (↑Y : Type u_2))
h1 : x_1 ≫ Functor.toCatHom (Prod.fst (↑X : Type u_2) (↑Y : Type u_2)) = x.fst
h2 : x_1 ≫ Functor.toCatHom (Prod.snd (↑X : Type u_2) (↑Y : Type u_2)) = x.snd
x_2 : (↑x.pt : Type u_2)
⊢ (x_1.toFunctor.obj x_2).2 =
    (Functor.obj (Hom.toFunctor ((fun (S : BinaryFan X Y) ↦ (S.fst.toFunctor.prod' S.snd.toFunctor).toCatHom) x)) x_2).2

Tactic:
simp [← h2]
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
X Y : Cat
x : BinaryFan X Y
x_1 : x.pt ⟶ of ((↑X : Type u_2) × (↑Y : Type u_2))
h1 : x_1 ≫ Functor.toCatHom (Prod.fst (↑X : Type u_2) (↑Y : Type u_2)) = x.fst
h2 : x_1 ≫ Functor.toCatHom (Prod.snd (↑X : Type u_2) (↑Y : Type u_2)) = x.snd
x_2 x_3 : (↑x.pt : Type u_2)
x_4 : x_2 ⟶ x_3
dsimp : x_1.toFunctor.map x_4 ≍ Prod.mkHom (x.fst.toFunctor.map x_4) (x.snd.toFunctor.map x_4)
⊢ HEq (x_1.toFunctor.map x_4) (β :=
    Quiver.Hom (V := (↑(of ((↑X : Type u_2) × (↑Y : Type u_2))) : Type u_2))
      (Functor.obj (Hom.toFunctor ((fun (S : BinaryFan X Y) ↦ (S.fst.toFunctor.prod' S.snd.toFunctor).toCatHom) x)) x_2)
      (Functor.obj (Hom.toFunctor ((fun (S : BinaryFan X Y) ↦ (S.fst.toFunctor.prod' S.snd.toFunctor).toCatHom) x))
        x_3))
    (Functor.map (Hom.toFunctor ((fun (S : BinaryFan X Y) ↦ (S.fst.toFunctor.prod' S.snd.toFunctor).toCatHom) x)) x_4)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
X Y : Cat
x : BinaryFan X Y
x_1 : x.pt ⟶ of ((↑X : Type u_2) × (↑Y : Type u_2))
h1 : x_1 ≫ Functor.toCatHom (Prod.fst (↑X : Type u_2) (↑Y : Type u_2)) = x.fst
h2 : x_1 ≫ Functor.toCatHom (Prod.snd (↑X : Type u_2) (↑Y : Type u_2)) = x.snd
x_2 x_3 : (↑x.pt : Type u_2)
x_4 : x_2 ⟶ x_3
rw :
  x_1.toFunctor.map x_4 ≍
    Prod.mkHom ((x_1 ≫ Functor.toCatHom (Prod.fst (↑X : Type u_2) (↑Y : Type u_2))).toFunctor.map x_4)
      ((x_1 ≫ Functor.toCatHom (Prod.snd (↑X : Type u_2) (↑Y : Type u_2))).toFunctor.map x_4)
⊢ x_1.toFunctor.map x_4 ≍ Prod.mkHom (x.fst.toFunctor.map x_4) (x.snd.toFunctor.map x_4)

Tactic:
rw [← h1, ← h2]
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
X Y : Cat
x : BinaryFan X Y
x_1 : x.pt ⟶ of ((↑X : Type u_2) × (↑Y : Type u_2))
h1 : x_1 ≫ Functor.toCatHom (Prod.fst (↑X : Type u_2) (↑Y : Type u_2)) = x.fst
h2 : x_1 ≫ Functor.toCatHom (Prod.snd (↑X : Type u_2) (↑Y : Type u_2)) = x.snd
x_2 x_3 : (↑x.pt : Type u_2)
x_4 : x_2 ⟶ x_3
⊢ x_1.toFunctor.map x_4 ≍
    Prod.mkHom ((x_1 ≫ Functor.toCatHom (Prod.fst (↑X : Type u_2) (↑Y : Type u_2))).toFunctor.map x_4)
      ((x_1 ≫ Functor.toCatHom (Prod.snd (↑X : Type u_2) (↑Y : Type u_2))).toFunctor.map x_4)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
⊢ MonoidalCategory Cat

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
⊢ SymmetricCategory Cat

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
C D : Cat
⊢ MonoidalCategoryStruct.tensorObj (𝒞 := Cat.category) C D = Cat.of ((↑C : Type u_2) × (↑D : Type u_2))

Tactic:
rfl

Premises used: CategoryTheory.Cat.of, CategoryTheory.Bundled.of, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
X A B : Cat
F : A ⟶ B
⊢ X ◁ F = Functor.toCatHom (Functor.prod (𝟭 (↑X : Type u_2)) F.toFunctor)

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, CategoryTheory.Functor.prod, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
X A B : Cat
f : A ⟶ B
⊢ Cat.Hom.toFunctor (X ◁ f) ⋙ Prod.fst (↑X : Type u_2) (↑B : Type u_2) = Prod.fst (↑X : Type u_2) (↑A : Type u_2)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Prod.fst, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
X A B : Cat
f : A ⟶ B
⊢ Cat.Hom.toFunctor (X ◁ f) ⋙ Prod.snd (↑X : Type u_2) (↑B : Type u_2) =
    Prod.snd (↑X : Type u_2) (↑A : Type u_2) ⋙ f.toFunctor

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.prod', CategoryTheory.Prod.snd, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
A B : Cat
f : A ⟶ B
X : Cat
⊢ f ▷ X = Functor.toCatHom (f.toFunctor.prod (𝟭 (↑X : Type u_2)))

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, CategoryTheory.Functor.prod, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
A B : Cat
f : A ⟶ B
X : Cat
⊢ Cat.Hom.toFunctor (f ▷ X) ⋙ Prod.fst (↑B : Type u_2) (↑X : Type u_2) =
    Prod.fst (↑A : Type u_2) (↑X : Type u_2) ⋙ f.toFunctor

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.prod', CategoryTheory.Prod.fst, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
A B : Cat
f : A ⟶ B
X : Cat
⊢ Cat.Hom.toFunctor (f ▷ X) ⋙ Prod.snd (↑B : Type u_2) (↑X : Type u_2) = Prod.snd (↑A : Type u_2) (↑X : Type u_2)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Prod.snd, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
A B : Cat
f : A ⟶ B
X Y : Cat
g : X ⟶ Y
⊢ f ⊗ₘ g = (f.toFunctor.prod g.toFunctor).toCatHom

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, CategoryTheory.Functor.prod, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
⊢ (𝟙_ Cat) (𝒞 := Cat.category) = Cat.chosenTerminal

Tactic:
rfl

Premises used: CategoryTheory.Cat.of, CategoryTheory.Bundled.of, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
X Y Z : Cat
⊢ Iso.hom (α_ X Y Z) =
    Functor.toCatHom
      (Functor.prod'
        (Prod.fst ((↑X : Type u_2) × (↑Y : Type u_2)) (↑Z : Type u_2) ⋙ Prod.fst (↑X : Type u_2) (↑Y : Type u_2))
        (Functor.prod'
          (Prod.fst ((↑X : Type u_2) × (↑Y : Type u_2)) (↑Z : Type u_2) ⋙ Prod.snd (↑X : Type u_2) (↑Y : Type u_2))
          (Prod.snd ((↑X : Type u_2) × (↑Y : Type u_2)) (↑Z : Type u_2))))

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, CategoryTheory.Functor.comp, CategoryTheory.Functor.prod', rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
X Y Z : Cat
⊢ Iso.inv (α_ X Y Z) =
    Functor.toCatHom
      (Functor.prod'
        (Functor.prod' (Prod.fst (↑X : Type u_2) ((↑Y : Type u_2) × (↑Z : Type u_2)))
          (Prod.snd (↑X : Type u_2) ((↑Y : Type u_2) × (↑Z : Type u_2)) ⋙ Prod.fst (↑Y : Type u_2) (↑Z : Type u_2)))
        (Prod.snd (↑X : Type u_2) ((↑Y : Type u_2) × (↑Z : Type u_2)) ⋙ Prod.snd (↑Y : Type u_2) (↑Z : Type u_2)))

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, CategoryTheory.Functor.comp, CategoryTheory.Functor.prod', rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
C : Cat
⊢ Iso.hom (λ_ C) = Functor.toCatHom (Prod.snd (↑((𝟙_ Cat) (𝒞 := Cat.category)) : Type u) (↑C : Type u))

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
C : Cat
⊢ Iso.inv (λ_ C) =
    Functor.toCatHom
      (Prod.sectR { down := { as := PUnit.unit : Discrete Unit } : ULift.{u, 0} (ULiftHom (Discrete Unit)) }
        (↑C : Type u))

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, CategoryTheory.Prod.sectR, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
C : Cat
⊢ Iso.hom (ρ_ C) = Functor.toCatHom (Prod.fst (↑C : Type u) (↑((𝟙_ Cat) (𝒞 := Cat.category)) : Type u))

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
C : Cat
⊢ Iso.inv (ρ_ C) =
    Functor.toCatHom
      (Prod.sectL (↑C : Type u)
        { down := { as := PUnit.unit : Discrete Unit } : ULift.{u, 0} (ULiftHom (Discrete Unit)) })

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, CategoryTheory.Prod.sectL, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X : C
G : CommGrp.{v, u} C
H I : (Grp.{v, u} C)ᵒᵖ
f : H ⟶ I
h :
  Eq (α := (unop I).toMon.X ⟶ G.toGrp.toMon.X) (Mon.Hom.hom (InducedCategory.Hom.hom (f.unop ≫ 1)))
    (Mon.Hom.hom (InducedCategory.Hom.hom 1))
⊢ Eq (α := unop I ⟶ G.toGrp) (f.unop ≫ 1) 1

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X : C
G : CommGrp.{v, u} C
H I : (Grp.{v, u} C)ᵒᵖ
f : H ⟶ I
⊢ Eq (α := (unop I).toMon.X ⟶ G.toGrp.toMon.X) (Mon.Hom.hom (InducedCategory.Hom.hom (f.unop ≫ 1)))
    (Mon.Hom.hom (InducedCategory.Hom.hom 1))

Tactic:
simp [Mon.Hom.hom_one]

Premises used: CategoryTheory.Mon.Hom.hom_one
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X : C
G : CommGrp.{v, u} C
H I : (Grp.{v, u} C)ᵒᵖ
f : H ⟶ I
g h : unop H ⟶ G.toGrp
h₁ : (f.unop ≫ (g * h)).hom.hom = (f.unop ≫ g * f.unop ≫ h).hom.hom
⊢ f.unop ≫ (g * h) = f.unop ≫ g * f.unop ≫ h

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X : C
G : CommGrp.{v, u} C
H I : (Grp.{v, u} C)ᵒᵖ
f : H ⟶ I
g h : unop H ⟶ G.toGrp
⊢ (f.unop ≫ (g * h)).hom.hom = (f.unop ≫ g * f.unop ≫ h).hom.hom

Tactic:
simpa using ((yonedaGrpObj G.X).map f.unop.hom.hom.op).hom.map_mul g.hom.hom h.hom.hom

Premises used: GrpCat.Hom.hom, Quiver.Hom.op, CategoryTheory.Mon.Hom.hom, Quiver.Hom.unop, CategoryTheory.CommGrp.X, CategoryTheory.Functor.map, CategoryTheory.InducedCategory.Hom.hom, MonoidHom.map_mul, CategoryTheory.yonedaGrpObj
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X : C
X₁ X₂ : CommGrp.{v, u} C
ψ : X₁ ⟶ X₂
Y : (Grp.{v, u} C)ᵒᵖ
h :
  Eq (α := (unop Y).toMon.X ⟶ X₂.toGrp.toMon.X) (Mon.Hom.hom (InducedCategory.Hom.hom (1 ≫ ψ.hom)))
    (Mon.Hom.hom (InducedCategory.Hom.hom 1))
⊢ Eq (α := unop Y ⟶ X₂.toGrp) (1 ≫ ψ.hom) 1

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X : C
X₁ X₂ : CommGrp.{v, u} C
ψ : X₁ ⟶ X₂
Y : (Grp.{v, u} C)ᵒᵖ
⊢ Eq (α := (unop Y).toMon.X ⟶ X₂.toGrp.toMon.X) (Mon.Hom.hom (InducedCategory.Hom.hom (1 ≫ ψ.hom)))
    (Mon.Hom.hom (InducedCategory.Hom.hom 1))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X : C
X₁ X₂ : CommGrp.{v, u} C
ψ : X₁ ⟶ X₂
Y : (Grp.{v, u} C)ᵒᵖ
f g : unop Y ⟶ X₁.toGrp
h : ((f * g) ≫ ψ.hom).hom.hom = (f ≫ ψ.hom * g ≫ ψ.hom).hom.hom
⊢ (f * g) ≫ ψ.hom = f ≫ ψ.hom * g ≫ ψ.hom

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X : C
X₁ X₂ : CommGrp.{v, u} C
ψ : X₁ ⟶ X₂
Y : (Grp.{v, u} C)ᵒᵖ
f g : unop Y ⟶ X₁.toGrp
⊢ ((f * g) ≫ ψ.hom).hom.hom = (f ≫ ψ.hom * g ≫ ψ.hom).hom.hom

Tactic:
simpa using ((yonedaGrp.map ψ.hom).app (op (unop Y).X)).hom.map_mul f.hom.hom g.hom.hom

Premises used: GrpCat.Hom.hom, CategoryTheory.Mon.Hom.hom, CategoryTheory.Functor.map, Opposite.op, CategoryTheory.yonedaGrp, CategoryTheory.InducedCategory.Hom.hom, MonoidHom.map_mul, Opposite.unop, CategoryTheory.Grp.X, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    Comon.X.{v, u}
        { X := X,
          comon :=
            { counit := toUnit X, comul := lift (𝟙 X) (𝟙 X), counit_comul := ⋯, comul_counit := ⋯, comul_assoc := ⋯ } :
          Comon.{v, u} C } ⟶
      tensorObj.{v, u} (𝒞 := inst)
        (Comon.X.{v, u}
          { X := Y,
            comon :=
              { counit := toUnit Y, comul := lift (𝟙 Y) (𝟙 Y), counit_comul := ⋯, comul_counit := ⋯,
                comul_assoc := ⋯ } })
        (Comon.X.{v, u}
          { X := Y,
            comon :=
              { counit := toUnit Y, comul := lift (𝟙 Y) (𝟙 Y), counit_comul := ⋯, comul_counit := ⋯,
                comul_assoc := ⋯ } }))
    (f ≫ Δ) (Δ ≫ (f ⊗ₘ f))

Tactic:
simp +instances
-- 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 ⟶ tensorUnit.{v, u} C (𝒞 := inst)) ε (toUnit A)

Tactic:
ext
-- 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
h_fst :
  Eq.{v + 1} (α := A ⟶ A) (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A A) Δ (fst A A))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A A) (lift (𝟙 A) (𝟙 A)) (fst A A))
h_snd :
  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))
⊢ Eq.{v + 1} (α := A ⟶ tensorObj.{v, u} (𝒞 := inst) A A) Δ (lift (𝟙 A) (𝟙 A))

Tactic:
ext
-- 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) Δ (fst A A))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A A) (lift (𝟙 A) (𝟙 A)) (fst A A))

Tactic:
simpa using comul_counit A =≫ fst _ _

Premises used: CategoryTheory.ComonObj.comul_counit, CategoryTheory.SemiCartesianMonoidalCategory.fst