Lean4
/-- The free functor `Type u ⥤ ModuleCat R` is a monoidal functor. -/
instance : (free R).Monoidal :=
Functor.CoreMonoidal.toMonoidal
{ εIso := εIso R
μIso := μIso R
μIso_hom_natural_left := fun {X Y} f X' ↦
by
rw [← cancel_epi (μIso R X X').inv]
aesop
μIso_hom_natural_right := fun {X Y} X' f ↦
by
rw [← cancel_epi (μIso R X' X).inv]
aesop
associativity := fun X Y Z ↦
by
rw [← cancel_epi ((μIso R X Y).inv ▷ _), ← cancel_epi (μIso R _ _).inv]
ext ⟨⟨x, y⟩, z⟩
dsimp
rw [μIso_inv_freeMk, MonoidalCategory.whiskerRight_apply, μIso_inv_freeMk, MonoidalCategory.whiskerRight_apply,
μIso_hom_freeMk_tmul_freeMk, μIso_hom_freeMk_tmul_freeMk, free_map_apply, CategoryTheory.associator_hom_apply,
MonoidalCategory.associator_hom_apply, MonoidalCategory.whiskerLeft_apply, μIso_hom_freeMk_tmul_freeMk,
μIso_hom_freeMk_tmul_freeMk]
left_unitality := fun X ↦ by
rw [← cancel_epi (λ_ _).inv, Iso.inv_hom_id]
aesop
right_unitality := fun X ↦ by
rw [← cancel_epi (ρ_ _).inv, Iso.inv_hom_id]
aesop }
