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_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 (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))
have 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))
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 (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))
have 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
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
⊢ 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
have 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)
Tactic: rw [MonoidalCategory.leftUnitor_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
W X_1 Y_1 Z : F C
⊢ 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))))
have 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))))
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
W X_1 Y_1 Z : F C
⊢ 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))))
have 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))))
Tactic: rw [MonoidalCategory.pentagon]
-- 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 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))
have 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)
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
⊢ 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)
have 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)
Tactic: rw [MonoidalCategory.triangle]
-- 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
h : f ≈ g
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 f)
    (projectMapAux f_1 g)
have refl : ∀ {X Y : F C} (f : X ⟶ᵐ Y),
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 f)
    (projectMapAux f_1 f)
Tactic: induction h with
    | refl => rfl
    | symm _ _ _ hfg' => exact hfg'.symm
    | trans _ _ hfg hgh => exact hfg.trans hgh
    | comp _ _ hf hg => dsimp only [projectMapAux]; rw [hf, hg]
    | whiskerLeft _ _ _ _ hf => dsimp only [projectMapAux, projectObj]; rw [hf]
    | whiskerRight _ _ _ _ hf => dsimp only [projectMapAux, projectObj]; rw [hf]
    | tensor _ _ hfg hfg' => dsimp only [projectMapAux]; rw [hfg, hfg']
    | tensorHom_def _ _ =>
        dsimp only [projectMapAux, projectObj]; rw [MonoidalCategory.tensorHom_def]
    | comp_id => dsimp only [projectMapAux]; rw [Category.comp_id]
    | id_comp => dsimp only [projectMapAux]; rw [Category.id_comp]
    | assoc => dsimp only [projectMapAux]; rw [Category.assoc]
    | id_tensorHom_id => dsimp only [projectMapAux]; rw [MonoidalCategory.id_tensorHom_id]; rfl
    | tensorHom_comp_tensorHom =>
      dsimp only [projectMapAux]; rw [MonoidalCategory.tensorHom_comp_tensorHom]
    | whiskerLeft_id =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.whiskerLeft_id]
    | id_whiskerRight =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.id_whiskerRight]
    | α_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
    | α_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
    | associator_naturality =>
        dsimp only [projectMapAux]; rw [MonoidalCategory.associator_naturality]
    | ρ_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
    | ρ_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
    | ρ_naturality =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.rightUnitor_naturality]
    | l_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
    | l_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
    | l_naturality =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.leftUnitor_naturality]
    | pentagon =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.pentagon]
    | triangle =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.triangle]
Cleared hypotheses: h
-- 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
h : f ≈ g
refl :
  ∀ {X Y : F C} (f : X ⟶ᵐ Y),
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 f)
      (projectMapAux f_1 f)
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 f)
    (projectMapAux f_1 g)
have symm : ∀ {X Y : F C} (f g : X ⟶ᵐ Y),
  HomEquiv f g →
    ∀
      (hfg' :
        Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 f)
          (projectMapAux f_1 g)),
      Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 g)
        (projectMapAux f_1 f)
