awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxMonoidal
inst_10 : F'.LaxMonoidal
inst_11 : G.LaxMonoidal
X Y : C
inst_12 : MonObj X
inst_13 : MonObj Y
f : X ⟶ Y
inst_14 : IsMonHom f
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) ⟶ F.obj X)
    (F.obj X ◁ CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (F.map η) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) («μ» F X X) (F.map μ))
    (Iso.hom (ρ_ (F.obj X)))

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxMonoidal
inst_10 : F'.LaxMonoidal
inst_11 : G.LaxMonoidal
X Y : C
inst_12 : MonObj X
inst_13 : MonObj Y
f : X ⟶ Y
inst_14 : IsMonHom f
simp_rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (F.obj X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.obj X))
      («μ» F X X ▷ F.obj X)
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X))
        («μ» F (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X) (F.map (μ ▷ X) ≫ F.map μ)))
    (Iso.hom (α_ (F.obj X) (F.obj X) (F.obj X)) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
        (F.obj X ◁ «μ» F X X)
        (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
          («μ» F X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.map (X ◁ μ) ≫ F.map μ)))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (F.obj X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) («μ» F X X) (F.map μ) ▷ F.obj X ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) («μ» F X X) (F.map μ))
    (Iso.hom (α_ (F.obj X) (F.obj X) (F.obj X)) ≫
      F.obj X ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) («μ» F X X) (F.map μ) ≫
        CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) («μ» F X X) (F.map μ))

Tactic:
simp_rw [comp_whiskerRight, Category.assoc, μ_natural_left_assoc,
      MonoidalCategory.whiskerLeft_comp, Category.assoc, μ_natural_right_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.Functor.LaxMonoidal.μ_natural_right_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxMonoidal
inst_10 : F'.LaxMonoidal
inst_11 : G.LaxMonoidal
X Y : C
inst_12 : MonObj X
inst_13 : MonObj Y
f : X ⟶ Y
inst_14 : IsMonHom f
a : F.map (Iso.hom (α_ X X X) ≫ X ◁ μ ≫ μ)
| F.map (μ ▷ X) ≫ F.map μ

Tactic:
rw [← F.map_comp, MonObj.mul_assoc]

Premises used: CategoryTheory.MonObj.mul_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxMonoidal
inst_10 : F'.LaxMonoidal
inst_11 : G.LaxMonoidal
X Y : C
inst_12 : MonObj X
inst_13 : MonObj Y
f : X ⟶ Y
inst_14 : IsMonHom f
slice_lhs :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (F.obj X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.obj X))
      («μ» F X X ▷ F.obj X) («μ» F (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X ≫ F.map (Iso.hom (α_ X X X) ≫ X ◁ μ ≫ μ)))
    (Iso.hom (α_ (F.obj X) (F.obj X) (F.obj X)) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
        (F.obj X ◁ «μ» F X X)
        (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
          («μ» F X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.map (X ◁ μ) ≫ F.map μ)))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (F.obj X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.obj X))
      («μ» F X X ▷ F.obj X)
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X))
        («μ» F (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X) (F.map (μ ▷ X) ≫ F.map μ)))
    (Iso.hom (α_ (F.obj X) (F.obj X) (F.obj X)) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
        (F.obj X ◁ «μ» F X X)
        (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
          («μ» F X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.map (X ◁ μ) ≫ F.map μ)))

Tactic:
slice_lhs 3 4 => rw [← F.map_comp, MonObj.mul_assoc]

Premises used: CategoryTheory.MonObj.mul_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxMonoidal
inst_10 : F'.LaxMonoidal
inst_11 : G.LaxMonoidal
X Y : C
inst_12 : MonObj X
inst_13 : MonObj Y
f : X ⟶ Y
inst_14 : IsMonHom f
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (F.obj X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.obj X))
      («μ» F X X ▷ F.obj X) («μ» F (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X ≫ F.map (Iso.hom (α_ X X X) ≫ X ◁ μ ≫ μ)))
    (Iso.hom (α_ (F.obj X) (F.obj X) (F.obj X)) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
        (F.obj X ◁ «μ» F X X)
        (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)))
          («μ» F X (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.map (X ◁ μ) ≫ F.map μ)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.LaxMonoidal
X : C
inst_5 : MonObj X
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj X) η
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (F.map η))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.LaxMonoidal
X : C
inst_5 : MonObj X
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj X) ⟶ F.obj X) μ
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) («μ» F X X) (F.map μ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxMonoidal
inst_10 : F'.LaxMonoidal
inst_11 : G.LaxMonoidal
X Y : C
inst_12 : MonObj X
inst_13 : MonObj Y
f : X ⟶ Y
inst_14 : IsMonHom f
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_5) ⟶ F.obj Y) (η ≫ F.map f) η

