awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (μ F X Y ▷ F.obj Z)
      (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
        F.map (Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
X Y Z : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
        (μ F X Y ▷ F.obj Z)
        (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
          F.map (Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z) ≫
      Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z)) (μ F X Y ▷ F.obj Z)
        (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
          F.map (Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) (F.obj X ◁ μ F Y Z)
        (μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
          F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
    (Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
      (F.obj X ◁ μ F Y Z)
      (μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
        F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z))

Tactic:
rw [← cancel_epi (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom, map_associator']

Premises used: CategoryTheory.Functor.Monoidal.map_associator', CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
        (μ F X Y ▷ F.obj Z)
        (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
          F.map (Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z) ≫
      Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z)) (μ F X Y ▷ F.obj Z)
        (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
          F.map (Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) (F.obj X ◁ μ F Y Z)
        (μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
          F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
X : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶ F.obj X)
    (F.map (Iso.hom (λ_ X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (η F ▷ F.obj X ≫ Iso.hom (λ_ (F.obj X))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
X : C
⊢ Eq (α := F.obj X ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (F.map (Iso.inv (λ_ X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
      (Iso.inv (λ_ (F.obj X))) (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
X : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶ F.obj X)
    (F.map (Iso.hom (ρ_ X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X ◁ η F ≫ Iso.hom (ρ_ (F.obj X))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
X : C
⊢ Eq (α := F.obj X ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (F.map (Iso.inv (ρ_ X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (Iso.inv (ρ_ (F.obj X))) (F.obj X ◁ ε F ≫ μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
rw :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F))
    (Iso.hom (εIso F))
rw₁ :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F)) (Iso.inv (εIso F)) =
    𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
rw₂ :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F)) (η F) =
    𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
rw₃ rw₄ :
  Eq.{v₂ + 1} (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F))
    (ε F)

Tactic:
rw [← εIso_hom, ← Iso.comp_inv_eq_id, εIso_inv, IsIso.inv_hom_id]

Premises used: CategoryTheory.Functor.Monoidal.εIso_hom, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.Iso.comp_inv_eq_id, CategoryTheory.Functor.Monoidal.εIso_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
⊢ Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (CategoryTheory.inv (ε F))
    (η F)

Tactic:
simp [← inv_η]

Premises used: CategoryTheory.Functor.Monoidal.inv_η
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
X Y : C
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (CategoryTheory.inv (CategoryTheory.inv (μ F X Y))) (CategoryTheory.inv (Iso.inv (μIso F X Y)))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (CategoryTheory.inv (μ F X Y)) (δ F X Y)

Tactic:
rw [← Monoidal.μIso_inv, ← CategoryTheory.IsIso.inv_eq_inv]

Premises used: CategoryTheory.Functor.Monoidal.μIso_inv, CategoryTheory.IsIso.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (CategoryTheory.inv (CategoryTheory.inv (μ F X Y))) (CategoryTheory.inv (Iso.inv (μIso F X Y)))

Tactic:
simp only [IsIso.inv_inv, IsIso.Iso.inv_inv, μIso_hom]

Premises used: CategoryTheory.IsIso.inv_inv, CategoryTheory.Functor.Monoidal.μIso_hom, CategoryTheory.IsIso.Iso.inv_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (CategoryTheory.inv (δ F X Y)) (μ F X Y)

Tactic:
simp [← inv_μ]

Premises used: CategoryTheory.Functor.Monoidal.inv_μ
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
⊢ CategoryStruct.comp (Y := (F ⋙ G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F ⋙ G)) (η (F ⋙ G)) =
    𝟙 (tensorUnit.{v₃, u₃} E (𝒞 := inst_4))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
⊢ CategoryStruct.comp (Y := tensorUnit.{v₃, u₃} E (𝒞 := inst_4)) (η (F ⋙ G)) (ε (F ⋙ G)) =
    𝟙 ((F ⋙ G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
x x_1 : C
⊢ CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ (F ⋙ G) x x_1) (δ (F ⋙ G) x x_1) =
    𝟙 (tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj x) ((F ⋙ G).obj x_1))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
x x_1 : C
⊢ CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj x) ((F ⋙ G).obj x_1)) (δ (F ⋙ G) x x_1)
      (μ (F ⋙ G) x x_1) =
    𝟙 ((F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
ε :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F)
    (LaxMonoidal.ε F)
μ :
  Eq (α :=
    (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F) (LaxMonoidal.μ F)
η :
  Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (OplaxMonoidal.η F)
    (OplaxMonoidal.η F)
δ :
  Eq (α :=
    (X Y : C) → F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (OplaxMonoidal.δ F) (OplaxMonoidal.δ F)
⊢ a = b

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (ε F)

Tactic:
congr(($eq).ε)

Premises used: congrArg, CategoryTheory.Functor.LaxMonoidal.ε, id
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (ε F)

Tactic:
exact congr(($eq).ε)
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
⊢ Eq (α :=
    (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F)
    (μ F)

Tactic:
congr(($eq).μ)

Premises used: congrArg, id, CategoryTheory.Functor.LaxMonoidal.μ
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
⊢ Eq (α :=
    (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F)
    (μ F)

Tactic:
exact congr(($eq).μ)
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
η :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (εIso F)) (OplaxMonoidal.η F))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (εIso F)) (OplaxMonoidal.η F))
⊢ Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (OplaxMonoidal.η F)
    (OplaxMonoidal.η F)

Tactic:
rw [← cancel_epi (εIso _).hom]

Premises used: CategoryTheory.Functor.Monoidal.εIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
η :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (εIso F)) (OplaxMonoidal.η F))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (OplaxMonoidal.η F))
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (εIso F)) (OplaxMonoidal.η F))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (εIso F)) (OplaxMonoidal.η F))

Tactic:
rw [εIso_hom, ε_η, ← @ε_η _ _ _ _ _ _ _ a, ← εIso_hom]

Premises used: CategoryTheory.Functor.Monoidal.εIso_hom, CategoryTheory.Functor.Monoidal.ε_η
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (εIso F)) (η F))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F))

Tactic:
congr(($eq.symm).ε ≫ _)

Premises used: congrArg, CategoryTheory.Functor.LaxMonoidal.ε, id, CategoryTheory.CategoryStruct.comp, Eq.symm, CategoryTheory.Functor.OplaxMonoidal.η
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (εIso F)) (η F))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F))

