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 : F C
f_2 g_1 : X_1 ⟶ᵐ Y_1
h : HomEquiv f_2 g_1
hfg' :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 g_1)
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 g_1)
    (projectMapAux f_1 f_2)

Tactic:
exact hfg'.symm

Premises used: Eq.symm
-- 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 g_1 h : X_1 ⟶ᵐ Y_1
h_1 : HomEquiv f_2 g_1
h_2 : HomEquiv g_1 h
hfg :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 g_1)
hgh :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 g_1)
    (projectMapAux f_1 h)
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 h)

Tactic:
hfg.trans hgh

Premises used: Eq.trans
-- 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 g_1 h : X_1 ⟶ᵐ Y_1
h_1 : HomEquiv f_2 g_1
h_2 : HomEquiv g_1 h
hfg :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 g_1)
hgh :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 g_1)
    (projectMapAux f_1 h)
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 h)

Tactic:
exact hfg.trans hgh

Premises used: Eq.trans
-- 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
f_2 f' : X_1 ⟶ᵐ Y_1
g_1 g' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
h_1 : HomEquiv g_1 g'
hf :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
hg :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g_1)
    (projectMapAux f_1 g')
comp :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Z)
    (projectMapAux f_1 f_2 ≫ projectMapAux f_1 g_1) (projectMapAux f_1 f' ≫ projectMapAux f_1 g')
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 (f_2.comp g_1))
    (projectMapAux f_1 (f'.comp g'))

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
f_2 f' : X_1 ⟶ᵐ Y_1
g_1 g' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
h_1 : HomEquiv g_1 g'
hf :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
hg :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g_1)
    (projectMapAux f_1 g')
comp :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Z)
    (projectMapAux f_1 f' ≫ projectMapAux f_1 g_1) (projectMapAux f_1 f' ≫ projectMapAux f_1 g')
comp₁ comp₂ :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Z)
    (projectMapAux f_1 f' ≫ projectMapAux f_1 g') (projectMapAux f_1 f' ≫ projectMapAux f_1 g')
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Z)
    (projectMapAux f_1 f_2 ≫ projectMapAux f_1 g_1) (projectMapAux f_1 f' ≫ projectMapAux f_1 g')

