awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
inst_8 : IsCommMonObj.{v, u_1} M
f g : X ⟶ M
⊢ f * g = g * f

Tactic:
simpa [-IsCommMonObj.mul_comm] using lift g f ≫= IsCommMonObj.mul_comm M

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, CategoryTheory.IsCommMonObj.mul_comm
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
inst_3 : IsCommMonObj.{v, u_1} N.X
⊢ Eq.{v + 1} (α := M.X ⟶ N.X) (hom 1) 1

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.SemiCartesianMonoidalCategory.toUnit, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
inst_3 : IsCommMonObj.{v, u_1} N.X
f g : M ⟶ N
⊢ (f * g).hom = f.hom * g.hom

Tactic:
rfl

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
inst_3 : IsCommMonObj.{v, u_1} N.X
f : M ⟶ N
n : ℕ
zero : (HPow.hPow (β := ℕ) f 0).hom = HPow.hPow (β := ℕ) f.hom 0
succ : ∀ (n : ℕ), (f ^ n).hom = f.hom ^ n → (f ^ (n + 1)).hom = f.hom ^ (n + 1)
⊢ (f ^ n).hom = f.hom ^ n

Tactic:
induction n
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
inst_3 : IsCommMonObj.{v, u_1} N.X
f : M ⟶ N
⊢ (HPow.hPow (β := ℕ) f 0).hom = HPow.hPow (β := ℕ) f.hom 0

Tactic:
simp [pow_succ, *]

Premises used: pow_succ
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
inst_3 : IsCommMonObj.{v, u_1} N.X
f : M ⟶ N
n : ℕ
h : (f ^ n).hom = f.hom ^ n
⊢ (f ^ (n + 1)).hom = f.hom ^ (n + 1)

Tactic:
simp [pow_succ, *]

Premises used: pow_succ
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X_1 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f : M ⟶ N
inst_7 : IsMonHom f
X : C
⊢ Eq (α := X ⟶ N) (1 ≫ f) 1

Tactic:
simp [Hom.one_def]

Premises used: CategoryTheory.Hom.one_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X_1 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f : M ⟶ N
inst_7 : IsMonHom f
X : C
⊢ ∀ (x y : X ⟶ M), (x * y) ≫ f = x ≫ f * y ≫ f

Tactic:
simp [Hom.mul_def]

Premises used: CategoryTheory.Hom.mul_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X_1 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
change :
  Eq (α := unop Y₂ ⟶ M) (φ.unop ≫ CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop X)) η)
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
⊢ Eq (α := unop Y₂ ⟶ M) (φ.unop ≫ 1) 1

Tactic:
change φ.unop ≫ toUnit _ ≫ η = toUnit _ ≫ η

Premises used: Quiver.Hom.unop, CategoryTheory.SemiCartesianMonoidalCategory.toUnit
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X_1 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
rw :
  Eq (α := unop Y₂ ⟶ M) (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (φ.unop ≫ toUnit (unop X)) η)
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
rw₁ :
  Eq.{v + 1} (α := unop Y₂ ⟶ M) (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
rw₂ : unop Y₂ ⟶ tensorUnit.{v, u_1} C (𝒞 := inst)
rw₃ :
  Eq.{v + 1} (α := unop Y₂ ⟶ M) (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)
rw₄ : unop Y₂ ⟶ tensorUnit.{v, u_1} C (𝒞 := inst)
⊢ Eq (α := unop Y₂ ⟶ M) (φ.unop ≫ CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop X)) η)
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (unop Y₂)) η)

Tactic:
rw [← Category.assoc, toUnit_unique (φ.unop ≫ toUnit _)]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique, Quiver.Hom.unop, CategoryTheory.CategoryStruct.comp, CategoryTheory.SemiCartesianMonoidalCategory.toUnit
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X_1 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
f₁ f₂ : unop X ⟶ M
change :
  φ.unop ≫ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift (φ.unop ≫ f₁) (φ.unop ≫ f₂)) μ
⊢ φ.unop ≫ (f₁ * f₂) = φ.unop ≫ f₁ * φ.unop ≫ f₂

