awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
D : Type u₂
D' : Type u₃
E : Type u₄
inst_2 : Category.{v₂, u₂} D
inst_3 : Category.{v₃, u₃} D'
inst_4 : Category.{v₄, u₄} E
H : Functor.{v₂, v₁, u₂, u₁} D V
L : Functor.{v₂, v₃, u₂, u₃} D D'
H' : Functor.{v₃, v₁, u₃, u₁} D' V
α : H ⟶ L ⋙ H'
K : Functor.{v₄, v₁, u₄, u₁} E V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst_5 : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft (K.obj e))
cone : Limits.Cocone (J := CostructuredArrow (Functor.prod (𝟭 E) L) (e, d))
  (CostructuredArrow.proj (Functor.prod (𝟭 E) L) (e, d) ⋙ K ⊠ H) :=
  (Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)
equiv : CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d ≌
  CostructuredArrow (Functor.prod (𝟭 E) L) (e, d) :=
  Equivalence.symm (CostructuredArrow.prodEquivalence (𝟭 E) L e d)
I : CostructuredArrow L d ⥤ CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d :=
  Equivalence.inverse (prod.leftUnitorEquivalence (CostructuredArrow L d)) ⋙
    Functor.prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 (Functor.obj.{v₄, v₄, u₄, u₄} (𝟭 E) e))))
      (𝟭 (CostructuredArrow L d))
this : Functor.Final (D := CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e)
  (Functor.fromPUnit (CostructuredArrow.mk (𝟙 e))) :=
  ⋯
apply :
  Functor.Final (C := Discrete PUnit.{1} × CostructuredArrow L d) (D :=
    CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d)
    (Functor.prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 e))) (𝟭 (CostructuredArrow L d)))
⊢ I.Final

Tactic:
apply Iff.mp <| Functor.final_iff_final_comp
      (F := (prod.leftUnitorEquivalence <| CostructuredArrow L d).inverse)
      (G := Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e) |>.prod <| 𝟭 _)

Premises used: CategoryTheory.Functor.id, CategoryTheory.CategoryStruct.id, CategoryTheory.CostructuredArrow, CategoryTheory.Functor.prod, CategoryTheory.prod.leftUnitorEquivalence, CategoryTheory.Functor.final_iff_final_comp, Iff.mp, CategoryTheory.CostructuredArrow.mk, CategoryTheory.Functor.fromPUnit, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
D : Type u₂
D' : Type u₃
E : Type u₄
inst_2 : Category.{v₂, u₂} D
inst_3 : Category.{v₃, u₃} D'
inst_4 : Category.{v₄, u₄} E
H : Functor.{v₂, v₁, u₂, u₁} D V
L : Functor.{v₂, v₃, u₂, u₃} D D'
H' : Functor.{v₃, v₁, u₃, u₁} D' V
α : H ⟶ L ⋙ H'
K : Functor.{v₄, v₁, u₄, u₁} E V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst_5 : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft (K.obj e))
cone : Limits.Cocone (J := CostructuredArrow (Functor.prod (𝟭 E) L) (e, d))
  (CostructuredArrow.proj (Functor.prod (𝟭 E) L) (e, d) ⋙ K ⊠ H) :=
  (Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)
equiv : CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d ≌
  CostructuredArrow (Functor.prod (𝟭 E) L) (e, d) :=
  Equivalence.symm (CostructuredArrow.prodEquivalence (𝟭 E) L e d)
I : CostructuredArrow L d ⥤ CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d :=
  Equivalence.inverse (prod.leftUnitorEquivalence (CostructuredArrow L d)) ⋙
    Functor.prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 (Functor.obj.{v₄, v₄, u₄, u₄} (𝟭 E) e))))
      (𝟭 (CostructuredArrow L d))
this : Functor.Final (D := CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e)
  (Functor.fromPUnit (CostructuredArrow.mk (𝟙 e))) :=
  ⋯
⊢ Functor.Final (C := Discrete PUnit.{1} × CostructuredArrow L d) (D :=
    CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d)
    (Functor.prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 e))) (𝟭 (CostructuredArrow L d)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
D : Type u₂
D' : Type u₃
E : Type u₄
inst_2 : Category.{v₂, u₂} D
inst_3 : Category.{v₃, u₃} D'
inst_4 : Category.{v₄, u₄} E
H : Functor.{v₂, v₁, u₂, u₁} D V
L : Functor.{v₂, v₃, u₂, u₃} D D'
H' : Functor.{v₃, v₁, u₃, u₁} D' V
α : H ⟶ L ⋙ H'
K : Functor.{v₄, v₁, u₄, u₁} E V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst_5 : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft (K.obj e))
cone : Limits.Cocone (J := CostructuredArrow (Functor.prod (𝟭 E) L) (e, d))
  (CostructuredArrow.proj (Functor.prod (𝟭 E) L) (e, d) ⋙ K ⊠ H) :=
  (Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)