Tactic:
exact congr(($eq.symm).ε ≫ _)
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
δ :
  ∀ (x x_1 : C),
    Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
      (OplaxMonoidal.δ F x x_1) (OplaxMonoidal.δ F x x_1)
⊢ Eq (α :=
    (X Y : C) → F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (OplaxMonoidal.δ F) (OplaxMonoidal.δ F)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
x x_1 : C
δ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (Iso.hom (μIso F x x_1))
      (OplaxMonoidal.δ F x x_1))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (Iso.hom (μIso F x x_1))
      (OplaxMonoidal.δ F x x_1))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
    (OplaxMonoidal.δ F x x_1) (OplaxMonoidal.δ F x x_1)

Tactic:
rw [← cancel_epi (μIso F _ _).hom]

Premises used: CategoryTheory.Functor.Monoidal.μIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
x x_1 : C
δ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (Iso.hom (μIso F x x_1))
      (OplaxMonoidal.δ F x x_1))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ F x x_1) (OplaxMonoidal.δ F x x_1))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (Iso.hom (μIso F x x_1))
      (OplaxMonoidal.δ F x x_1))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (Iso.hom (μIso F x x_1))
      (OplaxMonoidal.δ F x x_1))

Tactic:
rw [μIso_hom, μ_δ, ← @μ_δ _ _ _ _ _ _ _ a, ← μIso_hom]

Premises used: CategoryTheory.Functor.Monoidal.μIso_hom, CategoryTheory.Functor.Monoidal.μ_δ
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
x x_1 : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (Iso.hom (μIso F x x_1)) (δ F x x_1))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ F x x_1) (δ F x x_1))

Tactic:
congr(($eq.symm).μ _ _ ≫ _)

Premises used: congrArg, CategoryTheory.Functor.OplaxMonoidal.δ, id, CategoryTheory.Functor.LaxMonoidal.μ, CategoryTheory.CategoryStruct.comp, Eq.symm