Tactic:
rw [hf, hg]
-- 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
f_2 f' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
hf :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
whiskerLeft :
  Eq.{v' + 1} (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (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 Z))
    (projectObj.{v', u, u'} f_1 X_1 ◁ projectMapAux f_1 f_2) (projectObj.{v', u, u'} f_1 X_1 ◁ projectMapAux f_1 f')
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X_1.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
    (projectMapAux f_1 (Hom.whiskerLeft X_1 f_2)) (projectMapAux f_1 (Hom.whiskerLeft X_1 f'))

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 Z : F C
f_2 f' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
hf :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
whiskerLeft whiskerLeft₁ :
  Eq.{v' + 1} (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (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 Z))
    (projectObj.{v', u, u'} f_1 X_1 ◁ projectMapAux f_1 f') (projectObj.{v', u, u'} f_1 X_1 ◁ projectMapAux f_1 f')
⊢ Eq.{v' + 1} (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (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 Z))
    (projectObj.{v', u, u'} f_1 X_1 ◁ projectMapAux f_1 f_2) (projectObj.{v', u, u'} f_1 X_1 ◁ projectMapAux f_1 f')

Tactic:
rw [hf]
-- 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
Y_1 Z : F C
f_2 f' : Y_1 ⟶ᵐ Z
X_1 : F C
h : HomEquiv f_2 f'
hf :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
whiskerRight :
  Eq.{v' + 1} (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 X_1) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Z) (projectObj.{v', u, u'} f_1 X_1))
    (projectMapAux f_1 f_2 ▷ projectObj.{v', u, u'} f_1 X_1) (projectMapAux f_1 f' ▷ projectObj.{v', u, u'} f_1 X_1)
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (Y_1.tensor X_1) ⟶ projectObj.{v', u, u'} f_1 (Z.tensor X_1))
    (projectMapAux f_1 (f_2.whiskerRight X_1)) (projectMapAux f_1 (f'.whiskerRight X_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
Y_1 Z : F C
f_2 f' : Y_1 ⟶ᵐ Z
X_1 : F C
h : HomEquiv f_2 f'
hf :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
whiskerRight whiskerRight₁ :
  Eq.{v' + 1} (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 X_1) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Z) (projectObj.{v', u, u'} f_1 X_1))
    (projectMapAux f_1 f' ▷ projectObj.{v', u, u'} f_1 X_1) (projectMapAux f_1 f' ▷ projectObj.{v', u, u'} f_1 X_1)
⊢ Eq.{v' + 1} (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 X_1) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Z) (projectObj.{v', u, u'} f_1 X_1))
    (projectMapAux f_1 f_2 ▷ projectObj.{v', u, u'} f_1 X_1) (projectMapAux f_1 f' ▷ projectObj.{v', u, u'} f_1 X_1)

Tactic:
rw [hf]
-- 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
f_2 f' : W ⟶ᵐ X_1
g_1 g' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
h_1 : HomEquiv g_1 g'
hfg :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 W ⟶ projectObj.{v', u, u'} f_1 X_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
hfg' :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g_1)
    (projectMapAux f_1 g')
tensor :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
    (projectMapAux f_1 f_2 ⊗ₘ projectMapAux f_1 g_1) (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g')
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
    (projectMapAux f_1 (f_2.tensor g_1)) (projectMapAux f_1 (f'.tensor g'))

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
W X_1 Y_1 Z : F C
f_2 f' : W ⟶ᵐ X_1
g_1 g' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
h_1 : HomEquiv g_1 g'
hfg :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 W ⟶ projectObj.{v', u, u'} f_1 X_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
hfg' :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g_1)
    (projectMapAux f_1 g')
tensor :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
    (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g_1) (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g')
tensor₁ tensor₂ :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
    (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g') (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g')
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
    (projectMapAux f_1 f_2 ⊗ₘ projectMapAux f_1 g_1) (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g')

Tactic:
rw [hfg, hfg']
-- 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₁ Y₁ X₂ Y₂ : F C
f_2 : X₁ ⟶ᵐ Y₁
g_1 : X₂ ⟶ᵐ Y₂
tensorHom_def :
  Eq (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X₁) (projectObj.{v', u, u'} f_1 X₂) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y₁) (projectObj.{v', u, u'} f_1 Y₂))
    (projectMapAux f_1 f_2 ⊗ₘ projectMapAux f_1 g_1)
    (projectMapAux f_1 f_2 ▷ projectObj.{v', u, u'} f_1 X₂ ≫ projectObj.{v', u, u'} f_1 Y₁ ◁ projectMapAux f_1 g_1)
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X₁.tensor X₂) ⟶ projectObj.{v', u, u'} f_1 (Y₁.tensor Y₂))
    (projectMapAux f_1 (f_2.tensor g_1)) (projectMapAux f_1 ((f_2.whiskerRight X₂).comp (Hom.whiskerLeft Y₁ g_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₁ Y₁ X₂ Y₂ : F C
f_2 : X₁ ⟶ᵐ Y₁
g_1 : X₂ ⟶ᵐ Y₂
tensorHom_def tensorHom_def₁ :
  Eq (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X₁) (projectObj.{v', u, u'} f_1 X₂) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y₁) (projectObj.{v', u, u'} f_1 Y₂))
    (projectMapAux f_1 f_2 ▷ projectObj.{v', u, u'} f_1 X₂ ≫ projectObj.{v', u, u'} f_1 Y₁ ◁ projectMapAux f_1 g_1)
    (projectMapAux f_1 f_2 ▷ projectObj.{v', u, u'} f_1 X₂ ≫ projectObj.{v', u, u'} f_1 Y₁ ◁ projectMapAux f_1 g_1)
⊢ Eq (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X₁) (projectObj.{v', u, u'} f_1 X₂) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y₁) (projectObj.{v', u, u'} f_1 Y₂))
    (projectMapAux f_1 f_2 ⊗ₘ projectMapAux f_1 g_1)
    (projectMapAux f_1 f_2 ▷ projectObj.{v', u, u'} f_1 X₂ ≫ projectObj.{v', u, u'} f_1 Y₁ ◁ projectMapAux f_1 g_1)

Tactic:
rw [MonoidalCategory.tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- 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
comp_id : projectMapAux f_1 f_2 ≫ 𝟙 (projectObj.{v', u, u'} f_1 Y_1) = projectMapAux f_1 f_2
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1)
    (projectMapAux f_1 (f_2.comp (Hom.id Y_1))) (projectMapAux f_1 f_2)

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 : F C
f_2 : X_1 ⟶ᵐ Y_1
comp_id comp_id₁ :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f_2)
⊢ projectMapAux f_1 f_2 ≫ 𝟙 (projectObj.{v', u, u'} f_1 Y_1) = projectMapAux f_1 f_2

Tactic:
rw [Category.comp_id]

Premises used: CategoryTheory.Category.comp_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
id_comp : 𝟙 (projectObj.{v', u, u'} f_1 X_1) ≫ projectMapAux f_1 f_2 = projectMapAux f_1 f_2
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1)
    (projectMapAux f_1 ((Hom.id X_1).comp f_2)) (projectMapAux f_1 f_2)

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 : F C
f_2 : X_1 ⟶ᵐ Y_1
id_comp id_comp₁ :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f_2)
⊢ 𝟙 (projectObj.{v', u, u'} f_1 X_1) ≫ projectMapAux f_1 f_2 = projectMapAux f_1 f_2

Tactic:
rw [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- 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 U V : F C
f_2 : X_1 ⟶ᵐ U
g_1 : U ⟶ᵐ V
h : V ⟶ᵐ Y_1
assoc :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1)
    ((projectMapAux f_1 f_2 ≫ projectMapAux f_1 g_1) ≫ projectMapAux f_1 h)
    (projectMapAux f_1 f_2 ≫ projectMapAux f_1 g_1 ≫ projectMapAux f_1 h)
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1)
    (projectMapAux f_1 ((f_2.comp g_1).comp h)) (projectMapAux f_1 (f_2.comp (g_1.comp h)))

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 U V : F C
f_2 : X_1 ⟶ᵐ U
g_1 : U ⟶ᵐ V
h : V ⟶ᵐ Y_1
assoc assoc₁ :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1)
    (projectMapAux f_1 f_2 ≫ projectMapAux f_1 g_1 ≫ projectMapAux f_1 h)
    (projectMapAux f_1 f_2 ≫ projectMapAux f_1 g_1 ≫ projectMapAux f_1 h)
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1)
    ((projectMapAux f_1 f_2 ≫ projectMapAux f_1 g_1) ≫ projectMapAux f_1 h)
    (projectMapAux f_1 f_2 ≫ projectMapAux f_1 g_1 ≫ projectMapAux f_1 h)

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
id_tensorHom_id :
  𝟙 (projectObj.{v', u, u'} f_1 X_1) ⊗ₘ 𝟙 (projectObj.{v', u, u'} f_1 Y_1) =
    𝟙 (projectObj.{v', u, u'} f_1 (X_1.tensor Y_1))
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X_1.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Y_1))
    (projectMapAux f_1 ((Hom.id X_1).tensor (Hom.id Y_1))) (projectMapAux f_1 (Hom.id (X_1.tensor Y_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 Y_1 : F C
id_tensorHom_id :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X_1.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Y_1))
    (𝟙 (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 (X_1.tensor Y_1)))
⊢ 𝟙 (projectObj.{v', u, u'} f_1 X_1) ⊗ₘ 𝟙 (projectObj.{v', u, u'} f_1 Y_1) =
    𝟙 (projectObj.{v', u, u'} f_1 (X_1.tensor Y_1))

Tactic:
rw [MonoidalCategory.id_tensorHom_id]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom_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
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X_1.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Y_1))
    (𝟙 (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 (X_1.tensor Y_1)))

Tactic:
rfl
-- 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₁ Y₁ Z₁ X₂ Y₂ Z₂ : F C
f₁ : X₁ ⟶ᵐ Y₁
f₂ : X₂ ⟶ᵐ Y₂
g₁ : Y₁ ⟶ᵐ Z₁
g₂ : Y₂ ⟶ᵐ Z₂
tensorHom_comp_tensorHom :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X₁.tensor X₂) ⟶ projectObj.{v', u, u'} f_1 (Z₁.tensor Z₂))
    ((projectMapAux f_1 f₁ ⊗ₘ projectMapAux f_1 f₂) ≫ (projectMapAux f_1 g₁ ⊗ₘ projectMapAux f_1 g₂))
    (projectMapAux f_1 f₁ ≫ projectMapAux f_1 g₁ ⊗ₘ projectMapAux f_1 f₂ ≫ projectMapAux f_1 g₂)
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X₁.tensor X₂) ⟶ projectObj.{v', u, u'} f_1 (Z₁.tensor Z₂))
    (projectMapAux f_1 ((f₁.tensor f₂).comp (g₁.tensor g₂))) (projectMapAux f_1 ((f₁.comp g₁).tensor (f₂.comp g₂)))

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₁ Y₁ Z₁ X₂ Y₂ Z₂ : F C
f₁ : X₁ ⟶ᵐ Y₁
f₂ : X₂ ⟶ᵐ Y₂
g₁ : Y₁ ⟶ᵐ Z₁
g₂ : Y₂ ⟶ᵐ Z₂
tensorHom_comp_tensorHom tensorHom_comp_tensorHom₁ :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X₁.tensor X₂) ⟶ projectObj.{v', u, u'} f_1 (Z₁.tensor Z₂))
    (projectMapAux f_1 f₁ ≫ projectMapAux f_1 g₁ ⊗ₘ projectMapAux f_1 f₂ ≫ projectMapAux f_1 g₂)
    (projectMapAux f_1 f₁ ≫ projectMapAux f_1 g₁ ⊗ₘ projectMapAux f_1 f₂ ≫ projectMapAux f_1 g₂)
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X₁.tensor X₂) ⟶ projectObj.{v', u, u'} f_1 (Z₁.tensor Z₂))
    ((projectMapAux f_1 f₁ ⊗ₘ projectMapAux f_1 f₂) ≫ (projectMapAux f_1 g₁ ⊗ₘ projectMapAux f_1 g₂))
    (projectMapAux f_1 f₁ ≫ projectMapAux f_1 g₁ ⊗ₘ projectMapAux f_1 f₂ ≫ projectMapAux f_1 g₂)