equiv : CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d ≌
  CostructuredArrow (Functor.prod (𝟭 E) L) (e, d) :=
  Equivalence.symm (CostructuredArrow.prodEquivalence (𝟭 E) L e d)
I : CostructuredArrow L d ⥤ CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d :=
  Equivalence.inverse (prod.leftUnitorEquivalence (CostructuredArrow L d)) ⋙
    Functor.prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 (Functor.obj.{v₄, v₄, u₄, u₄} (𝟭 E) e))))
      (𝟭 (CostructuredArrow L d))
this : I.Final := ⋯
apply : Limits.IsColimit (Limits.Cocone.whisker I (Limits.Cocone.whisker equiv.functor cone))
⊢ Limits.IsColimit
    (Limits.Cocone.whisker equiv.functor
      ((Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)))

Tactic:
apply Functor.Final.isColimitWhiskerEquiv I (Limits.Cocone.whisker equiv.functor cone) |>.toFun

Premises used: CategoryTheory.Limits.Cocone.whisker, CategoryTheory.Equivalence.functor, Equiv.toFun, CategoryTheory.Functor.Final.isColimitWhiskerEquiv
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
D : Type u₂
D' : Type u₃
E : Type u₄
inst_2 : Category.{v₂, u₂} D
inst_3 : Category.{v₃, u₃} D'
inst_4 : Category.{v₄, u₄} E
H : Functor.{v₂, v₁, u₂, u₁} D V
L : Functor.{v₂, v₃, u₂, u₃} D D'
H' : Functor.{v₃, v₁, u₃, u₁} D' V
α : H ⟶ L ⋙ H'
K : Functor.{v₄, v₁, u₄, u₁} E V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst_5 : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft (K.obj e))
cone : Limits.Cocone (J := CostructuredArrow (Functor.prod (𝟭 E) L) (e, d))
  (CostructuredArrow.proj (Functor.prod (𝟭 E) L) (e, d) ⋙ K ⊠ H) :=
  (Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)
equiv : CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d ≌
  CostructuredArrow (Functor.prod (𝟭 E) L) (e, d) :=
  Equivalence.symm (CostructuredArrow.prodEquivalence (𝟭 E) L e d)
I : CostructuredArrow L d ⥤ CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d :=
  Equivalence.inverse (prod.leftUnitorEquivalence (CostructuredArrow L d)) ⋙
    Functor.prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 (Functor.obj.{v₄, v₄, u₄, u₄} (𝟭 E) e))))
      (𝟭 (CostructuredArrow L d))
this : I.Final := ⋯
diag_iso : (CostructuredArrow.proj L d ⋙ H) ⋙ tensorLeft (K.obj e) ≅
  I ⋙ equiv.functor ⋙ CostructuredArrow.proj (Functor.prod (𝟭 E) L) (e, d) ⋙ K ⊠ H :=
  NatIso.ofComponents
    (fun (x : CostructuredArrow L d) ↦ Iso.refl (((CostructuredArrow.proj L d ⋙ H) ⋙ tensorLeft (K.obj e)).obj x)) ⋯