Tactic:
change φ.unop ≫ lift f₁ f₂ ≫ μ = lift (φ.unop ≫ f₁) (φ.unop ≫ f₂) ≫ μ

Premises used: Quiver.Hom.unop, CategoryTheory.CartesianMonoidalCategory.lift, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X_1 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
f₁ f₂ : unop X ⟶ M
rw :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (φ.unop ≫ lift f₁ f₂) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift (φ.unop ≫ f₁) (φ.unop ≫ f₂)) μ
⊢ φ.unop ≫ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift (φ.unop ≫ f₁) (φ.unop ≫ f₂)) μ

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y_1 : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
F : Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat
α :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          MonCat.carrier)).RepresentableBy
    X
this : MonObj X := ofRepresentableBy X F α
Y : Cᵒᵖ
f₁ f₂ : unop Y ⟶ X
⊢ HMul.hMul (α := (↑(F.obj (op (unop Y))) : Type v)) (β := (↑(F.obj (op (unop Y))) : Type v))
      ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) :
            (a : unop Y ⟶ X) → ToType (F.obj (op (unop Y))))
          (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) X X) (lift f₁ f₂) (fst X X)) :
        ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
          (F.obj (op (unop Y))))
      ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) :
            (a : unop Y ⟶ X) → ToType (F.obj (op (unop Y))))
          (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) X X) (lift f₁ f₂) (snd X X)) :
        ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
          (F.obj (op (unop Y)))) =
    HMul.hMul (α :=
      ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
        (F.obj (op (unop Y))))
      (β :=
      ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
        (F.obj (op (unop Y))))
      ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) :
            (a : unop Y ⟶ X) → ToType (F.obj (op (unop Y))))
          f₁ :
        ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
          (F.obj (op (unop Y))))
      ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) :
            (a : unop Y ⟶ X) → ToType (F.obj (op (unop Y))))
          f₂ :
        ToType (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
          (F.obj (op (unop Y))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M N X Y : C
inst_2 : MonObj M
inst_3 : MonObj N
α : Quiver.Hom (V := Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat) (yonedaMonObj M) (yonedaMonObj N)
f : X ⟶ Y
g : Y ⟶ M
⊢ Eq (α := (↑(Functor.obj (yonedaMonObj N) (op X)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
            (X := Functor.obj (yonedaMonObj M) (op X)) (α.app (op X)) :
          (a : (↑((yonedaMonObj M).obj (op X)) : Type v)) → (↑((yonedaMonObj N).obj (op X)) : Type v))
        (f ≫ g) :
      (↑(Functor.obj (yonedaMonObj N) (op X)) : Type v))
    (f ≫
        (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
              (X := Functor.obj (yonedaMonObj M) (op Y)) (α.app (op Y)) :
            (a : (↑((yonedaMonObj M).obj (op Y)) : Type v)) → (↑((yonedaMonObj N).obj (op Y)) : Type v))
          g :
      X ⟶ N)

Tactic:
congr($(α.naturality f.op) g)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, id, CategoryTheory.NatTrans.naturality, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M : C
inst_2 : MonObj M
H : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) M M ⟶ M) μ μ
⊢ ofRepresentableBy M (yonedaMonObj M) (yonedaMonObjRepresentableBy M) = inst_2

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M : C
inst_2 : MonObj M
H :
  Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) M M ⟶ M)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift (fst M M) (snd M M)) μ) μ
⊢ Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) M M ⟶ M) μ μ

Tactic:
change lift (fst M M) (snd M M) ≫ μ = μ

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.snd, CategoryTheory.CartesianMonoidalCategory.lift, CategoryTheory.SemiCartesianMonoidalCategory.fst
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M : C
inst_2 : MonObj M
H : 𝟙 (tensorObj.{v, u_1} (𝒞 := inst) M M) ≫ μ = μ
H₁ H₂ : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) M M ⟶ M) μ μ
⊢ Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) M M ⟶ M)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift (fst M M) (snd M M)) μ) μ

