awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 Y_1 Z : F C
α_hom_inv :
  Iso.hom (α_ (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)) ≫
      Iso.inv (α_ (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)) =
    𝟙 (projectObj.{v', u, u'} f_1 ((X_1.tensor Y_1).tensor Z))
⊢ Eq.{v' + 1} (α :=
    projectObj.{v', u, u'} f_1 ((X_1.tensor Y_1).tensor Z) ⟶ projectObj.{v', u, u'} f_1 ((X_1.tensor Y_1).tensor Z))
    (projectMapAux f_1 ((α_hom X_1 Y_1 Z).comp (α_inv X_1 Y_1 Z)))
    (projectMapAux f_1 (Hom.id ((X_1.tensor Y_1).tensor Z)))

Tactic:
dsimp only [projectMapAux]

Premises used: CategoryTheory.FreeMonoidalCategory.projectMapAux
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 Y_1 Z : F C
α_hom_inv α_hom_inv₁ :
  Eq.{v' + 1} (α :=
    projectObj.{v', u, u'} f_1 ((X_1.tensor Y_1).tensor Z) ⟶ projectObj.{v', u, u'} f_1 ((X_1.tensor Y_1).tensor Z))
    (𝟙 (projectObj.{v', u, u'} f_1 ((X_1.tensor Y_1).tensor Z)))
    (𝟙 (projectObj.{v', u, u'} f_1 ((X_1.tensor Y_1).tensor Z)))
⊢ Iso.hom (α_ (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)) ≫
      Iso.inv (α_ (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)) =
    𝟙 (projectObj.{v', u, u'} f_1 ((X_1.tensor Y_1).tensor Z))

Tactic:
rw [Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 Y_1 Z : F C
α_inv_hom :
  Iso.inv (α_ (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)) ≫
      Iso.hom (α_ (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)) =
    𝟙 (projectObj.{v', u, u'} f_1 (X_1.tensor (Y_1.tensor Z)))
⊢ Eq.{v' + 1} (α :=
    projectObj.{v', u, u'} f_1 (X_1.tensor (Y_1.tensor Z)) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor (Y_1.tensor Z)))
    (projectMapAux f_1 ((α_inv X_1 Y_1 Z).comp (α_hom X_1 Y_1 Z)))
    (projectMapAux f_1 (Hom.id (X_1.tensor (Y_1.tensor Z))))

Tactic:
dsimp only [projectMapAux]

Premises used: CategoryTheory.FreeMonoidalCategory.projectMapAux
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 Y_1 Z : F C
α_inv_hom α_inv_hom₁ :
  Eq.{v' + 1} (α :=
    projectObj.{v', u, u'} f_1 (X_1.tensor (Y_1.tensor Z)) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor (Y_1.tensor Z)))
    (𝟙 (projectObj.{v', u, u'} f_1 (X_1.tensor (Y_1.tensor Z))))
    (𝟙 (projectObj.{v', u, u'} f_1 (X_1.tensor (Y_1.tensor Z))))
⊢ Iso.inv (α_ (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)) ≫
      Iso.hom (α_ (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)) =
    𝟙 (projectObj.{v', u, u'} f_1 (X_1.tensor (Y_1.tensor Z)))