apply :
  Limits.IsColimit (F := (CostructuredArrow.proj L d ⋙ H) ⋙ tensorLeft (K.obj e))
    (Functor.mapCocone (tensorLeft (K.obj e)) ((Functor.LeftExtension.mk H' α).coconeAt d))
⊢ Limits.IsColimit (Limits.Cocone.whisker I (Limits.Cocone.whisker equiv.functor cone))

Tactic:
apply Limits.IsColimit.equivOfNatIsoOfIso diag_iso
    (d := Limits.Cocone.whisker I <| Limits.Cocone.whisker equiv.functor cone)
    (c := (tensorLeft <| K.obj e).mapCocone <| (Functor.LeftExtension.mk H' α).coconeAt d)
    (Limits.Cocone.ext <| .refl _) |>.toFun

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Functor.LeftExtension.mk, CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.Limits.Cocone.whisker, CategoryTheory.Iso.refl, CategoryTheory.Equivalence.functor, Equiv.toFun, CategoryTheory.Functor.LeftExtension.coconeAt, CategoryTheory.MonoidalCategory.tensorLeft, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
D : Type u₂
D' : Type u₃
E : Type u₄
inst_2 : Category.{v₂, u₂} D
inst_3 : Category.{v₃, u₃} D'
inst_4 : Category.{v₄, u₄} E
H : Functor.{v₂, v₁, u₂, u₁} D V
L : Functor.{v₂, v₃, u₂, u₃} D D'
H' : Functor.{v₃, v₁, u₃, u₁} D' V
α : H ⟶ L ⋙ H'
K : Functor.{v₄, v₁, u₄, u₁} E V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst_5 : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft (K.obj e))
cone : Limits.Cocone (J := CostructuredArrow (Functor.prod (𝟭 E) L) (e, d))
  (CostructuredArrow.proj (Functor.prod (𝟭 E) L) (e, d) ⋙ K ⊠ H) :=
  (Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)
equiv : CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d ≌
  CostructuredArrow (Functor.prod (𝟭 E) L) (e, d) :=
  Equivalence.symm (CostructuredArrow.prodEquivalence (𝟭 E) L e d)
I : CostructuredArrow L d ⥤ CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d :=
  Equivalence.inverse (prod.leftUnitorEquivalence (CostructuredArrow L d)) ⋙
    Functor.prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 (Functor.obj.{v₄, v₄, u₄, u₄} (𝟭 E) e))))
      (𝟭 (CostructuredArrow L d))
this : I.Final := ⋯
diag_iso : (CostructuredArrow.proj L d ⋙ H) ⋙ tensorLeft (K.obj e) ≅
  I ⋙ equiv.functor ⋙ CostructuredArrow.proj (Functor.prod (𝟭 E) L) (e, d) ⋙ K ⊠ H :=
  NatIso.ofComponents
    (fun (x : CostructuredArrow L d) ↦ Iso.refl (((CostructuredArrow.proj L d ⋙ H) ⋙ tensorLeft (K.obj e)).obj x)) ⋯
⊢ Limits.IsColimit (F := (CostructuredArrow.proj L d ⋙ H) ⋙ tensorLeft (K.obj e))
    (Functor.mapCocone (tensorLeft (K.obj e)) ((Functor.LeftExtension.mk H' α).coconeAt d))

Tactic:
exact Limits.PreservesColimit.preserves (F := tensorLeft <| K.obj e) P |>.some

Premises used: Nonempty.some, CategoryTheory.Limits.PreservesColimit.preserves
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X Y : F C
f_1 : Quotient (X.setoidHom Y)
f : X ⟶ᵐ Y
⊢ Eq (α := Quotient (X.setoidHom Y))
    (Quotient.map₂ (sb := X.setoidHom Y) Hom.comp ⋯ ⟦Hom.id X⟧
      (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f))
    (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f)

Tactic:
Quotient.sound (id_comp f)

Premises used: CategoryTheory.FreeMonoidalCategory.HomEquiv.id_comp, Quotient.map₂, Quotient.sound
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X Y : F C
f_1 : Quotient (X.setoidHom Y)
f : X ⟶ᵐ Y
⊢ Eq (α := Quotient (X.setoidHom Y))
    (Quotient.map₂ (sb := X.setoidHom Y) Hom.comp ⋯ ⟦Hom.id X⟧
      (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f))
    (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f)

Tactic:
exact Quotient.sound (id_comp f)

Premises used: Quotient.sound
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X Y : F C
f_1 : Quotient (X.setoidHom Y)
f : X ⟶ᵐ Y
⊢ Eq (α := Quotient (X.setoidHom Y))
    (Quotient.map₂ (sa := X.setoidHom Y) Hom.comp ⋯ (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f)
      ⟦Hom.id Y⟧)
    (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f)

Tactic:
Quotient.sound (comp_id f)

Premises used: Quotient.map₂, CategoryTheory.FreeMonoidalCategory.HomEquiv.comp_id, Quotient.sound
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X Y : F C
f_1 : Quotient (X.setoidHom Y)
f : X ⟶ᵐ Y
⊢ Eq (α := Quotient (X.setoidHom Y))
    (Quotient.map₂ (sa := X.setoidHom Y) Hom.comp ⋯ (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f)
      ⟦Hom.id Y⟧)
    (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f)

Tactic:
exact Quotient.sound (comp_id f)

Premises used: Quotient.sound
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
W X Y Z : F C
f_1 : Quotient (W.setoidHom X)
f : W ⟶ᵐ X
g_1 : Quotient (X.setoidHom Y)
g : X ⟶ᵐ Y
h_1 : Quotient (Y.setoidHom Z)
h : Y ⟶ᵐ Z
⊢ Eq (α := Quotient (W.setoidHom Z))
    (Quotient.map₂ (sa := W.setoidHom Y) (sb := Y.setoidHom Z) Hom.comp ⋯
      (Quotient.map₂ (sa := W.setoidHom X) (sb := X.setoidHom Y) Hom.comp ⋯
        (Quot.mk (⇑(W.setoidHom X) : (W ⟶ᵐ X) → (W ⟶ᵐ X) → Prop) f)
        (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) g))
      (Quot.mk (⇑(Y.setoidHom Z) : (Y ⟶ᵐ Z) → (Y ⟶ᵐ Z) → Prop) h))
    (Quotient.map₂ (sa := W.setoidHom X) (sb := X.setoidHom Z) Hom.comp ⋯
      (Quot.mk (⇑(W.setoidHom X) : (W ⟶ᵐ X) → (W ⟶ᵐ X) → Prop) f)
      (Quotient.map₂ (sa := X.setoidHom Y) (sb := Y.setoidHom Z) Hom.comp ⋯
        (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) g)
        (Quot.mk (⇑(Y.setoidHom Z) : (Y ⟶ᵐ Z) → (Y ⟶ᵐ Z) → Prop) h)))

Tactic:
Quotient.sound (assoc f g h)

Premises used: CategoryTheory.FreeMonoidalCategory.HomEquiv.assoc, Quotient.map₂, Quotient.sound
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
W X Y Z : F C
f_1 : Quotient (W.setoidHom X)
f : W ⟶ᵐ X
g_1 : Quotient (X.setoidHom Y)
g : X ⟶ᵐ Y
h_1 : Quotient (Y.setoidHom Z)
h : Y ⟶ᵐ Z
⊢ Eq (α := Quotient (W.setoidHom Z))
    (Quotient.map₂ (sa := W.setoidHom Y) (sb := Y.setoidHom Z) Hom.comp ⋯
      (Quotient.map₂ (sa := W.setoidHom X) (sb := X.setoidHom Y) Hom.comp ⋯
        (Quot.mk (⇑(W.setoidHom X) : (W ⟶ᵐ X) → (W ⟶ᵐ X) → Prop) f)
        (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) g))
      (Quot.mk (⇑(Y.setoidHom Z) : (Y ⟶ᵐ Z) → (Y ⟶ᵐ Z) → Prop) h))
    (Quotient.map₂ (sa := W.setoidHom X) (sb := X.setoidHom Z) Hom.comp ⋯
      (Quot.mk (⇑(W.setoidHom X) : (W ⟶ᵐ X) → (W ⟶ᵐ X) → Prop) f)
      (Quotient.map₂ (sa := X.setoidHom Y) (sb := Y.setoidHom Z) Hom.comp ⋯
        (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) g)
        (Quot.mk (⇑(Y.setoidHom Z) : (Y ⟶ᵐ Z) → (Y ⟶ᵐ Z) → Prop) h)))

