awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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₂
⊢ 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)))
have 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)
Tactic: dsimp only [projectMapAux, projectObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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₂
⊢ 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)
have 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)
Tactic: rw [MonoidalCategory.tensorHom_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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)
have comp_id : projectMapAux f_1 f_2 ≫ 𝟙 (projectObj.{v', u, u'} f_1 Y_1) = projectMapAux f_1 f_2
Tactic: dsimp only [projectMapAux]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ projectMapAux f_1 f_2 ≫ 𝟙 (projectObj.{v', u, u'} f_1 Y_1) = projectMapAux f_1 f_2
have 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)
Tactic: rw [Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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)
have id_comp : 𝟙 (projectObj.{v', u, u'} f_1 X_1) ≫ projectMapAux f_1 f_2 = projectMapAux f_1 f_2
Tactic: dsimp only [projectMapAux]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 𝟙 (projectObj.{v', u, u'} f_1 X_1) ≫ projectMapAux f_1 f_2 = projectMapAux f_1 f_2
have 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)
Tactic: rw [Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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)))
have 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)
Tactic: dsimp only [projectMapAux]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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))
    (projectMapAux f_1 ((Hom.id X_1).tensor (Hom.id Y_1))) (projectMapAux f_1 (Hom.id (X_1.tensor Y_1)))
have 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))
Tactic: dsimp only [projectMapAux]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 𝟙 (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))
have 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)))
Tactic: rw [MonoidalCategory.id_tensorHom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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₂
⊢ 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₂)))
have 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₂)
Tactic: dsimp only [projectMapAux]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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₂
⊢ 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₂)
have 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₂)
Tactic: rw [MonoidalCategory.tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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))
    (projectMapAux f_1 (Hom.whiskerLeft X_1 (Hom.id Y_1))) (projectMapAux f_1 (Hom.id (X_1.tensor Y_1)))
have 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))
Tactic: dsimp only [projectMapAux, projectObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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))
have 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)))
Tactic: rw [MonoidalCategory.whiskerLeft_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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))
    (projectMapAux f_1 ((Hom.id X_1).whiskerRight Y_1)) (projectMapAux f_1 (Hom.id (X_1.tensor Y_1)))
have 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))
Tactic: dsimp only [projectMapAux, projectObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 𝟙 (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))
have 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)))
Tactic: rw [MonoidalCategory.id_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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)))
have α_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))
Tactic: dsimp only [projectMapAux]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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))
have α_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)))
Tactic: rw [Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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))))
have α_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)))
Tactic: dsimp only [projectMapAux]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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)))
have α_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))))
Tactic: rw [Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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₃
⊢ 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₃))))
have 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₃))
Tactic: dsimp only [projectMapAux]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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₃
⊢ 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₃))
have 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₃))
Tactic: rw [MonoidalCategory.associator_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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)))
have ρ_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))
Tactic: dsimp only [projectMapAux]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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))
have ρ_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)))
Tactic: rw [Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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))
have ρ_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))
Tactic: dsimp only [projectMapAux]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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))
have ρ_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))
Tactic: rw [Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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))
have ρ_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)
Tactic: dsimp only [projectMapAux, projectObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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)
have ρ_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)
Tactic: rw [MonoidalCategory.rightUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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)))
have 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))
Tactic: dsimp only [projectMapAux]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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))
have 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)))
Tactic: rw [Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ 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))
have 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))
Tactic: dsimp only [projectMapAux]