Tactic:
rw [MonoidalCategory.tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom
-- 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
whiskerLeft_id :
  projectObj.{v', u, u'} f_1 X_1 ◁ 𝟙 (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))
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X_1.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Y_1))
    (projectMapAux f_1 (Hom.whiskerLeft X_1 (Hom.id Y_1))) (projectMapAux f_1 (Hom.id (X_1.tensor 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
whiskerLeft_id whiskerLeft_id₁ :
  Eq.{v' + 1} (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (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))
    (𝟙 (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (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)))
⊢ projectObj.{v', u, u'} f_1 X_1 ◁ 𝟙 (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))

Tactic:
rw [MonoidalCategory.whiskerLeft_id]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_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
id_whiskerRight :
  𝟙 (projectObj.{v', u, u'} f_1 X_1) ▷ 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))
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X_1.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Y_1))
    (projectMapAux f_1 ((Hom.id X_1).whiskerRight Y_1)) (projectMapAux f_1 (Hom.id (X_1.tensor 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
id_whiskerRight id_whiskerRight₁ :
  Eq.{v' + 1} (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (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))
    (𝟙 (tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (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)))
⊢ 𝟙 (projectObj.{v', u, u'} f_1 X_1) ▷ 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))

Tactic:
rw [MonoidalCategory.id_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.id_whiskerRight