Tactic:
exact Quotient.sound (assoc f g h)

Premises used: Quotient.sound
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
W X Y Z : F C
f_1 : W ⟶ X
f : W ⟶ᵐ X
g_1 : Y ⟶ Z
g : Y ⟶ᵐ Z
⊢ Eq (α := W.tensor Y ⟶ X.tensor Z)
    (Quotient.map₂ (sa := W.setoidHom X) (sb := Y.setoidHom Z) Hom.tensor ⋯
      (Quot.mk (⇑(W.setoidHom X) : (W ⟶ᵐ X) → (W ⟶ᵐ X) → Prop) f)
      (Quot.mk (⇑(Y.setoidHom Z) : (Y ⟶ᵐ Z) → (Y ⟶ᵐ Z) → Prop) g))
    (CategoryStruct.comp (Y := X.tensor Y)
      (Quot.map (ra := HomEquiv) (rb :=
        (⇑((W.tensor Y).setoidHom (X.tensor Y)) : (W.tensor Y ⟶ᵐ X.tensor Y) → (W.tensor Y ⟶ᵐ X.tensor Y) → Prop))
        (fun (f : W ⟶ᵐ X) ↦ f.whiskerRight Y) ⋯ (Quot.mk (⇑(W.setoidHom X) : (W ⟶ᵐ X) → (W ⟶ᵐ X) → Prop) f))
      (Quot.map (ra := HomEquiv) (rb :=
        (⇑((X.tensor Y).setoidHom (X.tensor Z)) : (X.tensor Y ⟶ᵐ X.tensor Z) → (X.tensor Y ⟶ᵐ X.tensor Z) → Prop))
        (fun (f : Y ⟶ᵐ Z) ↦ Hom.whiskerLeft X f) ⋯ (Quot.mk (⇑(Y.setoidHom Z) : (Y ⟶ᵐ Z) → (Y ⟶ᵐ Z) → Prop) g)))