Tactic:
simp [← map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxMonoidal
inst_10 : F'.LaxMonoidal
inst_11 : G.LaxMonoidal
X Y : C
inst_12 : MonObj X
inst_13 : MonObj Y
f : X ⟶ Y
inst_14 : IsMonHom f
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X) ⟶ F.obj Y) (μ ≫ F.map f) ((F.map f ⊗ₘ F.map f) ≫ μ)

Tactic:
simp [← map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Mon.{v₁, u₁} C
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ Mon.X (obj (mapMon (𝟭 C)) X)) η
    (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ η)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Mon.{v₁, u₁} C
⊢ μ = 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X.X X.X) ≫ μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.LaxMonoidal
inst_7 : G.LaxMonoidal
X : Mon.{v₁, u₁} C
⊢ Eq (α := tensorUnit.{v₃, u₃} E (𝒞 := inst_4) ⟶ Mon.X (obj (F ⋙ G).mapMon X)) η
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F ⋙ G)) ((F ⋙ G).map η))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.LaxMonoidal
inst_7 : G.LaxMonoidal
X : Mon.{v₁, u₁} C
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (Mon.X (obj (F ⋙ G).mapMon X)) (Mon.X (obj (F ⋙ G).mapMon X)) ⟶
      Mon.X (obj (F ⋙ G).mapMon X))
    μ
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X.X X.X)) («μ» (F ⋙ G) X.X X.X)
      ((F ⋙ G).map μ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.OplaxMonoidal
hF : F.FullyFaithful
X : C
inst_10 : MonObj (F.obj X)
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶ F.obj X)
    (F.map
      (hF.preimage (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) («η» F) η) ▷ X ≫
        hF.preimage (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (δ F X X) μ)))
    (F.map (Iso.hom (λ_ X)))

Tactic:
simp [← δ_natural_left_assoc]

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ_natural_left_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.OplaxMonoidal
hF : F.FullyFaithful
X : C
inst_10 : MonObj (F.obj X)
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶ F.obj X)
    (F.map
      (X ◁ hF.preimage (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) («η» F) η) ≫
        hF.preimage (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (δ F X X) μ)))
    (F.map (Iso.hom (ρ_ X)))

Tactic:
simp [← δ_natural_right_assoc]

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ_natural_right_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.OplaxMonoidal
hF : F.FullyFaithful
X : C
inst_10 : MonObj (F.obj X)
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X) ⟶ F.obj X)
    (F.map
      (hF.preimage (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (δ F X X) μ) ▷ X ≫
        hF.preimage (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (δ F X X) μ)))
    (F.map
      (Iso.hom (α_ X X X) ≫
        X ◁ hF.preimage (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (δ F X X) μ) ≫
          hF.preimage (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj X) (F.obj X)) (δ F X X) μ)))

Tactic:
simp [← δ_natural_left_assoc, ← δ_natural_right_assoc]

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ_natural_left_assoc, CategoryTheory.Functor.OplaxMonoidal.δ_natural_right_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.Monoidal
inst_10 : F.Full
inst_11 : F.Faithful
X Y : Mon.{v₁, u₁} C
f : Quiver.Hom (V := Mon.{v₂, u₂} D) (obj F.mapMon X) (obj F.mapMon Y)
g : X.X ⟶ Y.X
hg : F.map g = f.hom
⊢ Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ F.obj Y.X) (F.map (η ≫ g)) (F.map η)

Tactic:
simpa [← hg, cancel_epi] using IsMonHom.one_hom f.hom

Premises used: CategoryTheory.Mon.Hom.hom, CategoryTheory.IsMonHom.one_hom, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.Monoidal
inst_10 : F.Full
inst_11 : F.Faithful
X Y : Mon.{v₁, u₁} C
f : Quiver.Hom (V := Mon.{v₂, u₂} D) (obj F.mapMon X) (obj F.mapMon Y)
g : X.X ⟶ Y.X
hg : F.map g = f.hom
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X.X X.X) ⟶ F.obj Y.X) (F.map (μ ≫ g)) (F.map ((g ⊗ₘ g) ≫ μ))

Tactic:
simpa [← hg, cancel_epi] using IsMonHom.mul_hom f.hom

Premises used: CategoryTheory.Mon.Hom.hom, CategoryTheory.IsMonHom.mul_hom, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.Monoidal
hF : F.FullyFaithful
X Y : C
inst_10 : AddMonObj X
inst_11 : AddMonObj Y
f : F.obj X ⟶ F.obj Y
inst_12 : IsAddMonHom f
⊢ Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ F.obj Y) (F.map (AddMonObj.zero ≫ hF.preimage f))
    (F.map AddMonObj.zero)

Tactic:
simp [← cancel_epi (ε F), ← obj.ζ_def_assoc, ← obj.ζ_def]

