awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
⊢ ∀ (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X_1 ⟶
        inclusionObj
          ((tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory))
                X_1).normalizeObj
            n))
      (inclusionObj n ◁ Iso.inv (λ_ X_1) ≫
        Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X_1) n))
      ((normalizeIsoApp' C X_1 n).hom ≫ map inclusion (eqToHom ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
⊢ ∀ (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
          (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory))) ⟶
        inclusionObj (X_1.normalizeObj n))
      (inclusionObj n ◁ Iso.hom (ρ_ X_1) ≫ (normalizeIsoApp' C X_1 n).hom)
      (Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory))) n) ≫
        map inclusion (eqToHom ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
⊢ ∀ (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X_1 ⟶
        inclusionObj
          ((tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1
                ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory))).normalizeObj
            n))
      (inclusionObj n ◁ Iso.inv (ρ_ X_1) ≫
        Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory))) n))
      ((normalizeIsoApp' C X_1 n).hom ≫ map inclusion (eqToHom ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
w :
  ∀ (n : NormalMonoidalObject C),
    Eq (α :=
      ((tensorFunc C).obj X).obj { as := n : Discrete (NormalMonoidalObject C) } ⟶
        ((normalize' C).obj Y).obj { as := n })
      (((tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom).app { as := n })
      (((normalizeIsoAux C X).hom ≫ (normalize' C).map f).app { as := n })
⊢ (tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom = (normalizeIsoAux C X).hom ≫ (normalize' C).map f

Tactic:
ext ⟨n⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
n : NormalMonoidalObject C
⊢ inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)

Tactic:
normalize_naturality n f

Premises used: CategoryTheory.FreeMonoidalCategory.normalize_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
n : NormalMonoidalObject C
h :
  (((tensorFunc C).obj X).obj { as := n : Discrete (NormalMonoidalObject C) } ⟶
        ((normalize' C).obj Y).obj { as := n : Discrete (NormalMonoidalObject C) }) =
      (tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj n)) →
    ((tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom).app { as := n } =
      inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom
h₁ :
  (((tensorFunc C).obj X).obj { as := n : Discrete (NormalMonoidalObject C) } ⟶
        ((normalize' C).obj Y).obj { as := n : Discrete (NormalMonoidalObject C) }) =
      (tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj n)) →
    ((normalizeIsoAux C X).hom ≫ (normalize' C).map f).app { as := n } =
      (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)
⊢ Eq (α :=
    ((tensorFunc C).obj X).obj { as := n : Discrete (NormalMonoidalObject C) } ⟶ ((normalize' C).obj Y).obj { as := n })
    (((tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom).app { as := n })
    (((normalizeIsoAux C X).hom ≫ (normalize' C).map f).app { as := n })

Tactic:
convert! normalize_naturality n f using 1

Premises used: CategoryTheory.FreeMonoidalCategory.normalize_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
n : NormalMonoidalObject C
e_1 :
  (((tensorFunc C).obj X).obj { as := n : Discrete (NormalMonoidalObject C) } ⟶
      ((normalize' C).obj Y).obj { as := n : Discrete (NormalMonoidalObject C) }) =
    (tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj n))
h :
  inclusionObj n ◁ f ≫ Iso.hom (normalizeIsoApp C Y { as := n : Discrete (NormalMonoidalObject C) }) =
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom
⊢ ((tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom).app { as := n } = inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
n : NormalMonoidalObject C
e_1 :
  (((tensorFunc C).obj X).obj { as := n : Discrete (NormalMonoidalObject C) } ⟶
      ((normalize' C).obj Y).obj { as := n : Discrete (NormalMonoidalObject C) }) =
    (tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj n))
h h₁ :
  inclusionObj n ◁ f ≫ Iso.hom (normalizeIsoApp' C Y { as := n : Discrete (NormalMonoidalObject C) }.as) =
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom
⊢ inclusionObj n ◁ f ≫ Iso.hom (normalizeIsoApp C Y { as := n : Discrete (NormalMonoidalObject C) }) =
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom

Tactic:
rw [normalizeIsoApp_eq]

Premises used: CategoryTheory.FreeMonoidalCategory.normalizeIsoApp_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
n : NormalMonoidalObject C
e_1 :
  (((tensorFunc C).obj X).obj { as := n : Discrete (NormalMonoidalObject C) } ⟶
      ((normalize' C).obj Y).obj { as := n : Discrete (NormalMonoidalObject C) }) =
    (tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj n))
h :
  Eq (α :=
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶
      inclusionObj (Y.normalizeObj'.obj { as := n }).as)
    (Iso.hom (normalizeIsoApp C X { as := n : Discrete (NormalMonoidalObject C) }) ≫ eqToHom ⋯ :
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶
        inclusionObj (Y.normalizeObj'.obj { as := n }).as)
    ((normalizeIsoApp' C X n).hom ≫ eqToHom ⋯ :
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj n))
⊢ ((normalizeIsoAux C X).hom ≫ (normalize' C).map f).app { as := n } =
    (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
n : NormalMonoidalObject C
e_1 :
  (((tensorFunc C).obj X).obj { as := n : Discrete (NormalMonoidalObject C) } ⟶
      ((normalize' C).obj Y).obj { as := n : Discrete (NormalMonoidalObject C) }) =
    (tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj n))
h h₁ :
  Eq (α :=
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶
      inclusionObj (Y.normalizeObj'.obj { as := n }).as)
    (Iso.hom (normalizeIsoApp' C X { as := n : Discrete (NormalMonoidalObject C) }.as) ≫ eqToHom ⋯)
    ((normalizeIsoApp' C X n).hom ≫ eqToHom ⋯)
⊢ Eq (α :=
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶
      inclusionObj (Y.normalizeObj'.obj { as := n }).as)
    (Iso.hom (normalizeIsoApp C X { as := n : Discrete (NormalMonoidalObject C) }) ≫ eqToHom ⋯ :
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶
        inclusionObj (Y.normalizeObj'.obj { as := n }).as)
    ((normalizeIsoApp' C X n).hom ≫ eqToHom ⋯ :
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶ inclusionObj (Y.normalizeObj n))

Tactic:
rw [normalizeIsoApp_eq]

Premises used: CategoryTheory.FreeMonoidalCategory.normalizeIsoApp_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
dsimp :
  Eq (α := X ⟶ inclusionObj ((fullNormalize C).obj Y).as)
    (f ≫
        CategoryStruct.comp (Y :=
          tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) Y)
          (Iso.inv (λ_ Y)) (((normalizeIso C).hom.app Y).app { as := NormalMonoidalObject.unit }) :
      X ⟶ inclusionObj ((fullNormalize C).obj Y).as)
    (CategoryStruct.comp (Y := inclusionObj ((fullNormalize C).obj X).as)
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
          (Iso.inv (λ_ X)) (((normalizeIso C).hom.app X).app { as := NormalMonoidalObject.unit }))
        (eqToHom ⋯) :
      X ⟶ inclusionObj ((fullNormalize C).obj Y).as)
⊢ Eq (α := obj (𝟭 (F C)) X ⟶ (fullNormalize C ⋙ inclusion).obj Y)
    (map (𝟭 (F C)) f ≫
      Iso.hom
        ((fun (X : F C) ↦
            (Iso.trans (Y :=
                tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
                (Iso.symm (λ_ X)) (((normalizeIso C).app X).app { as := NormalMonoidalObject.unit }) :
              obj (𝟭 (F C)) X ≅ (fullNormalize C ⋙ inclusion).obj X))
          Y))
    (Iso.hom
        ((fun (X : F C) ↦
            (Iso.trans (Y :=
                tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
                (Iso.symm (λ_ X)) (((normalizeIso C).app X).app { as := NormalMonoidalObject.unit }) :
              obj (𝟭 (F C)) X ≅ (fullNormalize C ⋙ inclusion).obj X))
          X) ≫
      (fullNormalize C ⋙ inclusion).map f)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
rw :
  (𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory) ◁ f ≫
      ((normalizeIso C).hom.app Y).app { as := NormalMonoidalObject.unit } =
    CategoryStruct.comp (Y := inclusionObj ((fullNormalize C).obj X).as)
      (((normalizeIso C).hom.app X).app { as := NormalMonoidalObject.unit : Discrete (NormalMonoidalObject C) })
      (eqToHom ⋯)
⊢ Eq (α := X ⟶ inclusionObj ((fullNormalize C).obj Y).as)
    (f ≫
        CategoryStruct.comp (Y :=
          tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) Y)
          (Iso.inv (λ_ Y)) (((normalizeIso C).hom.app Y).app { as := NormalMonoidalObject.unit }) :
      X ⟶ inclusionObj ((fullNormalize C).obj Y).as)
    (CategoryStruct.comp (Y := inclusionObj ((fullNormalize C).obj X).as)
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
          (Iso.inv (λ_ X)) (((normalizeIso C).hom.app X).app { as := NormalMonoidalObject.unit }))
        (eqToHom ⋯) :
      X ⟶ inclusionObj ((fullNormalize C).obj Y).as)

Tactic:
rw [leftUnitor_inv_naturality_assoc, Category.assoc, Iso.cancel_iso_inv_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.cancel_iso_inv_left, CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
⊢ (𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory) ◁ f ≫
      ((normalizeIso C).hom.app Y).app { as := NormalMonoidalObject.unit } =
    CategoryStruct.comp (Y := inclusionObj ((fullNormalize C).obj X).as)
      (((normalizeIso C).hom.app X).app { as := NormalMonoidalObject.unit : Discrete (NormalMonoidalObject C) })
      (eqToHom ⋯)

Tactic:
congr_arg (fun f => NatTrans.app f (Discrete.mk NormalMonoidalObject.unit))
          ((normalizeIso.{u} C).hom.naturality f)

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.Discrete.mk, congr_arg, Quotient, CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.unit, CategoryTheory.NatTrans.naturality, CategoryTheory.FreeMonoidalCategory.normalizeIso, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, CategoryTheory.FreeMonoidalCategory.inclusionObj
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
⊢ (𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory) ◁ f ≫
      ((normalizeIso C).hom.app Y).app { as := NormalMonoidalObject.unit } =
    CategoryStruct.comp (Y := inclusionObj ((fullNormalize C).obj X).as)
      (((normalizeIso C).hom.app X).app { as := NormalMonoidalObject.unit : Discrete (NormalMonoidalObject C) })
      (eqToHom ⋯)

Tactic:
exact
        congr_arg (fun f => NatTrans.app f (Discrete.mk NormalMonoidalObject.unit))
          ((normalizeIso.{u} C).hom.naturality f)
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f g : X ⟶ Y
⊢ (fullNormalize C).map f = (fullNormalize C).map g

Tactic:
have hfg : (fullNormalize C).map f = (fullNormalize C).map g := Subsingleton.elim _ _
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f g : X ⟶ Y
hfg : (fullNormalize C).map f = (fullNormalize C).map g
⊢ (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map f ≫ (fullNormalizeIso C).inv.app Y =
    map (𝟭 (F C)) f

Tactic:
have hf := NatIso.naturality_2 (fullNormalizeIso.{u} C) f
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f g : X ⟶ Y
hfg : (fullNormalize C).map f = (fullNormalize C).map g
hf :
  (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map f ≫ (fullNormalizeIso C).inv.app Y =
    map (𝟭 (F C)) f
⊢ (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map g ≫ (fullNormalizeIso C).inv.app Y =
    map (𝟭 (F C)) g

Tactic:
have hg := NatIso.naturality_2 (fullNormalizeIso.{u} C) g
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f g : X ⟶ Y
hfg : (fullNormalize C).map f = (fullNormalize C).map g
hf :
  (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map f ≫ (fullNormalizeIso C).inv.app Y =
    map (𝟭 (F C)) f
hg :
  (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map g ≫ (fullNormalizeIso C).inv.app Y =
    map (𝟭 (F C)) g
⊢ (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map f ≫ (fullNormalizeIso C).inv.app Y =
    (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map g ≫ (fullNormalizeIso C).inv.app Y

Tactic:
simp only [Functor.comp_map, hfg]

Premises used: CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f g : X ⟶ Y
hfg : (fullNormalize C).map f = (fullNormalize C).map g
hf :
  (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map f ≫ (fullNormalizeIso C).inv.app Y =
    map (𝟭 (F C)) f
hg :
  (fullNormalizeIso C).hom.app X ≫ (fullNormalize C ⋙ inclusion).map g ≫ (fullNormalizeIso C).inv.app Y =
    map (𝟭 (F C)) g
⊢ f = g

Tactic:
exact hf.symm.trans (Eq.trans (by simp only [Functor.comp_map, hfg]) hg)

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

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

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

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.LaxMonoidal
X : C
Y : D
f : Y ⟶ F.obj X
⊢ tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ◁ f ≫ Iso.hom (λ_ (F.obj X)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (ε F ⊗ₘ f) (μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X)))

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.LaxMonoidal
X : C
Y : D
f : Y ⟶ F.obj X
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) Y (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶ F.obj X)
    (f ▷ tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ≫ Iso.hom (ρ_ (F.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (f ⊗ₘ ε F) (μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X))))

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.LaxMonoidal
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) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (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 ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)) ≫ F.map (Iso.inv (α_ X Y Z)))
rw₁ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (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 ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z) ≫ Iso.inv (α_ X Y Z)))
rw₂ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (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 ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
        F.map (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)))
rw₃ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (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 ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
        𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)))
rw₄ rw₅ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (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 ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
    (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
      F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.map (Iso.inv (α_ X Y Z)))

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

Premises used: CategoryTheory.Functor.LaxMonoidal.associativity_assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.LaxMonoidal
X Y Z : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
    (Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
      Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
rw₁ rw₂ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) 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 ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
    (Iso.inv (α_ (F.obj X) (F.obj 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)))

Tactic:
rw [associativity, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Functor.LaxMonoidal.associativity