Tactic:
Quotient.sound (tensorHom_def _ _)

Premises used: Quotient.map₂, CategoryTheory.FreeMonoidalCategory.HomEquiv.tensorHom_def, Quotient.sound
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
W X Y Z : F C
f_1 : W ⟶ X
f : W ⟶ᵐ X
g_1 : Y ⟶ Z
g : Y ⟶ᵐ Z
⊢ Eq (α := W.tensor Y ⟶ X.tensor Z)
    (Quotient.map₂ (sa := W.setoidHom X) (sb := Y.setoidHom Z) Hom.tensor ⋯
      (Quot.mk (⇑(W.setoidHom X) : (W ⟶ᵐ X) → (W ⟶ᵐ X) → Prop) f)
      (Quot.mk (⇑(Y.setoidHom Z) : (Y ⟶ᵐ Z) → (Y ⟶ᵐ Z) → Prop) g))
    (CategoryStruct.comp (Y := X.tensor Y)
      (Quot.map (ra := HomEquiv) (rb :=
        (⇑((W.tensor Y).setoidHom (X.tensor Y)) : (W.tensor Y ⟶ᵐ X.tensor Y) → (W.tensor Y ⟶ᵐ X.tensor Y) → Prop))
        (fun (f : W ⟶ᵐ X) ↦ f.whiskerRight Y) ⋯ (Quot.mk (⇑(W.setoidHom X) : (W ⟶ᵐ X) → (W ⟶ᵐ X) → Prop) f))
      (Quot.map (ra := HomEquiv) (rb :=
        (⇑((X.tensor Y).setoidHom (X.tensor Z)) : (X.tensor Y ⟶ᵐ X.tensor Z) → (X.tensor Y ⟶ᵐ X.tensor Z) → Prop))
        (fun (f : Y ⟶ᵐ Z) ↦ Hom.whiskerLeft X f) ⋯ (Quot.mk (⇑(Y.setoidHom Z) : (Y ⟶ᵐ Z) → (Y ⟶ᵐ Z) → Prop) g)))

Tactic:
exact Quotient.sound (tensorHom_def _ _)
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : F C
f₁_1 : X₁ ⟶ Y₁
f₁ : X₁ ⟶ᵐ Y₁
f₂_1 : X₂ ⟶ Y₂
f₂ : X₂ ⟶ᵐ Y₂
g₁_1 : Y₁ ⟶ Z₁
g₁ : Y₁ ⟶ᵐ Z₁
g₂_1 : Y₂ ⟶ Z₂
g₂ : Y₂ ⟶ᵐ Z₂
⊢ Eq.{u + 1} (α := X₁.tensor X₂ ⟶ Z₁.tensor Z₂)
    (Quotient.map₂ (sa := X₁.setoidHom Y₁) (sb := X₂.setoidHom Y₂) Hom.tensor ⋯
        (Quot.mk (⇑(X₁.setoidHom Y₁) : (X₁ ⟶ᵐ Y₁) → (X₁ ⟶ᵐ Y₁) → Prop) f₁)
        (Quot.mk (⇑(X₂.setoidHom Y₂) : (X₂ ⟶ᵐ Y₂) → (X₂ ⟶ᵐ Y₂) → Prop) f₂) ≫
      Quotient.map₂ (sa := Y₁.setoidHom Z₁) (sb := Y₂.setoidHom Z₂) Hom.tensor ⋯
        (Quot.mk (⇑(Y₁.setoidHom Z₁) : (Y₁ ⟶ᵐ Z₁) → (Y₁ ⟶ᵐ Z₁) → Prop) g₁)
        (Quot.mk (⇑(Y₂.setoidHom Z₂) : (Y₂ ⟶ᵐ Z₂) → (Y₂ ⟶ᵐ Z₂) → Prop) g₂))
    (Quotient.map₂ (sa := X₁.setoidHom Z₁) (sb := X₂.setoidHom Z₂) Hom.tensor ⋯
      (Quot.mk (⇑(X₁.setoidHom Y₁) : (X₁ ⟶ᵐ Y₁) → (X₁ ⟶ᵐ Y₁) → Prop) f₁ ≫
        Quot.mk (⇑(Y₁.setoidHom Z₁) : (Y₁ ⟶ᵐ Z₁) → (Y₁ ⟶ᵐ Z₁) → Prop) g₁)
      (Quot.mk (⇑(X₂.setoidHom Y₂) : (X₂ ⟶ᵐ Y₂) → (X₂ ⟶ᵐ Y₂) → Prop) f₂ ≫
        Quot.mk (⇑(Y₂.setoidHom Z₂) : (Y₂ ⟶ᵐ Z₂) → (Y₂ ⟶ᵐ Z₂) → Prop) g₂))