Premises used: CategoryTheory.Functor.LaxMonoidal.ε, CategoryTheory.Functor.obj.ζ_def_assoc, CategoryTheory.cancel_epi, CategoryTheory.Functor.obj.ζ_def
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.Monoidal
hF : F.FullyFaithful
X Y : C
inst_10 : AddMonObj X
inst_11 : AddMonObj Y
f : F.obj X ⟶ F.obj Y
inst_12 : IsAddMonHom f
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X) ⟶ F.obj Y) (F.map (AddMonObj.add ≫ hF.preimage f))
    (F.map ((hF.preimage f ⊗ₘ hF.preimage f) ≫ AddMonObj.add))

Tactic:
simp [← obj.σ_def_assoc, ← obj.σ_def, ← μ_natural_assoc, ← cancel_epi (LaxMonoidal.μ F ..)]

Premises used: CategoryTheory.Functor.obj.σ_def, CategoryTheory.Functor.obj.σ_def_assoc, CategoryTheory.Functor.LaxMonoidal.μ, CategoryTheory.Functor.LaxMonoidal.μ_natural_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.Monoidal
hF : F.FullyFaithful
X Y : C
inst_10 : MonObj X
inst_11 : MonObj Y
f : F.obj X ⟶ F.obj Y
inst_12 : IsMonHom f
⊢ Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ F.obj Y) (F.map (η ≫ hF.preimage f)) (F.map η)

Tactic:
simp [← obj.η_def_assoc, ← obj.η_def, ← cancel_epi (ε F)]

Premises used: CategoryTheory.Functor.LaxMonoidal.ε, CategoryTheory.Functor.obj.η_def_assoc, CategoryTheory.Functor.obj.η_def, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.Monoidal
hF : F.FullyFaithful
X Y : C
inst_10 : MonObj X
inst_11 : MonObj Y
f : F.obj X ⟶ F.obj Y
inst_12 : IsMonHom f
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X) ⟶ F.obj Y) (F.map (μ ≫ hF.preimage f))
    (F.map ((hF.preimage f ⊗ₘ hF.preimage f) ≫ μ))

Tactic:
simp [← obj.μ_def_assoc, ← obj.μ_def, ← μ_natural_assoc, ← cancel_epi (LaxMonoidal.μ F ..)]

Premises used: CategoryTheory.Functor.obj.μ_def, CategoryTheory.Functor.LaxMonoidal.μ, CategoryTheory.Functor.obj.μ_def_assoc, CategoryTheory.Functor.LaxMonoidal.μ_natural_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
M : Mon.{v₂, u₂} D
N : Mon.{v₁, u₁} C
e : obj F.mapMon N ≅ M
⊢ F.essImage M.X

Tactic:
⟨N.X, ⟨(Mon.forget _).mapIso e⟩⟩

Premises used: CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Mon.forget, CategoryTheory.Mon.X, Exists.intro, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
M : Mon.{v₂, u₂} D
N : Mon.{v₁, u₁} C
e : obj F.mapMon N ≅ M
⊢ F.essImage M.X

Tactic:
exact ⟨N.X, ⟨(Mon.forget _).mapIso e⟩⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
M : Mon.{v₂, u₂} D
N : C
e : F.obj N ≅ M.X
this_1 : MonObj (F.obj N) := MonObj.ofIso e.symm
this : MonObj N := (FullyFaithful.ofFullyFaithful F).monObj N
⊢ essImage (C := Mon.{v₁, u₁} C) F.mapMon M

Tactic:
⟨.mk N, ⟨Mon.mkIso e ?_ ?_⟩⟩

Premises used: CategoryTheory.Mon.mkIso, CategoryTheory.Functor.essImage, Nonempty.intro, Exists.intro, CategoryTheory.Mon.mk
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
M : Mon.{v₂, u₂} D
N : C
e : F.obj N ≅ M.X
this_1 : MonObj (F.obj N) := MonObj.ofIso e.symm
this : MonObj N := (FullyFaithful.ofFullyFaithful F).monObj N
refine_1 : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ M.X) (η ≫ e.hom) η
refine_2 :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2)
        (Mon.X (obj (C := Mon.{v₁, u₁} C) F.mapMon { X := N, mon := this : Mon.{v₁, u₁} C }))
        (Mon.X (obj (C := Mon.{v₁, u₁} C) F.mapMon { X := N, mon := this : Mon.{v₁, u₁} C })) ⟶
      M.X)
    (μ ≫ e.hom) ((e.hom ⊗ₘ e.hom) ≫ μ)
⊢ essImage (C := Mon.{v₁, u₁} C) F.mapMon M

Tactic:
refine ⟨.mk N, ⟨Mon.mkIso e ?_ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
M : Mon.{v₂, u₂} D
N : C
e : F.obj N ≅ M.X
this_1 : MonObj (F.obj N) := MonObj.ofIso e.symm
this : MonObj N := (FullyFaithful.ofFullyFaithful F).monObj N
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ M.X) (η ≫ e.hom) η

Tactic:
simp