Tactic: induction h with
    | refl => rfl
    | symm _ _ _ hfg' => exact hfg'.symm
    | trans _ _ hfg hgh => exact hfg.trans hgh
    | comp _ _ hf hg => dsimp only [projectMapAux]; rw [hf, hg]
    | whiskerLeft _ _ _ _ hf => dsimp only [projectMapAux, projectObj]; rw [hf]
    | whiskerRight _ _ _ _ hf => dsimp only [projectMapAux, projectObj]; rw [hf]
    | tensor _ _ hfg hfg' => dsimp only [projectMapAux]; rw [hfg, hfg']
    | tensorHom_def _ _ =>
        dsimp only [projectMapAux, projectObj]; rw [MonoidalCategory.tensorHom_def]
    | comp_id => dsimp only [projectMapAux]; rw [Category.comp_id]
    | id_comp => dsimp only [projectMapAux]; rw [Category.id_comp]
    | assoc => dsimp only [projectMapAux]; rw [Category.assoc]
    | id_tensorHom_id => dsimp only [projectMapAux]; rw [MonoidalCategory.id_tensorHom_id]; rfl
    | tensorHom_comp_tensorHom =>
      dsimp only [projectMapAux]; rw [MonoidalCategory.tensorHom_comp_tensorHom]
    | whiskerLeft_id =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.whiskerLeft_id]
    | id_whiskerRight =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.id_whiskerRight]
    | α_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
    | α_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
    | associator_naturality =>
        dsimp only [projectMapAux]; rw [MonoidalCategory.associator_naturality]
    | ρ_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
    | ρ_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
    | ρ_naturality =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.rightUnitor_naturality]
    | l_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
    | l_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
    | l_naturality =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.leftUnitor_naturality]
    | pentagon =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.pentagon]
    | triangle =>
        dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.triangle]
Cleared hypotheses: h
-- 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 : X ⟶ Y
x : F C
⊢ Functor.map (project f_1) f ▷ Functor.obj.{u, v', u, u'} (project f_1) x ≫
      Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) Y)
            (Functor.obj.{u, v', u, u'} (project f_1) x))) =
    Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) X)
            (Functor.obj.{u, v', u, u'} (project f_1) x))) ≫
      Functor.map (project f_1) (f ▷ x)
have f₁ : ∀ (a : X ⟶ᵐ Y),
  Functor.map (project f_1) ⟦a⟧ ▷ Functor.obj.{u, v', u, u'} (project f_1) x ≫
      Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) Y)
            (Functor.obj.{u, v', u, u'} (project f_1) x))) =
    Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) X)
            (Functor.obj.{u, v', u, u'} (project f_1) x))) ≫
      Functor.map (project f_1) (⟦a⟧ ▷ x)
Tactic: induction f using Quotient.recOn
Cleared hypotheses: f
-- 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 : X ⟶ Y
x : F C
f₁ :
  ∀ (a : X ⟶ᵐ Y),
    Functor.map (project f_1) ⟦a⟧ ▷ Functor.obj.{u, v', u, u'} (project f_1) x ≫
        Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) Y)
              (Functor.obj.{u, v', u, u'} (project f_1) x))) =
      Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) X)
              (Functor.obj.{u, v', u, u'} (project f_1) x))) ≫
        Functor.map (project f_1) (⟦a⟧ ▷ x)
⊢ Functor.map (project f_1) f ▷ Functor.obj.{u, v', u, u'} (project f_1) x ≫
      Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) Y)
            (Functor.obj.{u, v', u, u'} (project f_1) x))) =
    Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) X)
            (Functor.obj.{u, v', u, u'} (project f_1) x))) ≫
      Functor.map (project f_1) (f ▷ x)
have h : ∀ (a b : X ⟶ᵐ Y) (p : a ≈ b),
  Eq (α :=
    Functor.map (project f_1) ⟦b⟧ ▷ Functor.obj.{u, v', u, u'} (project f_1) x ≫
        Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) Y)
              (Functor.obj.{u, v', u, u'} (project f_1) x))) =
      Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) X)
              (Functor.obj.{u, v', u, u'} (project f_1) x))) ≫
        Functor.map (project f_1) (⟦b⟧ ▷ x))
    sorry sorry
Tactic: induction f using Quotient.recOn
-- 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 x : F C
f : X ⟶ Y
⊢ Functor.obj.{u, v', u, u'} (project f_1) x ◁ Functor.map (project f_1) f ≫
      Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
            (Functor.obj.{u, v', u, u'} (project f_1) Y))) =
    Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
            (Functor.obj.{u, v', u, u'} (project f_1) X))) ≫
      Functor.map (project f_1) (x ◁ f)
