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
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
ε : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μ : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)) =
      Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
left_unitality :
  ∀ (X : C),
    Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
right_unitality :
  ∀ (X : C),
    Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
X Y : C
f : X ⟶ Y
X' : C
simp_rw : (F.map f ⊗ₘ 𝟙 (F.obj X')) ≫ μ Y X' = μ X X' ≫ F.map (f ⊗ₘ 𝟙 X')
simp_rw₁ : (F.map f ⊗ₘ F.map (𝟙 X')) ≫ μ Y X' = μ X X' ≫ F.map (f ⊗ₘ 𝟙 X')
⊢ F.map f ▷ F.obj X' ≫ μ Y X' = μ X X' ≫ F.map (f ▷ X')

Tactic:
simp_rw [← tensorHom_id, ← F.map_id, μ_natural]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.MonoidalCategory.tensorHom_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
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
ε : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μ : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)) =
      Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
left_unitality :
  ∀ (X : C),
    Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
right_unitality :
  ∀ (X : C),
    Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
X Y X' : C
f : X ⟶ Y
simp_rw : (𝟙 (F.obj X') ⊗ₘ F.map f) ≫ μ X' Y = μ X' X ≫ F.map (𝟙 X' ⊗ₘ f)
simp_rw₁ : (F.map (𝟙 X') ⊗ₘ F.map f) ≫ μ X' Y = μ X' X ≫ F.map (𝟙 X' ⊗ₘ f)
⊢ F.obj X' ◁ F.map f ≫ μ X' Y = μ X' X ≫ F.map (X' ◁ f)

Tactic:
simp_rw [← id_tensorHom, ← F.map_id, μ_natural]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.Functor.map_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
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
ε : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μ : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)) =
      Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
left_unitality :
  ∀ (X : C),
    Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
right_unitality :
  ∀ (X : C),
    Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
X Y Z : C
simp_rw :
  (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)) =
    Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ Y Z ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
simp_rw₁ :
  (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)) =
    Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
⊢ μ X Y ▷ F.obj Z ≫ μ (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)) =
    Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ Y Z ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)

Tactic:
simp_rw [← tensorHom_id, ← id_tensorHom, associativity]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.tensorHom_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
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
ε : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μ : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)) =
      Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
left_unitality :
  ∀ (X : C),
    Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
right_unitality :
  ∀ (X : C),
    Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
X : C
simp_rw : Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
⊢ Iso.hom (λ_ (F.obj X)) = ε ▷ F.obj X ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))

Tactic:
simp_rw [← tensorHom_id, left_unitality]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_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
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
ε : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μ : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)) =
      Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
left_unitality :
  ∀ (X : C),
    Iso.hom (λ_ (F.obj X)) = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))
right_unitality :
  ∀ (X : C),
    Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
X : C
simp_rw : Iso.hom (ρ_ (F.obj X)) = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))
⊢ Iso.hom (ρ_ (F.obj X)) = F.obj X ◁ ε ≫ μ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))