Tactic:
rw [Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X₁ X₂ X₃ Y₁ Y₂ Y₃ : F C
f₁ : X₁ ⟶ᵐ Y₁
f₂ : X₂ ⟶ᵐ Y₂
f₃ : X₃ ⟶ᵐ Y₃
associator_naturality :
  Eq (α :=
    projectObj.{v', u, u'} f_1 ((X₁.tensor X₂).tensor X₃) ⟶ projectObj.{v', u, u'} f_1 (Y₁.tensor (Y₂.tensor Y₃)))
    (((projectMapAux f_1 f₁ ⊗ₘ projectMapAux f_1 f₂) ⊗ₘ projectMapAux f_1 f₃) ≫
      Iso.hom (α_ (projectObj.{v', u, u'} f_1 Y₁) (projectObj.{v', u, u'} f_1 Y₂) (projectObj.{v', u, u'} f_1 Y₃)))
    (Iso.hom (α_ (projectObj.{v', u, u'} f_1 X₁) (projectObj.{v', u, u'} f_1 X₂) (projectObj.{v', u, u'} f_1 X₃)) ≫
      (projectMapAux f_1 f₁ ⊗ₘ projectMapAux f_1 f₂ ⊗ₘ projectMapAux f_1 f₃))
⊢ Eq.{v' + 1} (α :=
    projectObj.{v', u, u'} f_1 ((X₁.tensor X₂).tensor X₃) ⟶ projectObj.{v', u, u'} f_1 (Y₁.tensor (Y₂.tensor Y₃)))
    (projectMapAux f_1 (((f₁.tensor f₂).tensor f₃).comp (α_hom Y₁ Y₂ Y₃)))
    (projectMapAux f_1 ((α_hom X₁ X₂ X₃).comp (f₁.tensor (f₂.tensor f₃))))

Tactic:
dsimp only [projectMapAux]

Premises used: CategoryTheory.FreeMonoidalCategory.projectMapAux
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X₁ X₂ X₃ Y₁ Y₂ Y₃ : F C
f₁ : X₁ ⟶ᵐ Y₁
f₂ : X₂ ⟶ᵐ Y₂
f₃ : X₃ ⟶ᵐ Y₃
associator_naturality associator_naturality₁ :
  Eq (α :=
    projectObj.{v', u, u'} f_1 ((X₁.tensor X₂).tensor X₃) ⟶ projectObj.{v', u, u'} f_1 (Y₁.tensor (Y₂.tensor Y₃)))
    (Iso.hom (α_ (projectObj.{v', u, u'} f_1 X₁) (projectObj.{v', u, u'} f_1 X₂) (projectObj.{v', u, u'} f_1 X₃)) ≫
      (projectMapAux f_1 f₁ ⊗ₘ projectMapAux f_1 f₂ ⊗ₘ projectMapAux f_1 f₃))
    (Iso.hom (α_ (projectObj.{v', u, u'} f_1 X₁) (projectObj.{v', u, u'} f_1 X₂) (projectObj.{v', u, u'} f_1 X₃)) ≫
      (projectMapAux f_1 f₁ ⊗ₘ projectMapAux f_1 f₂ ⊗ₘ projectMapAux f_1 f₃))
⊢ Eq (α :=
    projectObj.{v', u, u'} f_1 ((X₁.tensor X₂).tensor X₃) ⟶ projectObj.{v', u, u'} f_1 (Y₁.tensor (Y₂.tensor Y₃)))
    (((projectMapAux f_1 f₁ ⊗ₘ projectMapAux f_1 f₂) ⊗ₘ projectMapAux f_1 f₃) ≫
      Iso.hom (α_ (projectObj.{v', u, u'} f_1 Y₁) (projectObj.{v', u, u'} f_1 Y₂) (projectObj.{v', u, u'} f_1 Y₃)))
    (Iso.hom (α_ (projectObj.{v', u, u'} f_1 X₁) (projectObj.{v', u, u'} f_1 X₂) (projectObj.{v', u, u'} f_1 X₃)) ≫
      (projectMapAux f_1 f₁ ⊗ₘ projectMapAux f_1 f₂ ⊗ₘ projectMapAux f_1 f₃))

Tactic:
rw [MonoidalCategory.associator_naturality]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 : F C
ρ_hom_inv :
  Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 X_1)) ≫ Iso.inv (ρ_ (projectObj.{v', u, u'} f_1 X_1)) =
    𝟙 (projectObj.{v', u, u'} f_1 (X_1.tensor unit))
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X_1.tensor unit) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor unit))
    (projectMapAux f_1 ((ρ_hom X_1).comp (ρ_inv X_1))) (projectMapAux f_1 (Hom.id (X_1.tensor unit)))

Tactic:
dsimp only [projectMapAux]