Tactic:
Quotient.sound (tensorHom_comp_tensorHom _ _ _ _)

Premises used: CategoryTheory.FreeMonoidalCategory.HomEquiv.tensorHom_comp_tensorHom, Quotient.map₂, Quotient.sound
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : F C
f₁_1 : X₁ ⟶ Y₁
f₁ : X₁ ⟶ᵐ Y₁
f₂_1 : X₂ ⟶ Y₂
f₂ : X₂ ⟶ᵐ Y₂
g₁_1 : Y₁ ⟶ Z₁
g₁ : Y₁ ⟶ᵐ Z₁
g₂_1 : Y₂ ⟶ Z₂
g₂ : Y₂ ⟶ᵐ Z₂
⊢ Eq.{u + 1} (α := X₁.tensor X₂ ⟶ Z₁.tensor Z₂)
    (Quotient.map₂ (sa := X₁.setoidHom Y₁) (sb := X₂.setoidHom Y₂) Hom.tensor ⋯
        (Quot.mk (⇑(X₁.setoidHom Y₁) : (X₁ ⟶ᵐ Y₁) → (X₁ ⟶ᵐ Y₁) → Prop) f₁)
        (Quot.mk (⇑(X₂.setoidHom Y₂) : (X₂ ⟶ᵐ Y₂) → (X₂ ⟶ᵐ Y₂) → Prop) f₂) ≫
      Quotient.map₂ (sa := Y₁.setoidHom Z₁) (sb := Y₂.setoidHom Z₂) Hom.tensor ⋯
        (Quot.mk (⇑(Y₁.setoidHom Z₁) : (Y₁ ⟶ᵐ Z₁) → (Y₁ ⟶ᵐ Z₁) → Prop) g₁)
        (Quot.mk (⇑(Y₂.setoidHom Z₂) : (Y₂ ⟶ᵐ Z₂) → (Y₂ ⟶ᵐ Z₂) → Prop) g₂))
    (Quotient.map₂ (sa := X₁.setoidHom Z₁) (sb := X₂.setoidHom Z₂) Hom.tensor ⋯
      (Quot.mk (⇑(X₁.setoidHom Y₁) : (X₁ ⟶ᵐ Y₁) → (X₁ ⟶ᵐ Y₁) → Prop) f₁ ≫
        Quot.mk (⇑(Y₁.setoidHom Z₁) : (Y₁ ⟶ᵐ Z₁) → (Y₁ ⟶ᵐ Z₁) → Prop) g₁)
      (Quot.mk (⇑(X₂.setoidHom Y₂) : (X₂ ⟶ᵐ Y₂) → (X₂ ⟶ᵐ Y₂) → Prop) f₂ ≫
        Quot.mk (⇑(Y₂.setoidHom Z₂) : (Y₂ ⟶ᵐ Z₂) → (Y₂ ⟶ᵐ Z₂) → Prop) g₂))