Tactic:
simp_rw [← id_tensorHom, right_unitality]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom
-- 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.LaxMonoidal
inst_8 : G.LaxMonoidal
x x_1 x_2 : C
dsimp :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
        (G.obj (F.obj x_2)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
          (μ G (F.obj x) (F.obj x_1)) (G.map (μ F x x_1)) ▷
        G.obj (F.obj x_2) ≫
      CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2)))
          (μ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2))
          (G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2)) ≫
        G.map (F.map (Iso.hom (α_ x x_1 x_2))))
    (Iso.hom (α_ (G.obj (F.obj x)) (G.obj (F.obj x_1)) (G.obj (F.obj x_2))) ≫
      G.obj (F.obj x) ◁
          CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
            (μ G (F.obj x_1) (F.obj x_2)) (G.map (μ F x_1 x_2)) ≫
        CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
          (μ G (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
          (G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj x) ((F ⋙ G).obj x_1))
        ((F ⋙ G).obj x_2) ⟶
      (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
          (μ G (F.obj x) (F.obj x_1)) (G.map (μ F x x_1)) ▷
        (F ⋙ G).obj x_2 ≫
      CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2)))
          (μ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2))
          (G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2)) ≫
        (F ⋙ G).map (Iso.hom (α_ x x_1 x_2)))
    (Iso.hom (α_ ((F ⋙ G).obj x) ((F ⋙ G).obj x_1) ((F ⋙ G).obj x_2)) ≫
      (F ⋙ G).obj x ◁
          CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
            (μ G (F.obj x_1) (F.obj x_2)) (G.map (μ F x_1 x_2)) ≫
        CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
          (μ G (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
          (G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))

Tactic:
dsimp
-- 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.OplaxMonoidal
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X') ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Y'))
    (δ F X X' ≫ (F.map f ⊗ₘ F.map g)) (F.map (f ⊗ₘ g) ≫ δ F Y Y')

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- 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.OplaxMonoidal
X : C
Y : D
f : F.obj X ⟶ Y
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) Y)
    (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ (η F ⊗ₘ f))
    (F.map (Iso.hom (λ_ X)) ≫ Iso.inv (λ_ (F.obj X)) ≫ tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ◁ f)

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- 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.OplaxMonoidal
X : C
Y : D
f : F.obj X ⟶ Y
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) Y (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ (f ⊗ₘ η F))
    (F.map (Iso.hom (ρ_ X)) ≫ Iso.inv (ρ_ (F.obj X)) ≫ f ▷ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))

Tactic:
simp [tensorHom_def']

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def'
-- 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.OplaxMonoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
      δ F X Y ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)))
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
      δ F X Y ▷ F.obj Z ≫
        𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z)))
rw₂ rw₃ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj 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)))

Tactic:
rw [← associativity_assoc, Iso.hom_inv_id, Category.comp_id]

Premises used: CategoryTheory.Functor.OplaxMonoidal.associativity_assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_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
inst_4 : F.OplaxMonoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y Z)) ≫
      F.map (Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y Z) ≫ Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₂ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
      δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₃ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
      δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₄ rw₅ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y Z)) ≫
      δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)))

Tactic:
rw [associativity, ← F.map_comp_assoc, Iso.inv_hom_id, Functor.map_id, Category.id_comp]

Premises used: CategoryTheory.Functor.OplaxMonoidal.associativity, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- 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.OplaxMonoidal
inst_8 : G.OplaxMonoidal
X Y : C
f : X ⟶ Y
X' : C
dsimp :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X')) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj X')))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj X'))) (G.map (δ F X X'))
        (δ G (F.obj X) (F.obj X')) ≫
      G.map (F.map f) ▷ G.obj (F.obj X'))
    (G.map (F.map (f ▷ X')) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X'))) (G.map (δ F Y X'))
        (δ G (F.obj Y) (F.obj X')))
⊢ Eq (α :=
    (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X') ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj Y) ((F ⋙ G).obj X'))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj X'))) (G.map (δ F X X'))
        (δ G (F.obj X) (F.obj X')) ≫
      (F ⋙ G).map f ▷ (F ⋙ G).obj X')
    ((F ⋙ G).map (f ▷ X') ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X'))) (G.map (δ F Y X'))
        (δ G (F.obj Y) (F.obj X')))

Tactic:
dsimp
-- 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.OplaxMonoidal
inst_8 : G.OplaxMonoidal
X Y x : C
x_1 : X ⟶ Y
dsimp :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
        (δ G (F.obj x) (F.obj X)) ≫
      G.obj (F.obj x) ◁ G.map (F.map x_1))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
⊢ Eq (α :=
    (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X) ⟶ tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj x) ((F ⋙ G).obj Y))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
        (δ G (F.obj x) (F.obj X)) ≫
      (F ⋙ G).obj x ◁ (F ⋙ G).map x_1)
    ((F ⋙ G).map (x ◁ x_1) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))

Tactic:
dsimp