Premises used: CategoryTheory.FreeMonoidalCategory.projectMapAux
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 : F C
ρ_hom_inv ρ_hom_inv₁ :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X_1.tensor unit) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor unit))
    (𝟙 (projectObj.{v', u, u'} f_1 (X_1.tensor unit))) (𝟙 (projectObj.{v', u, u'} f_1 (X_1.tensor unit)))
⊢ Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 X_1)) ≫ Iso.inv (ρ_ (projectObj.{v', u, u'} f_1 X_1)) =
    𝟙 (projectObj.{v', u, u'} f_1 (X_1.tensor unit))

Tactic:
rw [Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 : F C
ρ_inv_hom :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 X_1)
    (CategoryStruct.comp (Y := projectObj.{v', u, u'} f_1 (X_1.tensor unit))
      (Iso.inv (ρ_ (projectObj.{v', u, u'} f_1 X_1))) (Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 X_1))))
    (𝟙 (projectObj.{v', u, u'} f_1 X_1))
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 X_1)
    (projectMapAux f_1 ((ρ_inv X_1).comp (ρ_hom X_1))) (projectMapAux f_1 (Hom.id X_1))

Tactic:
dsimp only [projectMapAux]

Premises used: CategoryTheory.FreeMonoidalCategory.projectMapAux
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 : F C
ρ_inv_hom ρ_inv_hom₁ :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 X_1)
    (𝟙 (projectObj.{v', u, u'} f_1 X_1)) (𝟙 (projectObj.{v', u, u'} f_1 X_1))
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 X_1)
    (CategoryStruct.comp (Y := projectObj.{v', u, u'} f_1 (X_1.tensor unit))
      (Iso.inv (ρ_ (projectObj.{v', u, u'} f_1 X_1))) (Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 X_1))))
    (𝟙 (projectObj.{v', u, u'} f_1 X_1))

Tactic:
rw [Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 Y_1 : F C
f_2 : X_1 ⟶ᵐ Y_1
ρ_naturality :
  Eq (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (tensorUnit.{v', u'} D (𝒞 := inst)) ⟶
      projectObj.{v', u, u'} f_1 Y_1)
    (projectMapAux f_1 f_2 ▷ tensorUnit.{v', u'} D (𝒞 := inst) ≫ Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 Y_1)))
    (Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 X_1)) ≫ projectMapAux f_1 f_2)
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X_1.tensor unit) ⟶ projectObj.{v', u, u'} f_1 Y_1)
    (projectMapAux f_1 (Hom.comp (f_2.whiskerRight unit) (ρ_hom Y_1))) (projectMapAux f_1 ((ρ_hom X_1).comp f_2))

Tactic:
dsimp only [projectMapAux, projectObj]

Premises used: CategoryTheory.FreeMonoidalCategory.projectObj, CategoryTheory.FreeMonoidalCategory.projectMapAux
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 Y_1 : F C
f_2 : X_1 ⟶ᵐ Y_1
ρ_naturality ρ_naturality₁ :
  Eq (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (tensorUnit.{v', u'} D (𝒞 := inst)) ⟶
      projectObj.{v', u, u'} f_1 Y_1)
    (Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 X_1)) ≫ projectMapAux f_1 f_2)
    (Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 X_1)) ≫ projectMapAux f_1 f_2)
⊢ Eq (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (tensorUnit.{v', u'} D (𝒞 := inst)) ⟶
      projectObj.{v', u, u'} f_1 Y_1)
    (projectMapAux f_1 f_2 ▷ tensorUnit.{v', u'} D (𝒞 := inst) ≫ Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 Y_1)))
    (Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 X_1)) ≫ projectMapAux f_1 f_2)

Tactic:
rw [MonoidalCategory.rightUnitor_naturality]

Premises used: CategoryTheory.MonoidalCategory.rightUnitor_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 : F C
l_hom_inv :
  Iso.hom (λ_ (projectObj.{v', u, u'} f_1 X_1)) ≫ Iso.inv (λ_ (projectObj.{v', u, u'} f_1 X_1)) =
    𝟙 (projectObj.{v', u, u'} f_1 (tensor unit X_1))
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (tensor unit X_1) ⟶ projectObj.{v', u, u'} f_1 (tensor unit X_1))
    (projectMapAux f_1 ((l_hom X_1).comp (l_inv X_1))) (projectMapAux f_1 (Hom.id (tensor unit X_1)))