Tactic:
rw [lift_fst_snd, Category.id_comp]

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_fst_snd, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
M N : Mon.{v, u_1} C
α : Functor.obj yonedaMon M ⟶ Functor.obj yonedaMon N
dsimp :
  Eq (α := tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)
    (CategoryStruct.comp (Y := M.X) η
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
              MonCat.carrier) (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
            (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
          (𝟙 M.X)) :
      tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)
    (η : tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)
⊢ Eq (α := tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)
    (CategoryStruct.comp (Y := M.X) η
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
              MonCat.carrier) (X := (Functor.obj yonedaMon M).obj (op M.X)) (α.app (op M.X)) :
            (a : (↑((yonedaMon.obj M).obj (op M.X)) : Type v)) → (↑((yonedaMon.obj N).obj (op M.X)) : Type v))
          (𝟙 M.X)) :
      tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)
    (η : tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)

Tactic:
dsimp only [yonedaMon_obj] at α ⊢

Premises used: CategoryTheory.yonedaMon_obj
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
M N : Mon.{v, u_1} C
α : Quiver.Hom (V := Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat) (yonedaMonObj M.X) (yonedaMonObj N.X)
rw :
  Eq (α := tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
            (X := Functor.obj (yonedaMonObj M.X) (op (tensorUnit.{v, u_1} C (𝒞 := inst))))
            (α.app (op (tensorUnit.{v, u_1} C (𝒞 := inst)))) :
          (a : (↑((yonedaMonObj M.X).obj (op (𝟙_ C))) : Type v)) → (↑((yonedaMonObj N.X).obj (op (𝟙_ C))) : Type v))
        (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (tensorUnit.{v, u_1} C (𝒞 := inst))) η) :
      (↑(Functor.obj (yonedaMonObj N.X) (op (tensorUnit.{v, u_1} C (𝒞 := inst)))) : Type v))
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (tensorUnit.{v, u_1} C (𝒞 := inst))) η :
      tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)
⊢ Eq (α := tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)
    (CategoryStruct.comp (Y := M.X) η
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
              MonCat.carrier) (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
            (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
          (𝟙 M.X)) :
      tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)
    (η : tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)

Tactic:
rw [← yonedaMon_naturality, Category.comp_id,
            ← Category.id_comp η[M.X], toUnit_unique (𝟙 _) (toUnit _),
            ← Category.id_comp η[N.X], toUnit_unique (𝟙 _) (toUnit _)]

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique, CategoryTheory.yonedaMon_naturality, CategoryTheory.CategoryStruct.id, CategoryTheory.Category.comp_id, CategoryTheory.MonObj.one, CategoryTheory.SemiCartesianMonoidalCategory.toUnit, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
M N : Mon.{v, u_1} C
α : Quiver.Hom (V := Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat) (yonedaMonObj M.X) (yonedaMonObj N.X)
⊢ Eq (α := tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
            (X := Functor.obj (yonedaMonObj M.X) (op (tensorUnit.{v, u_1} C (𝒞 := inst))))
            (α.app (op (tensorUnit.{v, u_1} C (𝒞 := inst)))) :
          (a : (↑((yonedaMonObj M.X).obj (op (𝟙_ C))) : Type v)) → (↑((yonedaMonObj N.X).obj (op (𝟙_ C))) : Type v))
        (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (tensorUnit.{v, u_1} C (𝒞 := inst))) η) :
      (↑(Functor.obj (yonedaMonObj N.X) (op (tensorUnit.{v, u_1} C (𝒞 := inst)))) : Type v))
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (tensorUnit.{v, u_1} C (𝒞 := inst))) η :
      tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)

Tactic:
(α.app _).hom.map_one

Premises used: MonCat.Hom.hom, MonoidHom.map_one, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
M N : Mon.{v, u_1} C
α : Quiver.Hom (V := Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat) (yonedaMonObj M.X) (yonedaMonObj N.X)
⊢ Eq (α := tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
            (X := Functor.obj (yonedaMonObj M.X) (op (tensorUnit.{v, u_1} C (𝒞 := inst))))
            (α.app (op (tensorUnit.{v, u_1} C (𝒞 := inst)))) :
          (a : (↑((yonedaMonObj M.X).obj (op (𝟙_ C))) : Type v)) → (↑((yonedaMonObj N.X).obj (op (𝟙_ C))) : Type v))
        (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (tensorUnit.{v, u_1} C (𝒞 := inst))) η) :
      (↑(Functor.obj (yonedaMonObj N.X) (op (tensorUnit.{v, u_1} C (𝒞 := inst)))) : Type v))
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (tensorUnit.{v, u_1} C (𝒞 := inst))) η :
      tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ N.X)