have f₁ : ∀ (a : X ⟶ᵐ Y),
  Functor.obj.{u, v', u, u'} (project f_1) x ◁ Functor.map (project f_1) ⟦a⟧ ≫
      Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
            (Functor.obj.{u, v', u, u'} (project f_1) Y))) =
    Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
            (Functor.obj.{u, v', u, u'} (project f_1) X))) ≫
      Functor.map (project f_1) (x ◁ ⟦a⟧)
Tactic: induction f using Quotient.recOn
Cleared hypotheses: f
-- 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 x : F C
f : X ⟶ Y
f₁ :
  ∀ (a : X ⟶ᵐ Y),
    Functor.obj.{u, v', u, u'} (project f_1) x ◁ Functor.map (project f_1) ⟦a⟧ ≫
        Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
              (Functor.obj.{u, v', u, u'} (project f_1) Y))) =
      Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
              (Functor.obj.{u, v', u, u'} (project f_1) X))) ≫
        Functor.map (project f_1) (x ◁ ⟦a⟧)
⊢ Functor.obj.{u, v', u, u'} (project f_1) x ◁ Functor.map (project f_1) f ≫
      Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
            (Functor.obj.{u, v', u, u'} (project f_1) Y))) =
    Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
            (Functor.obj.{u, v', u, u'} (project f_1) X))) ≫
      Functor.map (project f_1) (x ◁ f)
have h : ∀ (a b : X ⟶ᵐ Y) (p : a ≈ b),
  Eq (α :=
    Functor.obj.{u, v', u, u'} (project f_1) x ◁ Functor.map (project f_1) ⟦b⟧ ≫
        Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
              (Functor.obj.{u, v', u, u'} (project f_1) Y))) =
      Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
              (Functor.obj.{u, v', u, u'} (project f_1) X))) ≫
        Functor.map (project f_1) (x ◁ ⟦b⟧))
    sorry sorry
Tactic: induction f using Quotient.recOn
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Coherence (goal)
Goal:
C : Type u
Z : F C
n n' : (Discrete ∘ NormalMonoidalObject) C
f : n ⟶ n'
⊢ ((tensorFunc C).obj Z).map f = map inclusion f ▷ Z
have mk : ∀ (as : NormalMonoidalObject C) (f : { as := as : Discrete (NormalMonoidalObject C) } ⟶ n'),
  ((tensorFunc C).obj Z).map f = map inclusion f ▷ Z
Tactic: cases n
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Coherence (goal)
Goal:
C : Type u
Z : F C
n' : (Discrete ∘ NormalMonoidalObject) C
as : NormalMonoidalObject C
f : { as := as : Discrete (NormalMonoidalObject C) } ⟶ n'
⊢ ((tensorFunc C).obj Z).map f = map inclusion f ▷ Z
have mk : ∀ (as_1 : NormalMonoidalObject C) (f : { as := as : Discrete (NormalMonoidalObject C) } ⟶ { as := as_1 }),
  ((tensorFunc C).obj Z).map f = map inclusion f ▷ Z
Tactic: cases n'
Cleared hypotheses: n', f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Coherence (goal)
Goal:
C : Type u
Z : F C
as as_1 : NormalMonoidalObject C
f : { as := as : Discrete (NormalMonoidalObject C) } ⟶ { as := as_1 }
⊢ ((tensorFunc C).obj Z).map f = map inclusion f ▷ Z
have mk : ∀ (h : { as := as : Discrete (NormalMonoidalObject C) }.as = { as := as_1 }.as),
  ((tensorFunc C).obj Z).map
      {
        down :=
          { down := h :
            PLift
              ({ as := as : Discrete (NormalMonoidalObject C) }.as =
                { as := as_1 : Discrete (NormalMonoidalObject C) }.as) } :
        ULift.{u, 0}
          (PLift
            ({ as := as : Discrete (NormalMonoidalObject C) }.as =
              { as := as_1 : Discrete (NormalMonoidalObject C) }.as)) } =
    map inclusion { down := { down := h } } ▷ Z
Tactic: rcases f with ⟨⟨h⟩⟩
Cleared hypotheses: f