Tactic:
dsimp only [projectMapAux]

Premises used: CategoryTheory.FreeMonoidalCategory.projectMapAux
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 : F C
l_hom_inv l_hom_inv₁ :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (tensor unit X_1) ⟶ projectObj.{v', u, u'} f_1 (tensor unit X_1))
    (𝟙 (projectObj.{v', u, u'} f_1 (tensor unit X_1))) (𝟙 (projectObj.{v', u, u'} f_1 (tensor unit X_1)))
⊢ Iso.hom (λ_ (projectObj.{v', u, u'} f_1 X_1)) ≫ Iso.inv (λ_ (projectObj.{v', u, u'} f_1 X_1)) =
    𝟙 (projectObj.{v', u, u'} f_1 (tensor unit X_1))

Tactic:
rw [Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 : F C
l_inv_hom :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 X_1)
    (CategoryStruct.comp (Y := projectObj.{v', u, u'} f_1 (tensor unit X_1))
      (Iso.inv (λ_ (projectObj.{v', u, u'} f_1 X_1))) (Iso.hom (λ_ (projectObj.{v', u, u'} f_1 X_1))))
    (𝟙 (projectObj.{v', u, u'} f_1 X_1))
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 X_1)
    (projectMapAux f_1 ((l_inv X_1).comp (l_hom X_1))) (projectMapAux f_1 (Hom.id X_1))

Tactic:
dsimp only [projectMapAux]

Premises used: CategoryTheory.FreeMonoidalCategory.projectMapAux
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 : F C
l_inv_hom l_inv_hom₁ :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 X_1)
    (𝟙 (projectObj.{v', u, u'} f_1 X_1)) (𝟙 (projectObj.{v', u, u'} f_1 X_1))
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 X_1)
    (CategoryStruct.comp (Y := projectObj.{v', u, u'} f_1 (tensor unit X_1))
      (Iso.inv (λ_ (projectObj.{v', u, u'} f_1 X_1))) (Iso.hom (λ_ (projectObj.{v', u, u'} f_1 X_1))))
    (𝟙 (projectObj.{v', u, u'} f_1 X_1))

Tactic:
rw [Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 Y_1 : F C
f_2 : X_1 ⟶ᵐ Y_1
l_naturality :
  tensorUnit.{v', u'} D (𝒞 := inst) ◁ projectMapAux f_1 f_2 ≫ Iso.hom (λ_ (projectObj.{v', u, u'} f_1 Y_1)) =
    Iso.hom (λ_ (projectObj.{v', u, u'} f_1 X_1)) ≫ projectMapAux f_1 f_2
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (tensor unit X_1) ⟶ projectObj.{v', u, u'} f_1 Y_1)
    (projectMapAux f_1 (Hom.comp (Hom.whiskerLeft unit f_2) (l_hom Y_1))) (projectMapAux f_1 ((l_hom X_1).comp f_2))

Tactic:
dsimp only [projectMapAux, projectObj]

Premises used: CategoryTheory.FreeMonoidalCategory.projectObj, CategoryTheory.FreeMonoidalCategory.projectMapAux
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 Y_1 : F C
f_2 : X_1 ⟶ᵐ Y_1
l_naturality l_naturality₁ :
  Eq (α :=
    tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} D (𝒞 := inst)) (projectObj.{v', u, u'} f_1 X_1) ⟶
      projectObj.{v', u, u'} f_1 Y_1)
    (Iso.hom (λ_ (projectObj.{v', u, u'} f_1 X_1)) ≫ projectMapAux f_1 f_2)
    (Iso.hom (λ_ (projectObj.{v', u, u'} f_1 X_1)) ≫ projectMapAux f_1 f_2)
⊢ tensorUnit.{v', u'} D (𝒞 := inst) ◁ projectMapAux f_1 f_2 ≫ Iso.hom (λ_ (projectObj.{v', u, u'} f_1 Y_1)) =
    Iso.hom (λ_ (projectObj.{v', u, u'} f_1 X_1)) ≫ projectMapAux f_1 f_2