Tactic:
exact Quotient.sound (tensorHom_comp_tensorHom _ _ _ _)
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X₁ X₂ X₃ Y₁ Y₂ Y₃ : F C
f₁_1 : X₁ ⟶ Y₁
f₁ : X₁ ⟶ᵐ Y₁
f₂_1 : X₂ ⟶ Y₂
f₂ : X₂ ⟶ᵐ Y₂
f₃_1 : X₃ ⟶ Y₃
f₃ : X₃ ⟶ᵐ Y₃
⊢ Eq.{u + 1} (α := (X₁.tensor X₂).tensor X₃ ⟶ Y₁.tensor (Y₂.tensor Y₃))
    (Quotient.map₂ (sa := (X₁.tensor X₂).setoidHom (Y₁.tensor Y₂)) (sb := X₃.setoidHom Y₃) Hom.tensor ⋯
        (Quotient.map₂ (sa := X₁.setoidHom Y₁) (sb := X₂.setoidHom Y₂) Hom.tensor ⋯
          (Quot.mk (⇑(X₁.setoidHom Y₁) : (X₁ ⟶ᵐ Y₁) → (X₁ ⟶ᵐ Y₁) → Prop) f₁)
          (Quot.mk (⇑(X₂.setoidHom Y₂) : (X₂ ⟶ᵐ Y₂) → (X₂ ⟶ᵐ Y₂) → Prop) f₂))
        (Quot.mk (⇑(X₃.setoidHom Y₃) : (X₃ ⟶ᵐ Y₃) → (X₃ ⟶ᵐ Y₃) → Prop) f₃) ≫
      Iso.hom { hom := ⟦Hom.α_hom Y₁ Y₂ Y₃⟧, inv := ⟦Hom.α_inv Y₁ Y₂ Y₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ })
    (Iso.hom { hom := ⟦Hom.α_hom X₁ X₂ X₃⟧, inv := ⟦Hom.α_inv X₁ X₂ X₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
      Quotient.map₂ (sa := X₁.setoidHom Y₁) (sb := (X₂.tensor X₃).setoidHom (Y₂.tensor Y₃)) Hom.tensor ⋯
        (Quot.mk (⇑(X₁.setoidHom Y₁) : (X₁ ⟶ᵐ Y₁) → (X₁ ⟶ᵐ Y₁) → Prop) f₁)
        (Quotient.map₂ (sa := X₂.setoidHom Y₂) (sb := X₃.setoidHom Y₃) Hom.tensor ⋯
          (Quot.mk (⇑(X₂.setoidHom Y₂) : (X₂ ⟶ᵐ Y₂) → (X₂ ⟶ᵐ Y₂) → Prop) f₂)
          (Quot.mk (⇑(X₃.setoidHom Y₃) : (X₃ ⟶ᵐ Y₃) → (X₃ ⟶ᵐ Y₃) → Prop) f₃)))

Tactic:
Quotient.sound (associator_naturality _ _ _)

Premises used: Quotient.map₂, CategoryTheory.FreeMonoidalCategory.HomEquiv.associator_naturality, Quotient.sound
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X₁ X₂ X₃ Y₁ Y₂ Y₃ : F C
f₁_1 : X₁ ⟶ Y₁
f₁ : X₁ ⟶ᵐ Y₁
f₂_1 : X₂ ⟶ Y₂
f₂ : X₂ ⟶ᵐ Y₂
f₃_1 : X₃ ⟶ Y₃
f₃ : X₃ ⟶ᵐ Y₃
⊢ Eq.{u + 1} (α := (X₁.tensor X₂).tensor X₃ ⟶ Y₁.tensor (Y₂.tensor Y₃))
    (Quotient.map₂ (sa := (X₁.tensor X₂).setoidHom (Y₁.tensor Y₂)) (sb := X₃.setoidHom Y₃) Hom.tensor ⋯
        (Quotient.map₂ (sa := X₁.setoidHom Y₁) (sb := X₂.setoidHom Y₂) Hom.tensor ⋯
          (Quot.mk (⇑(X₁.setoidHom Y₁) : (X₁ ⟶ᵐ Y₁) → (X₁ ⟶ᵐ Y₁) → Prop) f₁)
          (Quot.mk (⇑(X₂.setoidHom Y₂) : (X₂ ⟶ᵐ Y₂) → (X₂ ⟶ᵐ Y₂) → Prop) f₂))
        (Quot.mk (⇑(X₃.setoidHom Y₃) : (X₃ ⟶ᵐ Y₃) → (X₃ ⟶ᵐ Y₃) → Prop) f₃) ≫
      Iso.hom { hom := ⟦Hom.α_hom Y₁ Y₂ Y₃⟧, inv := ⟦Hom.α_inv Y₁ Y₂ Y₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ })
    (Iso.hom { hom := ⟦Hom.α_hom X₁ X₂ X₃⟧, inv := ⟦Hom.α_inv X₁ X₂ X₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
      Quotient.map₂ (sa := X₁.setoidHom Y₁) (sb := (X₂.tensor X₃).setoidHom (Y₂.tensor Y₃)) Hom.tensor ⋯
        (Quot.mk (⇑(X₁.setoidHom Y₁) : (X₁ ⟶ᵐ Y₁) → (X₁ ⟶ᵐ Y₁) → Prop) f₁)
        (Quotient.map₂ (sa := X₂.setoidHom Y₂) (sb := X₃.setoidHom Y₃) Hom.tensor ⋯
          (Quot.mk (⇑(X₂.setoidHom Y₂) : (X₂ ⟶ᵐ Y₂) → (X₂ ⟶ᵐ Y₂) → Prop) f₂)
          (Quot.mk (⇑(X₃.setoidHom Y₃) : (X₃ ⟶ᵐ Y₃) → (X₃ ⟶ᵐ Y₃) → Prop) f₃)))

Tactic:
exact Quotient.sound (associator_naturality _ _ _)
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X Y : F C
f_1 : X ⟶ Y
f : X ⟶ᵐ Y
⊢ Eq.{u + 1} (α := tensor unit X ⟶ Y)
    (CategoryStruct.comp (Y := tensor unit Y)
      (Quot.map (ra := HomEquiv) (rb :=
        (⇑((unit.tensor X).setoidHom (unit.tensor Y)) :
          (unit.tensor X ⟶ᵐ unit.tensor Y) → (unit.tensor X ⟶ᵐ unit.tensor Y) → Prop))
        (fun (f : X ⟶ᵐ Y) ↦ Hom.whiskerLeft unit f) ⋯ (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f))
      (Iso.hom { hom := ⟦Hom.l_hom Y⟧, inv := ⟦Hom.l_inv Y⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }))
    (Iso.hom { hom := ⟦Hom.l_hom X⟧, inv := ⟦Hom.l_inv X⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
      Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f)

Tactic:
Quotient.sound (l_naturality _)

Premises used: CategoryTheory.FreeMonoidalCategory.HomEquiv.l_naturality, Quotient.map₂, Quotient.sound
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X Y : F C
f_1 : X ⟶ Y
f : X ⟶ᵐ Y
⊢ Eq.{u + 1} (α := tensor unit X ⟶ Y)
    (CategoryStruct.comp (Y := tensor unit Y)
      (Quot.map (ra := HomEquiv) (rb :=
        (⇑((unit.tensor X).setoidHom (unit.tensor Y)) :
          (unit.tensor X ⟶ᵐ unit.tensor Y) → (unit.tensor X ⟶ᵐ unit.tensor Y) → Prop))
        (fun (f : X ⟶ᵐ Y) ↦ Hom.whiskerLeft unit f) ⋯ (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f))
      (Iso.hom { hom := ⟦Hom.l_hom Y⟧, inv := ⟦Hom.l_inv Y⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }))
    (Iso.hom { hom := ⟦Hom.l_hom X⟧, inv := ⟦Hom.l_inv X⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
      Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f)

Tactic:
exact Quotient.sound (l_naturality _)

Premises used: Quotient.sound
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X Y : F C
f_1 : X ⟶ Y
f : X ⟶ᵐ Y
⊢ Eq.{u + 1} (α := X.tensor unit ⟶ Y)
    (CategoryStruct.comp (Y := Y.tensor unit)
      (Quot.map (ra := HomEquiv) (rb :=
        (⇑((X.tensor unit).setoidHom (Y.tensor unit)) :
          (X.tensor unit ⟶ᵐ Y.tensor unit) → (X.tensor unit ⟶ᵐ Y.tensor unit) → Prop))
        (fun (f : X ⟶ᵐ Y) ↦ f.whiskerRight unit) ⋯ (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f))
      (Iso.hom { hom := ⟦Hom.ρ_hom Y⟧, inv := ⟦Hom.ρ_inv Y⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }))
    (Iso.hom { hom := ⟦Hom.ρ_hom X⟧, inv := ⟦Hom.ρ_inv X⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
      Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f)

Tactic:
Quotient.sound (ρ_naturality _)

Premises used: Quotient.map₂, CategoryTheory.FreeMonoidalCategory.HomEquiv.ρ_naturality, Quotient.sound