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
F : Functor.{v, w, u_1, w + 1} Cᵒᵖ MonCat
α :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
          MonCat.carrier)).RepresentableBy
    X
⊢ HMul.hMul (α := (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst))))) : Type w)) (β :=
      (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst))))) : Type w))
      (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
              Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst)) ⟶ X)
                (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                  (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst))))))) :
            (a : X ⊗ 𝟙_ C ⟶ X) → ToType (F.obj (op (X ⊗ 𝟙_ C))))
          (fst X (tensorUnit.{v, u_1} C (𝒞 := inst))) :
        ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
          (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst))))))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
              (X := F.obj (op (tensorUnit.{v, u_1} C (𝒞 := inst)))) (Y :=
              F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst)))))
              (F.map (Quiver.Hom.op (snd X (tensorUnit.{v, u_1} C (𝒞 := inst))))) :
            (a : (↑(F.obj (op (𝟙_ C))) : Type w)) → (↑(F.obj (op (X ⊗ 𝟙_ C))) : Type w))
          1 :
        (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst))))) : Type w)) =
    ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
          Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst)) ⟶ X)
            (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
              (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorUnit.{v, u_1} C (𝒞 := inst))))))) :
        (a : X ⊗ 𝟙_ C ⟶ X) → ToType (F.obj (op (X ⊗ 𝟙_ C))))
      (Iso.hom (ρ_ X))

Tactic:
simp [rightUnitor_hom, -op_tensorObj, -op_whiskerRight, -op_tensorUnit]

Premises used: CategoryTheory.op_whiskerRight, CategoryTheory.op_tensorUnit, CategoryTheory.op_tensorObj, CategoryTheory.CartesianMonoidalCategory.rightUnitor_hom
-- 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
f₁ f₂ f₃ : X ⟶ M
change :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) f₃) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
⊢ f₁ * f₂ * f₃ = f₁ * (f₂ * f₃)

Tactic:
change lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, CategoryTheory.CategoryStruct.comp, CategoryTheory.MonObj.mul
-- 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
f₁ f₂ f₃ : X ⟶ M
trans :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) f₃) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (μ ▷ M ≫ μ)
trans₁ :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (μ ▷ M ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) f₃) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ

Tactic:
trans lift (lift f₁ f₂) f₃ ≫ μ ▷ M ≫ μ

Premises used: CategoryTheory.CartesianMonoidalCategory.lift
-- 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
f₁ f₂ f₃ : X ⟶ M
rw :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) f₃) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) ((μ ⊗ₘ 𝟙 M) ≫ μ)
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) f₃) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) (f₃ ≫ 𝟙 M)) μ
rw₂ rw₃ :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) f₃) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) f₃) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ) f₃) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (μ ▷ M ≫ μ)

Tactic:
rw [← tensorHom_id, lift_map_assoc, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.CartesianMonoidalCategory.lift_map_assoc, CategoryTheory.MonoidalCategory.tensorHom_id
-- 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
f₁ f₂ f₃ : X ⟶ M
trans :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (μ ▷ M ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ)
trans₁ :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (μ ▷ M ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ

Tactic:
trans lift f₁ (lift f₂ f₃) ≫ M ◁ μ ≫ μ

Premises used: CategoryTheory.CartesianMonoidalCategory.lift
-- 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
f₁ f₂ f₃ : X ⟶ M
rw :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (Iso.hom (α_ M M M) ≫ M ◁ μ ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ)
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (μ ▷ M ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ)

Tactic:
rw [MonObj.mul_assoc]

Premises used: CategoryTheory.MonObj.mul_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 : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
simp_rw :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) ((lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) ≫ M ◁ μ)
      μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
        (lift f₁ (lift f₂ f₃)) (M ◁ μ))
      μ
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) M M) M)
      (lift (lift f₁ f₂) f₃) (Iso.hom (α_ M M M) ≫ M ◁ μ ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ)

Tactic:
simp_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 : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f₁ f₂ f₃ : X ⟶ M
e_a :
  Eq (α := X ⟶ tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
    (lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) (lift f₁ (lift f₂ f₃))
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) ((lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) ≫ M ◁ μ)
      μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
        (lift f₁ (lift f₂ f₃)) (M ◁ μ))
      μ

Tactic:
congr 2
-- 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
f₁ f₂ f₃ : X ⟶ M
e_a :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) (fst M (tensorObj.{v, u_1} (𝒞 := inst) M M)) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (fst M (tensorObj.{v, u_1} (𝒞 := inst) M M))
e_a₁ :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      ((lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) ≫ snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)) (fst M M) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
        (lift f₁ (lift f₂ f₃)) (snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)))
      (fst M M)
e_a₂ :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      ((lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) ≫ snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)) (snd M M) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
        (lift f₁ (lift f₂ f₃)) (snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)))
      (snd M M)