Tactic:
rw [MonoidalCategory.leftUnitor_naturality]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
W X_1 Y_1 Z : F C
pentagon :
  Eq (α :=
    tensorObj.{v', u'} (𝒞 := inst)
        (tensorObj.{v', u'} (𝒞 := inst)
          (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 W) (projectObj.{v', u, u'} f_1 X_1))
          (projectObj.{v', u, u'} f_1 Y_1))
        (projectObj.{v', u, u'} f_1 Z) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 W)
        (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1)
          (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z))))
    (Iso.hom (α_ (projectObj.{v', u, u'} f_1 W) (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1)) ▷
        projectObj.{v', u, u'} f_1 Z ≫
      Iso.hom
          (α_ (projectObj.{v', u, u'} f_1 W)
            (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1))
            (projectObj.{v', u, u'} f_1 Z)) ≫
        projectObj.{v', u, u'} f_1 W ◁
          Iso.hom (α_ (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)))
    (Iso.hom
        (α_ (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 W) (projectObj.{v', u, u'} f_1 X_1))
          (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)) ≫
      Iso.hom
        (α_ (projectObj.{v', u, u'} f_1 W) (projectObj.{v', u, u'} f_1 X_1)
          (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z))))
⊢ Eq.{v' + 1} (α :=
    projectObj.{v', u, u'} f_1 (((W.tensor X_1).tensor Y_1).tensor Z) ⟶
      projectObj.{v', u, u'} f_1 (W.tensor (X_1.tensor (Y_1.tensor Z))))
    (projectMapAux f_1
      (((α_hom W X_1 Y_1).whiskerRight Z).comp
        (Hom.comp (α_hom W (X_1.tensor Y_1) Z) (Hom.whiskerLeft W (α_hom X_1 Y_1 Z)))))
    (projectMapAux f_1 ((α_hom (W.tensor X_1) Y_1 Z).comp (α_hom W X_1 (Y_1.tensor Z))))

Tactic:
dsimp only [projectMapAux, projectObj]

Premises used: CategoryTheory.FreeMonoidalCategory.projectObj, CategoryTheory.FreeMonoidalCategory.projectMapAux
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
W X_1 Y_1 Z : F C
pentagon pentagon₁ :
  Eq (α :=
    tensorObj.{v', u'} (𝒞 := inst)
        (tensorObj.{v', u'} (𝒞 := inst)
          (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 W) (projectObj.{v', u, u'} f_1 X_1))
          (projectObj.{v', u, u'} f_1 Y_1))
        (projectObj.{v', u, u'} f_1 Z) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 W)
        (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1)
          (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z))))
    (Iso.hom
        (α_ (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 W) (projectObj.{v', u, u'} f_1 X_1))
          (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)) ≫
      Iso.hom
        (α_ (projectObj.{v', u, u'} f_1 W) (projectObj.{v', u, u'} f_1 X_1)
          (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z))))
    (Iso.hom
        (α_ (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 W) (projectObj.{v', u, u'} f_1 X_1))
          (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)) ≫
      Iso.hom
        (α_ (projectObj.{v', u, u'} f_1 W) (projectObj.{v', u, u'} f_1 X_1)
          (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z))))
⊢ Eq (α :=
    tensorObj.{v', u'} (𝒞 := inst)
        (tensorObj.{v', u'} (𝒞 := inst)
          (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 W) (projectObj.{v', u, u'} f_1 X_1))
          (projectObj.{v', u, u'} f_1 Y_1))
        (projectObj.{v', u, u'} f_1 Z) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 W)
        (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1)
          (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z))))
    (Iso.hom (α_ (projectObj.{v', u, u'} f_1 W) (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1)) ▷
        projectObj.{v', u, u'} f_1 Z ≫
      Iso.hom
          (α_ (projectObj.{v', u, u'} f_1 W)
            (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1))
            (projectObj.{v', u, u'} f_1 Z)) ≫
        projectObj.{v', u, u'} f_1 W ◁
          Iso.hom (α_ (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)))
    (Iso.hom
        (α_ (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 W) (projectObj.{v', u, u'} f_1 X_1))
          (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z)) ≫
      Iso.hom
        (α_ (projectObj.{v', u, u'} f_1 W) (projectObj.{v', u, u'} f_1 X_1)
          (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 Z))))

