[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
⊢ ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
    ((Functor.mk src✝.toPrefunctor).map f ⊗ (Functor.mk src✝.toPrefunctor).map g) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) Y Y' =
      (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X X' ≫ (Functor.mk src✝.toPrefunctor).map (f ⊗ g)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
⊢ ((fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X Y ⊗ 𝟙 ((Functor.mk src✝.toPrefunctor).obj Z)) ≫
      (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) (X ⊗ Y) Z ≫ (Functor.mk src✝.toPrefunctor).map (α_ X Y Z).hom =
    (α_ ((Functor.mk src✝.toPrefunctor).obj X) ((Functor.mk src✝.toPrefunctor).obj Y)
          ((Functor.mk src✝.toPrefunctor).obj Z)).hom ≫
      (𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) Y Z) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X (Y ⊗ Z)
[PROOFSTEP]
ext ⟨⟨f, g⟩, h⟩
[GOAL]
case h.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : (Functor.mk src✝.toPrefunctor).obj Z
f : (Functor.mk src✝.toPrefunctor).obj X
g : (Functor.mk src✝.toPrefunctor).obj Y
⊢ (((fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X Y ⊗ 𝟙 ((Functor.mk src✝.toPrefunctor).obj Z)) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) (X ⊗ Y) Z ≫ (Functor.mk src✝.toPrefunctor).map (α_ X Y Z).hom)
      ((f, g), h) =
    ((α_ ((Functor.mk src✝.toPrefunctor).obj X) ((Functor.mk src✝.toPrefunctor).obj Y)
            ((Functor.mk src✝.toPrefunctor).obj Z)).hom ≫
        (𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) Y Z) ≫
          (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X (Y ⊗ Z))
      ((f, g), h)
[PROOFSTEP]
dsimp at f g h 
[GOAL]
case h.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
⊢ (((fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X Y ⊗ 𝟙 ((Functor.mk src✝.toPrefunctor).obj Z)) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) (X ⊗ Y) Z ≫ (Functor.mk src✝.toPrefunctor).map (α_ X Y Z).hom)
      ((f, g), h) =
    ((α_ ((Functor.mk src✝.toPrefunctor).obj X) ((Functor.mk src✝.toPrefunctor).obj Y)
            ((Functor.mk src✝.toPrefunctor).obj Z)).hom ≫
        (𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) Y Z) ≫
          (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X (Y ⊗ Z))
      ((f, g), h)
[PROOFSTEP]
dsimp
[GOAL]
case h.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
⊢ ((λ_ (𝟙_ C)).inv ≫ ((λ_ (𝟙_ C)).inv ≫ (f ⊗ g) ⊗ h)) ≫ (α_ X Y Z).hom =
    (λ_ (𝟙_ C)).inv ≫ (f ⊗ (λ_ (𝟙_ C)).inv ≫ (g ⊗ h))
[PROOFSTEP]
simp only [Iso.cancel_iso_inv_left, Category.assoc]
[GOAL]
case h.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
⊢ ((λ_ (𝟙_ C)).inv ≫ (f ⊗ g) ⊗ h) ≫ (α_ X Y Z).hom = f ⊗ (λ_ (𝟙_ C)).inv ≫ (g ⊗ h)
[PROOFSTEP]
conv_lhs =>
  rw [← Category.id_comp h, tensor_comp, Category.assoc, associator_naturality, ← Category.assoc, unitors_inv_equal,
    triangle_assoc_comp_right_inv]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| ((λ_ (𝟙_ C)).inv ≫ (f ⊗ g) ⊗ h) ≫ (α_ X Y Z).hom
[PROOFSTEP]
rw [← Category.id_comp h, tensor_comp, Category.assoc, associator_naturality, ← Category.assoc, unitors_inv_equal,
    triangle_assoc_comp_right_inv]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| ((λ_ (𝟙_ C)).inv ≫ (f ⊗ g) ⊗ h) ≫ (α_ X Y Z).hom
[PROOFSTEP]
rw [← Category.id_comp h, tensor_comp, Category.assoc, associator_naturality, ← Category.assoc, unitors_inv_equal,
    triangle_assoc_comp_right_inv]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| ((λ_ (𝟙_ C)).inv ≫ (f ⊗ g) ⊗ h) ≫ (α_ X Y Z).hom
[PROOFSTEP]
rw [← Category.id_comp h, tensor_comp, Category.assoc, associator_naturality, ← Category.assoc, unitors_inv_equal,
  triangle_assoc_comp_right_inv]
[GOAL]
case h.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
⊢ (𝟙 tensorUnit' ⊗ (λ_ (𝟙_ C)).inv) ≫ (f ⊗ g ⊗ h) = f ⊗ (λ_ (𝟙_ C)).inv ≫ (g ⊗ h)
[PROOFSTEP]
conv_rhs => rw [← Category.id_comp f, tensor_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| f ⊗ (λ_ (𝟙_ C)).inv ≫ (g ⊗ h)
[PROOFSTEP]
rw [← Category.id_comp f, tensor_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| f ⊗ (λ_ (𝟙_ C)).inv ≫ (g ⊗ h)
[PROOFSTEP]
rw [← Category.id_comp f, tensor_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| f ⊗ (λ_ (𝟙_ C)).inv ≫ (g ⊗ h)
[PROOFSTEP]
rw [← Category.id_comp f, tensor_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
⊢ ∀ (X : C),
    (λ_ ((Functor.mk src✝.toPrefunctor).obj X)).hom =
      ((fun _p => 𝟙 (op (𝟙_ C)).unop) ⊗ 𝟙 ((Functor.mk src✝.toPrefunctor).obj X)) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) (𝟙_ C) X ≫ (Functor.mk src✝.toPrefunctor).map (λ_ X).hom
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X : C
⊢ (ρ_ ((Functor.mk src✝.toPrefunctor).obj X)).hom =
    (𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ fun _p => 𝟙 (op (𝟙_ C)).unop) ≫
      (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X (𝟙_ C) ≫ (Functor.mk src✝.toPrefunctor).map (ρ_ X).hom
[PROOFSTEP]
ext ⟨f, ⟨⟩⟩
[GOAL]
case h.mk.unit
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X : C
f : (Functor.mk src✝.toPrefunctor).obj X
⊢ (ρ_ ((Functor.mk src✝.toPrefunctor).obj X)).hom (f, PUnit.unit) =
    ((𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ fun _p => 𝟙 (op (𝟙_ C)).unop) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X (𝟙_ C) ≫ (Functor.mk src✝.toPrefunctor).map (ρ_ X).hom)
      (f, PUnit.unit)
[PROOFSTEP]
dsimp at f 
[GOAL]
case h.mk.unit
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X : C
f : 𝟙_ C ⟶ X
⊢ (ρ_ ((Functor.mk src✝.toPrefunctor).obj X)).hom (f, PUnit.unit) =
    ((𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ fun _p => 𝟙 (op (𝟙_ C)).unop) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X (𝟙_ C) ≫ (Functor.mk src✝.toPrefunctor).map (ρ_ X).hom)
      (f, PUnit.unit)
[PROOFSTEP]
dsimp
[GOAL]
case h.mk.unit
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X : C
f : 𝟙_ C ⟶ X
⊢ f = ((λ_ (𝟙_ C)).inv ≫ (f ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ X).hom
[PROOFSTEP]
simp only [Category.assoc]
[GOAL]
case h.mk.unit
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X : C
f : 𝟙_ C ⟶ X
⊢ f = (λ_ (𝟙_ C)).inv ≫ (f ⊗ 𝟙 (𝟙_ C)) ≫ (ρ_ X).hom
[PROOFSTEP]
rw [rightUnitor_naturality, unitors_inv_equal, Iso.inv_hom_id_assoc]
