-- 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
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)
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)
trans :
  ∀ {X Y : F C} {f g h : X ⟶ᵐ Y},
    HomEquiv f g →
      HomEquiv g h →
        ∀
          (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))
          (hgh :
            Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 g)
              (projectMapAux f_1 h)),
          Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y) (projectMapAux f_1 f)
            (projectMapAux f_1 h)
comp :
  ∀ {X Y Z : F C} {f f' : X ⟶ᵐ Y} {g g' : Y ⟶ᵐ Z},
    HomEquiv f f' →
      HomEquiv g g' →
        ∀
          (hf :
            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'))
          (hg :
            Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g)
              (projectMapAux f_1 g')),
          Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 (f.comp g))
            (projectMapAux f_1 (f'.comp g'))
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f f' : Y ⟶ᵐ Z),
    HomEquiv f f' →
      ∀
        (hf :
          Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 f)
            (projectMapAux f_1 f')),
        Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X.tensor Y) ⟶ projectObj.{v', u, u'} f_1 (X.tensor Z))
          (projectMapAux f_1 (Hom.whiskerLeft X f)) (projectMapAux f_1 (Hom.whiskerLeft X f'))
whiskerRight :
  ∀ {Y Z : F C} (f f' : Y ⟶ᵐ Z) (X : F C),
    HomEquiv f f' →
      ∀
        (hf :
          Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 f)
            (projectMapAux f_1 f')),
        Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (Y.tensor X) ⟶ projectObj.{v', u, u'} f_1 (Z.tensor X))
          (projectMapAux f_1 (f.whiskerRight X)) (projectMapAux f_1 (f'.whiskerRight X))
tensor :
  ∀ {W X Y Z : F C} {f f' : W ⟶ᵐ X} {g g' : Y ⟶ᵐ Z},
    HomEquiv f f' →
      HomEquiv g g' →
        ∀
          (hfg :
            Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 W ⟶ projectObj.{v', u, u'} f_1 X) (projectMapAux f_1 f)
              (projectMapAux f_1 f'))
          (hfg' :
            Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g)
              (projectMapAux f_1 g')),
          Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y) ⟶ projectObj.{v', u, u'} f_1 (X.tensor Z))
            (projectMapAux f_1 (f.tensor g)) (projectMapAux f_1 (f'.tensor g'))
tensorHom_def :
  ∀ {X₁ Y₁ X₂ Y₂ : F C} (f : X₁ ⟶ᵐ Y₁) (g : 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.tensor g)) (projectMapAux f_1 ((f.whiskerRight X₂).comp (Hom.whiskerLeft Y₁ g)))
comp_id :
  ∀ {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.comp (Hom.id Y))) (projectMapAux f_1 f)
id_comp :
  ∀ {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 ((Hom.id X).comp f)) (projectMapAux f_1 f)
assoc :
  ∀ {X Y U V : F C} (f : X ⟶ᵐ U) (g : U ⟶ᵐ V) (h : V ⟶ᵐ Y),
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 Y)
      (projectMapAux f_1 ((f.comp g).comp h)) (projectMapAux f_1 (f.comp (g.comp h)))
id_tensorHom_id :
  ∀ {X Y : F C},
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X.tensor Y) ⟶ projectObj.{v', u, u'} f_1 (X.tensor Y))
      (projectMapAux f_1 ((Hom.id X).tensor (Hom.id Y))) (projectMapAux f_1 (Hom.id (X.tensor Y)))
tensorHom_comp_tensorHom :
  ∀ {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₂)))
whiskerLeft_id :
  ∀ (X Y : F C),
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X.tensor Y) ⟶ projectObj.{v', u, u'} f_1 (X.tensor Y))
      (projectMapAux f_1 (Hom.whiskerLeft X (Hom.id Y))) (projectMapAux f_1 (Hom.id (X.tensor Y)))
id_whiskerRight :
  ∀ (X Y : F C),
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X.tensor Y) ⟶ projectObj.{v', u, u'} f_1 (X.tensor Y))
      (projectMapAux f_1 ((Hom.id X).whiskerRight Y)) (projectMapAux f_1 (Hom.id (X.tensor Y)))
α_hom_inv :
  ∀ {X Y Z : F C},
    Eq.{v' + 1} (α :=
      projectObj.{v', u, u'} f_1 ((X.tensor Y).tensor Z) ⟶ projectObj.{v', u, u'} f_1 ((X.tensor Y).tensor Z))
      (projectMapAux f_1 ((α_hom X Y Z).comp (α_inv X Y Z))) (projectMapAux f_1 (Hom.id ((X.tensor Y).tensor Z)))
α_inv_hom :
  ∀ {X Y Z : F C},
    Eq.{v' + 1} (α :=
      projectObj.{v', u, u'} f_1 (X.tensor (Y.tensor Z)) ⟶ projectObj.{v', u, u'} f_1 (X.tensor (Y.tensor Z)))
      (projectMapAux f_1 ((α_inv X Y Z).comp (α_hom X Y Z))) (projectMapAux f_1 (Hom.id (X.tensor (Y.tensor Z))))
associator_naturality :
  ∀ {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₃))))
ρ_hom_inv :
  ∀ {X : F C},
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X.tensor unit) ⟶ projectObj.{v', u, u'} f_1 (X.tensor unit))
      (projectMapAux f_1 ((ρ_hom X).comp (ρ_inv X))) (projectMapAux f_1 (Hom.id (X.tensor unit)))