Tactic:
rw [MonoidalCategory.pentagon]

Premises used: CategoryTheory.MonoidalCategory.pentagon
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 Y_1 : F C
triangle :
  Eq.{v' + 1} (α :=
    tensorObj.{v', u'} (𝒞 := inst)
        (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (tensorUnit.{v', u'} D (𝒞 := inst)))
        (projectObj.{v', u, u'} f_1 Y_1) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1))
    (Iso.hom
        (α_ (projectObj.{v', u, u'} f_1 X_1) (tensorUnit.{v', u'} D (𝒞 := inst)) (projectObj.{v', u, u'} f_1 Y_1)) ≫
      projectObj.{v', u, u'} f_1 X_1 ◁ Iso.hom (λ_ (projectObj.{v', u, u'} f_1 Y_1)))
    (Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 X_1)) ▷ projectObj.{v', u, u'} f_1 Y_1)
⊢ Eq.{v' + 1} (α :=
    projectObj.{v', u, u'} f_1 ((X_1.tensor unit).tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Y_1))
    (projectMapAux f_1 (Hom.comp (α_hom X_1 unit Y_1) (Hom.whiskerLeft X_1 (l_hom Y_1))))
    (projectMapAux f_1 ((ρ_hom X_1).whiskerRight Y_1))

Tactic:
dsimp only [projectMapAux, projectObj]

Premises used: CategoryTheory.FreeMonoidalCategory.projectObj, CategoryTheory.FreeMonoidalCategory.projectMapAux
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 Y_1 : F C
triangle triangle₁ :
  Eq.{v' + 1} (α :=
    tensorObj.{v', u'} (𝒞 := inst)
        (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (tensorUnit.{v', u'} D (𝒞 := inst)))
        (projectObj.{v', u, u'} f_1 Y_1) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1))
    (Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 X_1)) ▷ projectObj.{v', u, u'} f_1 Y_1)
    (Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 X_1)) ▷ projectObj.{v', u, u'} f_1 Y_1)
⊢ Eq.{v' + 1} (α :=
    tensorObj.{v', u'} (𝒞 := inst)
        (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (tensorUnit.{v', u'} D (𝒞 := inst)))
        (projectObj.{v', u, u'} f_1 Y_1) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1))
    (Iso.hom
        (α_ (projectObj.{v', u, u'} f_1 X_1) (tensorUnit.{v', u'} D (𝒞 := inst)) (projectObj.{v', u, u'} f_1 Y_1)) ≫
      projectObj.{v', u, u'} f_1 X_1 ◁ Iso.hom (λ_ (projectObj.{v', u, u'} f_1 Y_1)))
    (Iso.hom (ρ_ (projectObj.{v', u, u'} f_1 X_1)) ▷ projectObj.{v', u, u'} f_1 Y_1)

Tactic:
rw [MonoidalCategory.triangle]

Premises used: CategoryTheory.MonoidalCategory.triangle
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f : C → D
X Y Z : F C
f_1 : X ⟶ Y
a : X ⟶ᵐ Y
g : Y ⟶ Z
a_1 : Y ⟶ᵐ Z
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f X ⟶ projectObj.{v', u, u'} f Z)
    (projectMap f X Z
      (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) a ≫
        Quot.mk (⇑(Y.setoidHom Z) : (Y ⟶ᵐ Z) → (Y ⟶ᵐ Z) → Prop) a_1))
    (projectMap f X Y (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) a) ≫
      projectMap f Y Z (Quot.mk (⇑(Y.setoidHom Z) : (Y ⟶ᵐ Z) → (Y ⟶ᵐ Z) → Prop) a_1))

Tactic:
rfl