Tactic:
exact (α.app _).hom.map_one

Premises used: MonCat.Hom.hom, MonoidHom.map_one, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
M N : Mon.{v, u_1} C
α : Functor.obj yonedaMon M ⟶ Functor.obj yonedaMon N
dsimp :
  Eq (α := tensorObj.{v, u_1} (𝒞 := inst) M.X M.X ⟶ N.X)
    (μ ≫
        (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
              (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
            (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
          (𝟙 M.X) :
      tensorObj.{v, u_1} (𝒞 := inst) M.X M.X ⟶ N.X)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) N.X N.X)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                MonCat.carrier) (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
              (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
            (𝟙 M.X) ⊗ₘ
          (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                MonCat.carrier) (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
              (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
            (𝟙 M.X))
        μ :
      tensorObj.{v, u_1} (𝒞 := inst) M.X M.X ⟶ N.X)
⊢ Eq (α := tensorObj.{v, u_1} (𝒞 := inst) M.X M.X ⟶ N.X)
    (μ ≫
        (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
              (X := (Functor.obj yonedaMon M).obj (op M.X)) (α.app (op M.X)) :
            (a : (↑((yonedaMon.obj M).obj (op M.X)) : Type v)) → (↑((yonedaMon.obj N).obj (op M.X)) : Type v))
          (𝟙 M.X) :
      tensorObj.{v, u_1} (𝒞 := inst) M.X M.X ⟶ N.X)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) N.X N.X)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                MonCat.carrier) (X := (Functor.obj yonedaMon M).obj (op M.X)) (α.app (op M.X)) :
              (a : (↑((yonedaMon.obj M).obj (op M.X)) : Type v)) → (↑((yonedaMon.obj N).obj (op M.X)) : Type v))
            (𝟙 M.X) ⊗ₘ
          (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                MonCat.carrier) (X := (Functor.obj yonedaMon M).obj (op M.X)) (α.app (op M.X)) :
              (a : (↑((yonedaMon.obj M).obj (op M.X)) : Type v)) → (↑((yonedaMon.obj N).obj (op M.X)) : Type v))
            (𝟙 M.X))
        μ :
      tensorObj.{v, u_1} (𝒞 := inst) M.X M.X ⟶ N.X)

Tactic:
dsimp only [yonedaMon_obj] at α ⊢

Premises used: CategoryTheory.yonedaMon_obj
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
M N : Mon.{v, u_1} C
α : Quiver.Hom (V := Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat) (yonedaMonObj M.X) (yonedaMonObj N.X)
⊢ Eq (α := tensorObj.{v, u_1} (𝒞 := inst) M.X M.X ⟶ N.X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
            (X := Functor.obj (yonedaMonObj M.X) (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)))
            (α.app (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) :
          (a : (↑((yonedaMonObj M.X).obj (op (M.X ⊗ M.X))) : Type v)) →
            (↑((yonedaMonObj N.X).obj (op (M.X ⊗ M.X))) : Type v))
        (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M.X M.X) (lift (fst M.X M.X) (snd M.X M.X)) μ) :
      (↑(Functor.obj (yonedaMonObj N.X) (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) : Type v))
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) N.X N.X)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                MonCat.carrier) (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
              (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
            (𝟙 M.X) ⊗ₘ
          (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                MonCat.carrier) (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
              (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
            (𝟙 M.X))
        μ :
      tensorObj.{v, u_1} (𝒞 := inst) M.X M.X ⟶ N.X)

Tactic:
((α.app _).hom.map_mul _ _).trans ?_

Premises used: MonCat.Hom.hom, MonoidHom.map_mul, CategoryTheory.NatTrans.app, Eq.trans