ρ_inv_hom :
  ∀ {X : F C},
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 X)
      (projectMapAux f_1 ((ρ_inv X).comp (ρ_hom X))) (projectMapAux f_1 (Hom.id X))
ρ_naturality :
  ∀ {X Y : F C} (f : X ⟶ᵐ Y),
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X.tensor unit) ⟶ projectObj.{v', u, u'} f_1 Y)
      (projectMapAux f_1 (Hom.comp (f.whiskerRight unit) (ρ_hom Y))) (projectMapAux f_1 ((ρ_hom X).comp f))
l_hom_inv :
  ∀ {X : F C},
    Eq.{v' + 1} (α :=
      projectObj.{v', u, u'} f_1 (FreeMonoidalCategory.tensor unit X) ⟶
        projectObj.{v', u, u'} f_1 (FreeMonoidalCategory.tensor unit X))
      (projectMapAux f_1 ((l_hom X).comp (l_inv X))) (projectMapAux f_1 (Hom.id (FreeMonoidalCategory.tensor unit X)))
l_inv_hom :
  ∀ {X : F C},
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X ⟶ projectObj.{v', u, u'} f_1 X)
      (projectMapAux f_1 ((l_inv X).comp (l_hom X))) (projectMapAux f_1 (Hom.id X))
l_naturality :
  ∀ {X Y : F C} (f : X ⟶ᵐ Y),
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (FreeMonoidalCategory.tensor unit X) ⟶ projectObj.{v', u, u'} f_1 Y)
      (projectMapAux f_1 (Hom.comp (Hom.whiskerLeft unit f) (l_hom Y))) (projectMapAux f_1 ((l_hom X).comp f))
pentagon :
  ∀ {W X Y Z : F C},
    Eq.{v' + 1} (α :=
      projectObj.{v', u, u'} f_1 (((W.tensor X).tensor Y).tensor Z) ⟶
        projectObj.{v', u, u'} f_1 (W.tensor (X.tensor (Y.tensor Z))))
      (projectMapAux f_1
        (((α_hom W X Y).whiskerRight Z).comp (Hom.comp (α_hom W (X.tensor Y) Z) (Hom.whiskerLeft W (α_hom X Y Z)))))
      (projectMapAux f_1 ((α_hom (W.tensor X) Y Z).comp (α_hom W X (Y.tensor Z))))
triangle :
  ∀ {X Y : F C},
    Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 ((X.tensor unit).tensor Y) ⟶ projectObj.{v', u, u'} f_1 (X.tensor Y))
      (projectMapAux f_1 (Hom.comp (α_hom X unit Y) (Hom.whiskerLeft X (l_hom Y))))
      (projectMapAux f_1 ((ρ_hom X).whiskerRight 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 g)

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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.leftUnitor_naturality, CategoryTheory.Iso.inv_hom_id, CategoryTheory.FreeMonoidalCategory.HomEquiv.pentagon, CategoryTheory.FreeMonoidalCategory.HomEquiv.tensorHom_comp_tensorHom, CategoryTheory.FreeMonoidalCategory.HomEquiv.refl, CategoryTheory.FreeMonoidalCategory.HomEquiv.id_comp, CategoryTheory.FreeMonoidalCategory.HomEquiv.assoc, CategoryTheory.FreeMonoidalCategory.HomEquiv.l_naturality, CategoryTheory.Iso.hom_inv_id, CategoryTheory.FreeMonoidalCategory.HomEquiv.ρ_hom_inv, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.FreeMonoidalCategory.projectObj, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.id_whiskerRight, CategoryTheory.FreeMonoidalCategory.projectMapAux, CategoryTheory.FreeMonoidalCategory.HomEquiv.ρ_naturality, CategoryTheory.FreeMonoidalCategory.HomEquiv.id_whiskerRight, CategoryTheory.FreeMonoidalCategory.HomEquiv.α_inv_hom, CategoryTheory.FreeMonoidalCategory.HomEquiv.comp_id, CategoryTheory.FreeMonoidalCategory.HomEquiv.symm, CategoryTheory.MonoidalCategory.associator_naturality, CategoryTheory.FreeMonoidalCategory.HomEquiv.associator_naturality, CategoryTheory.FreeMonoidalCategory.HomEquiv.l_inv_hom, CategoryTheory.MonoidalCategory.whiskerLeft_id, CategoryTheory.MonoidalCategory.triangle, CategoryTheory.MonoidalCategory.id_tensorHom_id, CategoryTheory.FreeMonoidalCategory.HomEquiv.triangle, CategoryTheory.FreeMonoidalCategory.HomEquiv.ρ_inv_hom, CategoryTheory.FreeMonoidalCategory.HomEquiv.l_hom_inv, CategoryTheory.FreeMonoidalCategory.HomEquiv.tensorHom_def, CategoryTheory.FreeMonoidalCategory.HomEquiv.whiskerLeft_id, CategoryTheory.MonoidalCategory.rightUnitor_naturality, CategoryTheory.FreeMonoidalCategory.HomEquiv.trans, CategoryTheory.FreeMonoidalCategory.HomEquiv.α_hom_inv, CategoryTheory.FreeMonoidalCategory.HomEquiv.id_tensorHom_id, CategoryTheory.MonoidalCategory.pentagon, CategoryTheory.FreeMonoidalCategory.tensor, CategoryTheory.Category.id_comp