⊢ Eq (α := X ⟶ tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
    (lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) (lift f₁ (lift f₂ f₃))

Tactic:
ext
-- 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
f₁ f₂ f₃ : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) (fst M (tensorObj.{v, u_1} (𝒞 := inst) M M)) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (fst M (tensorObj.{v, u_1} (𝒞 := inst) M M))

Tactic:
simp
-- 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
f₁ f₂ f₃ : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      ((lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) ≫ snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)) (fst M M) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
        (lift f₁ (lift f₂ f₃)) (snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)))
      (fst M M)

Tactic:
simp
-- 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
f₁ f₂ f₃ : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      ((lift (lift f₁ f₂) f₃ ≫ Iso.hom (α_ M M M)) ≫ snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)) (snd M M) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
        (lift f₁ (lift f₂ f₃)) (snd M (tensorObj.{v, u_1} (𝒞 := inst) M M)))
      (snd M M)

Tactic:
simp
-- 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
f₁ f₂ f₃ : X ⟶ M
rw :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) ((𝟙 M ⊗ₘ μ) ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (f₁ ≫ 𝟙 M) (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
rw₂ rw₃ :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorObj.{v, u_1} (𝒞 := inst) M M))
      (lift f₁ (lift f₂ f₃)) (M ◁ μ ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f₁ (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₂ f₃) μ)) μ

Tactic:
rw [← id_tensorHom, lift_map_assoc, Category.comp_id]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.CartesianMonoidalCategory.lift_map_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 : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f : X ⟶ M
change :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit X) η) f) μ =
    f
⊢ 1 * f = f

Tactic:
change lift (toUnit _ ≫ η) f ≫ μ = f

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, CategoryTheory.MonObj.one, 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 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f : X ⟶ M
rw :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) M) (lift (toUnit X) f)
      (snd (tensorUnit.{v, u_1} C (𝒞 := inst)) M) =
    f
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit X) η) f) μ =
    f

Tactic:
rw [← Category.comp_id f, ← lift_map_assoc, tensorHom_id, MonObj.one_mul,
      Category.comp_id, leftUnitor_hom]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.CartesianMonoidalCategory.lift_map_assoc, CategoryTheory.MonObj.one_mul, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.CartesianMonoidalCategory.leftUnitor_hom
-- 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
f : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) M) (lift (toUnit X) f)
      (snd (tensorUnit.{v, u_1} C (𝒞 := inst)) M) =
    f

Tactic:
lift_snd _ _

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_snd
-- 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
f : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) M) (lift (toUnit X) f)
      (snd (tensorUnit.{v, u_1} C (𝒞 := inst)) M) =
    f

Tactic:
exact lift_snd _ _

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_snd
-- 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
f : X ⟶ M
change :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit X) η)) μ =
    f
⊢ f * 1 = f

Tactic:
change lift f (toUnit _ ≫ η) ≫ μ = f

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, CategoryTheory.MonObj.one, 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 Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
f : X ⟶ M
rw :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorUnit.{v, u_1} C (𝒞 := inst))) (lift f (toUnit X))
      (fst M (tensorUnit.{v, u_1} C (𝒞 := inst))) =
    f
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M)
      (lift f (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit X) η)) μ =
    f

Tactic:
rw [← Category.comp_id f, ← lift_map_assoc, id_tensorHom, MonObj.mul_one,
      Category.comp_id, rightUnitor_hom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.MonObj.mul_one, CategoryTheory.CartesianMonoidalCategory.lift_map_assoc, CategoryTheory.CartesianMonoidalCategory.rightUnitor_hom
-- 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
f : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorUnit.{v, u_1} C (𝒞 := inst))) (lift f (toUnit X))
      (fst M (tensorUnit.{v, u_1} C (𝒞 := inst))) =
    f

Tactic:
lift_fst _ _

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_fst
-- 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
f : X ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M (tensorUnit.{v, u_1} C (𝒞 := inst))) (lift f (toUnit X))
      (fst M (tensorUnit.{v, u_1} C (𝒞 := inst))) =
    f

Tactic:
exact lift_fst _ _

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_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 X : C
inst_2 : MonObj M
⊢ Eq.{v + 1} (α := X ⟶ M) 1 (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit X) η)

Tactic:
rfl

Premises used: 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
M X : C
inst_2 : MonObj M
f₁ f₂ : X ⟶ M
⊢ f₁ * f₂ = CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift f₁ f₂) μ

Tactic:
rfl

Premises used: rfl
-- 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 X : C
inst_4 : MonObj M
F : Functor.{v, w, u_1, u_2} C D
inst_5 : F.Monoidal
f g : X ⟶ M
⊢ F.map (f * g) = F.map f * F.map g

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 X : C
inst_4 : MonObj M
F : Functor.{v, w, u_1, u_2} C D
inst_5 : F.Monoidal
⊢ Eq (α := F.obj X ⟶ F.obj M) (F.map 1) 1

Tactic:
simp [Hom.one_def]

Premises used: CategoryTheory.Hom.one_def