[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X✝ X'✝ Y✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
⊢ (f ⊗ g) ≫ ((fun X Y => prod.braiding X Y) Y✝ Y'✝).hom = ((fun X Y => prod.braiding X Y) X✝ X'✝).hom ≫ (g ⊗ f)
[PROOFSTEP]
dsimp [tensorHom]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X✝ X'✝ Y✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
⊢ prod.map f g ≫ prod.lift prod.snd prod.fst = prod.lift prod.snd prod.fst ≫ prod.map g f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y Z : C
⊢ (α_ X Y Z).hom ≫ ((fun X Y => prod.braiding X Y) X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
    (((fun X Y => prod.braiding X Y) X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ ((fun X Y => prod.braiding X Y) X Z).hom)
[PROOFSTEP]
dsimp [monoidalOfHasFiniteProducts.associator_hom]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y Z : C
⊢ prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd) ≫
      prod.lift prod.snd prod.fst ≫ prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd) =
    prod.map (prod.lift prod.snd prod.fst) (𝟙 Z) ≫
      prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd) ≫
        prod.map (𝟙 Y) (prod.lift prod.snd prod.fst)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ ((fun X Y => prod.braiding X Y) (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
    (𝟙 X ⊗ ((fun X Y => prod.braiding X Y) Y Z).hom) ≫ (α_ X Z Y).inv ≫ (((fun X Y => prod.braiding X Y) X Z).hom ⊗ 𝟙 Y)
[PROOFSTEP]
dsimp [monoidalOfHasFiniteProducts.associator_inv]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y Z : C
⊢ prod.lift (prod.lift prod.fst (prod.snd ≫ prod.fst)) (prod.snd ≫ prod.snd) ≫
      prod.lift prod.snd prod.fst ≫ prod.lift (prod.lift prod.fst (prod.snd ≫ prod.fst)) (prod.snd ≫ prod.snd) =
    prod.map (𝟙 X) (prod.lift prod.snd prod.fst) ≫
      prod.lift (prod.lift prod.fst (prod.snd ≫ prod.fst)) (prod.snd ≫ prod.snd) ≫
        prod.map (prod.lift prod.snd prod.fst) (𝟙 Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ prod.lift prod.snd prod.fst ≫ prod.lift prod.snd prod.fst = 𝟙 (X ⨯ Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X✝ X'✝ Y✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
⊢ (f ⊗ g) ≫ (coprod.braiding Y✝ Y'✝).hom = (coprod.braiding X✝ X'✝).hom ≫ (g ⊗ f)
[PROOFSTEP]
dsimp [tensorHom]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X✝ X'✝ Y✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
⊢ coprod.map f g ≫ coprod.desc coprod.inr coprod.inl = coprod.desc coprod.inr coprod.inl ≫ coprod.map g f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ (α_ X Y Z).hom ≫ (coprod.braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
    ((coprod.braiding X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (coprod.braiding X Z).hom)
[PROOFSTEP]
dsimp [monoidalOfHasFiniteCoproducts.associator_hom]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) ≫
      coprod.desc coprod.inr coprod.inl ≫
        coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) =
    coprod.map (coprod.desc coprod.inr coprod.inl) (𝟙 Z) ≫
      coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) ≫
        coprod.map (𝟙 Y) (coprod.desc coprod.inr coprod.inl)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ (coprod.braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
    (𝟙 X ⊗ (coprod.braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((coprod.braiding X Z).hom ⊗ 𝟙 Y)
[PROOFSTEP]
dsimp [monoidalOfHasFiniteCoproducts.associator_inv]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) ≫
      coprod.desc coprod.inr coprod.inl ≫
        coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) =
    coprod.map (𝟙 X) (coprod.desc coprod.inr coprod.inl) ≫
      coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) ≫
        coprod.map (coprod.desc coprod.inr coprod.inl) (𝟙 Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y : C
⊢ (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y : C
⊢ coprod.desc coprod.inr coprod.inl ≫ coprod.desc coprod.inr coprod.inl = 𝟙 (X ⨿ Y)
[PROOFSTEP]
simp


[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F G : J ⥤ C
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj (limit F ⊗ limit G)).map f ≫ (fun j => limit.π F j ⊗ limit.π G j) j' =
    (fun j => limit.π F j ⊗ limit.π G j) j ≫ (F ⊗ G).map f
[PROOFSTEP]
dsimp
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F G : J ⥤ C
j j' : J
f : j ⟶ j'
⊢ 𝟙 (limit F ⊗ limit G) ≫ (limit.π F j' ⊗ limit.π G j') = (limit.π F j ⊗ limit.π G j) ≫ (F.map f ⊗ G.map f)
[PROOFSTEP]
simp only [Category.id_comp, ← tensor_comp, limit.w]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X✝ Y✝ X'✝ Y'✝ : J ⥤ C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
⊢ (map (fun F => limit F) f ⊗ map (fun F => limit F) g) ≫
      (fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j })
        Y✝ Y'✝ =
    (fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j }) X✝
        X'✝ ≫
      map (fun F => limit F) (f ⊗ g)
[PROOFSTEP]
ext
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X✝ Y✝ X'✝ Y'✝ : J ⥤ C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
j✝ : J
⊢ ((map (fun F => limit F) f ⊗ map (fun F => limit F) g) ≫
        (fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j })
          Y✝ Y'✝) ≫
      limit.π (Y✝ ⊗ Y'✝) j✝ =
    ((fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j }) X✝
          X'✝ ≫
        map (fun F => limit F) (f ⊗ g)) ≫
      limit.π (Y✝ ⊗ Y'✝) j✝
[PROOFSTEP]
dsimp
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X✝ Y✝ X'✝ Y'✝ : J ⥤ C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
j✝ : J
⊢ ((limMap f ⊗ limMap g) ≫
        limit.lift (Y✝ ⊗ Y'✝) { pt := limit Y✝ ⊗ limit Y'✝, π := NatTrans.mk fun j => limit.π Y✝ j ⊗ limit.π Y'✝ j }) ≫
      limit.π (Y✝ ⊗ Y'✝) j✝ =
    (limit.lift (X✝ ⊗ X'✝) { pt := limit X✝ ⊗ limit X'✝, π := NatTrans.mk fun j => limit.π X✝ j ⊗ limit.π X'✝ j } ≫
        limMap (f ⊗ g)) ≫
      limit.π (Y✝ ⊗ Y'✝) j✝
[PROOFSTEP]
simp only [limit.lift_π, Cones.postcompose_obj_π, Monoidal.tensorHom_app, limit.lift_map, NatTrans.comp_app,
  Category.assoc, ← tensor_comp, limMap_π]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
⊢ ((fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j }) X
          Y ⊗
        𝟙 (limit Z)) ≫
      (fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j })
          (X ⊗ Y) Z ≫
        map (fun F => limit F) (α_ X Y Z).hom =
    (α_ (limit X) (limit Y) (limit Z)).hom ≫
      (𝟙 (limit X) ⊗
          (fun F G =>
              limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j })
            Y Z) ≫
        (fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j })
          X (Y ⊗ Z)
[PROOFSTEP]
ext j
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
⊢ (((fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j }) X
            Y ⊗
          𝟙 (limit Z)) ≫
        (fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j })
            (X ⊗ Y) Z ≫
          map (fun F => limit F) (α_ X Y Z).hom) ≫
      limit.π (X ⊗ Y ⊗ Z) j =
    ((α_ (limit X) (limit Y) (limit Z)).hom ≫
        (𝟙 (limit X) ⊗
            (fun F G =>
                limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j })
              Y Z) ≫
          (fun F G =>
              limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j })
            X (Y ⊗ Z)) ≫
      limit.π (X ⊗ Y ⊗ Z) j
[PROOFSTEP]
dsimp
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
⊢ ((limit.lift (X ⊗ Y) { pt := limit X ⊗ limit Y, π := NatTrans.mk fun j => limit.π X j ⊗ limit.π Y j } ⊗ 𝟙 (limit Z)) ≫
        limit.lift ((X ⊗ Y) ⊗ Z)
            { pt := limit (X ⊗ Y) ⊗ limit Z, π := NatTrans.mk fun j => limit.π (X ⊗ Y) j ⊗ limit.π Z j } ≫
          limMap (α_ X Y Z).hom) ≫
      limit.π (X ⊗ Y ⊗ Z) j =
    ((α_ (limit X) (limit Y) (limit Z)).hom ≫
        (𝟙 (limit X) ⊗
            limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }) ≫
          limit.lift (X ⊗ Y ⊗ Z)
            { pt := limit X ⊗ limit (Y ⊗ Z), π := NatTrans.mk fun j => limit.π X j ⊗ limit.π (Y ⊗ Z) j }) ≫
      limit.π (X ⊗ Y ⊗ Z) j
[PROOFSTEP]
simp only [limit.lift_π, Cones.postcompose_obj_π, Monoidal.associator_hom_app, limit.lift_map, NatTrans.comp_app,
  Category.assoc]
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
⊢ (limit.lift (X ⊗ Y) { pt := limit X ⊗ limit Y, π := NatTrans.mk fun j => limit.π X j ⊗ limit.π Y j } ⊗ 𝟙 (limit Z)) ≫
      (limit.π (X ⊗ Y) j ⊗ limit.π Z j) ≫ (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom =
    (α_ (limit X) (limit Y) (limit Z)).hom ≫
      (𝟙 (limit X) ⊗
          limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }) ≫
        (limit.π X j ⊗ limit.π (Y ⊗ Z) j)
[PROOFSTEP]
slice_lhs 2 2 => rw [← tensor_id_comp_id_tensor]
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| limit.π (X ⊗ Y) j ⊗ limit.π Z j
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| limit.lift (X ⊗ Y) { pt := limit X ⊗ limit Y, π := NatTrans.mk fun j => limit.π X j ⊗ limit.π Y j } ⊗ 𝟙 (limit Z)
[PROOFSTEP]
rw [← tensor_id_comp_id_tensor]
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| limit.π (X ⊗ Y) j ⊗ limit.π Z j
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| limit.lift (X ⊗ Y) { pt := limit X ⊗ limit Y, π := NatTrans.mk fun j => limit.π X j ⊗ limit.π Y j } ⊗ 𝟙 (limit Z)
[PROOFSTEP]
rw [← tensor_id_comp_id_tensor]
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| limit.π (X ⊗ Y) j ⊗ limit.π Z j
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| limit.lift (X ⊗ Y) { pt := limit X ⊗ limit Y, π := NatTrans.mk fun j => limit.π X j ⊗ limit.π Y j } ⊗ 𝟙 (limit Z)
[PROOFSTEP]
rw [← tensor_id_comp_id_tensor]
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
⊢ (limit.lift (X ⊗ Y) { pt := limit X ⊗ limit Y, π := NatTrans.mk fun j => limit.π X j ⊗ limit.π Y j } ⊗ 𝟙 (limit Z)) ≫
      ((limit.π (X ⊗ Y) j ⊗ 𝟙 (limit Z)) ≫ (𝟙 (X.obj j ⊗ Y.obj j) ⊗ limit.π Z j)) ≫
        (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom =
    (α_ (limit X) (limit Y) (limit Z)).hom ≫
      (𝟙 (limit X) ⊗
          limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }) ≫
        (limit.π X j ⊗ limit.π (Y ⊗ Z) j)
[PROOFSTEP]
slice_lhs 1 2 =>
  rw [← comp_tensor_id, limit.lift_π]
  dsimp
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (limit.lift (X ⊗ Y) { pt := limit X ⊗ limit Y, π := NatTrans.mk fun j => limit.π X j ⊗ limit.π Y j } ⊗ 𝟙 (limit Z)) ≫
    (limit.π (X ⊗ Y) j ⊗ 𝟙 (limit Z))
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| 𝟙 (X.obj j ⊗ Y.obj j) ⊗ limit.π Z j
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom
[PROOFSTEP]
  rw [← comp_tensor_id, limit.lift_π]
  dsimp
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (limit.lift (X ⊗ Y) { pt := limit X ⊗ limit Y, π := NatTrans.mk fun j => limit.π X j ⊗ limit.π Y j } ⊗ 𝟙 (limit Z)) ≫
    (limit.π (X ⊗ Y) j ⊗ 𝟙 (limit Z))
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| 𝟙 (X.obj j ⊗ Y.obj j) ⊗ limit.π Z j
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom
[PROOFSTEP]
  rw [← comp_tensor_id, limit.lift_π]
  dsimp
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (limit.lift (X ⊗ Y) { pt := limit X ⊗ limit Y, π := NatTrans.mk fun j => limit.π X j ⊗ limit.π Y j } ⊗ 𝟙 (limit Z)) ≫
    (limit.π (X ⊗ Y) j ⊗ 𝟙 (limit Z))
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| 𝟙 (X.obj j ⊗ Y.obj j) ⊗ limit.π Z j
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom
[PROOFSTEP]
rw [← comp_tensor_id, limit.lift_π]
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| NatTrans.app { pt := limit X ⊗ limit Y, π := NatTrans.mk fun j => limit.π X j ⊗ limit.π Y j }.π j ⊗ 𝟙 (limit Z)
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| 𝟙 (X.obj j ⊗ Y.obj j) ⊗ limit.π Z j
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom
[PROOFSTEP]
dsimp
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
⊢ (((limit.π X j ⊗ limit.π Y j) ⊗ 𝟙 (limit Z)) ≫ (𝟙 (X.obj j ⊗ Y.obj j) ⊗ limit.π Z j)) ≫
      (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom =
    (α_ (limit X) (limit Y) (limit Z)).hom ≫
      (𝟙 (limit X) ⊗
          limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }) ≫
        (limit.π X j ⊗ limit.π (Y ⊗ Z) j)
[PROOFSTEP]
slice_lhs 1 2 => rw [tensor_id_comp_id_tensor]
[GOAL]
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| ((limit.π X j ⊗ limit.π Y j) ⊗ 𝟙 (limit Z)) ≫ (𝟙 (X.obj j ⊗ Y.obj j) ⊗ limit.π Z j)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom
[PROOFSTEP]
rw [tensor_id_comp_id_tensor]
[GOAL]
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| ((limit.π X j ⊗ limit.π Y j) ⊗ 𝟙 (limit Z)) ≫ (𝟙 (X.obj j ⊗ Y.obj j) ⊗ limit.π Z j)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom
[PROOFSTEP]
rw [tensor_id_comp_id_tensor]
[GOAL]
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| ((limit.π X j ⊗ limit.π Y j) ⊗ 𝟙 (limit Z)) ≫ (𝟙 (X.obj j ⊗ Y.obj j) ⊗ limit.π Z j)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom
[PROOFSTEP]
rw [tensor_id_comp_id_tensor]
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
⊢ ((limit.π X j ⊗ limit.π Y j) ⊗ limit.π Z j) ≫ (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom =
    (α_ (limit X) (limit Y) (limit Z)).hom ≫
      (𝟙 (limit X) ⊗
          limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }) ≫
        (limit.π X j ⊗ limit.π (Y ⊗ Z) j)
[PROOFSTEP]
conv_lhs => rw [associator_naturality]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| ((limit.π X j ⊗ limit.π Y j) ⊗ limit.π Z j) ≫ (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom
[PROOFSTEP]
rw [associator_naturality]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| ((limit.π X j ⊗ limit.π Y j) ⊗ limit.π Z j) ≫ (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom
[PROOFSTEP]
rw [associator_naturality]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| ((limit.π X j ⊗ limit.π Y j) ⊗ limit.π Z j) ≫ (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom
[PROOFSTEP]
rw [associator_naturality]
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
⊢ (α_ (limit X) (limit Y) (limit Z)).hom ≫ (limit.π X j ⊗ limit.π Y j ⊗ limit.π Z j) =
    (α_ (limit X) (limit Y) (limit Z)).hom ≫
      (𝟙 (limit X) ⊗
          limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }) ≫
        (limit.π X j ⊗ limit.π (Y ⊗ Z) j)
[PROOFSTEP]
conv_rhs => rw [← id_tensor_comp_tensor_id (limit.π (Y ⊗ Z) j)]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (limit X) (limit Y) (limit Z)).hom ≫
    (𝟙 (limit X) ⊗
        limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }) ≫
      (limit.π X j ⊗ limit.π (Y ⊗ Z) j)
[PROOFSTEP]
rw [← id_tensor_comp_tensor_id (limit.π (Y ⊗ Z) j)]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (limit X) (limit Y) (limit Z)).hom ≫
    (𝟙 (limit X) ⊗
        limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }) ≫
      (limit.π X j ⊗ limit.π (Y ⊗ Z) j)
[PROOFSTEP]
rw [← id_tensor_comp_tensor_id (limit.π (Y ⊗ Z) j)]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (limit X) (limit Y) (limit Z)).hom ≫
    (𝟙 (limit X) ⊗
        limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }) ≫
      (limit.π X j ⊗ limit.π (Y ⊗ Z) j)
[PROOFSTEP]
rw [← id_tensor_comp_tensor_id (limit.π (Y ⊗ Z) j)]
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
⊢ (α_ (limit X) (limit Y) (limit Z)).hom ≫ (limit.π X j ⊗ limit.π Y j ⊗ limit.π Z j) =
    (α_ (limit X) (limit Y) (limit Z)).hom ≫
      (𝟙 (limit X) ⊗
          limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }) ≫
        (𝟙 (limit X) ⊗ limit.π (Y ⊗ Z) j) ≫ (limit.π X j ⊗ 𝟙 ((Y ⊗ Z).obj j))
[PROOFSTEP]
slice_rhs 2 3 =>
  rw [← id_tensor_comp, limit.lift_π]
  dsimp
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (𝟙 (limit X) ⊗ limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }) ≫
    (𝟙 (limit X) ⊗ limit.π (Y ⊗ Z) j)
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| limit.π X j ⊗ 𝟙 ((Y ⊗ Z).obj j)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (limit X) (limit Y) (limit Z)).hom
[PROOFSTEP]
  rw [← id_tensor_comp, limit.lift_π]
  dsimp
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (𝟙 (limit X) ⊗ limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }) ≫
    (𝟙 (limit X) ⊗ limit.π (Y ⊗ Z) j)
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| limit.π X j ⊗ 𝟙 ((Y ⊗ Z).obj j)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (limit X) (limit Y) (limit Z)).hom
[PROOFSTEP]
  rw [← id_tensor_comp, limit.lift_π]
  dsimp
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (𝟙 (limit X) ⊗ limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }) ≫
    (𝟙 (limit X) ⊗ limit.π (Y ⊗ Z) j)
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| limit.π X j ⊗ 𝟙 ((Y ⊗ Z).obj j)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (limit X) (limit Y) (limit Z)).hom
[PROOFSTEP]
rw [← id_tensor_comp, limit.lift_π]
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| 𝟙 (limit X) ⊗ NatTrans.app { pt := limit Y ⊗ limit Z, π := NatTrans.mk fun j => limit.π Y j ⊗ limit.π Z j }.π j
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| limit.π X j ⊗ 𝟙 ((Y ⊗ Z).obj j)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
| (α_ (limit X) (limit Y) (limit Z)).hom
[PROOFSTEP]
dsimp
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
⊢ (α_ (limit X) (limit Y) (limit Z)).hom ≫ (limit.π X j ⊗ limit.π Y j ⊗ limit.π Z j) =
    (α_ (limit X) (limit Y) (limit Z)).hom ≫
      (𝟙 (limit X) ⊗ limit.π Y j ⊗ limit.π Z j) ≫ (limit.π X j ⊗ 𝟙 ((Y ⊗ Z).obj j))
[PROOFSTEP]
dsimp
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X Y Z : J ⥤ C
j : J
⊢ (α_ (limit X) (limit Y) (limit Z)).hom ≫ (limit.π X j ⊗ limit.π Y j ⊗ limit.π Z j) =
    (α_ (limit X) (limit Y) (limit Z)).hom ≫
      (𝟙 (limit X) ⊗ limit.π Y j ⊗ limit.π Z j) ≫ (limit.π X j ⊗ 𝟙 (Y.obj j ⊗ Z.obj j))
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
⊢ (λ_ (limit X)).hom =
    (limit.lift ((Functor.const J).obj tensorUnit')
          { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 (((Functor.const J).obj tensorUnit').obj j) } ⊗
        𝟙 (limit X)) ≫
      (fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j })
          (𝟙_ (J ⥤ C)) X ≫
        map (fun F => limit F) (λ_ X).hom
[PROOFSTEP]
ext j
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
⊢ (λ_ (limit X)).hom ≫ limit.π X j =
    ((limit.lift ((Functor.const J).obj tensorUnit')
            { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 (((Functor.const J).obj tensorUnit').obj j) } ⊗
          𝟙 (limit X)) ≫
        (fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j })
            (𝟙_ (J ⥤ C)) X ≫
          map (fun F => limit F) (λ_ X).hom) ≫
      limit.π X j
[PROOFSTEP]
dsimp
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
⊢ (λ_ (limit X)).hom ≫ limit.π X j =
    ((limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' } ⊗
          𝟙 (limit X)) ≫
        limit.lift (𝟙_ (J ⥤ C) ⊗ X)
            { pt := limit (𝟙_ (J ⥤ C)) ⊗ limit X, π := NatTrans.mk fun j => limit.π (𝟙_ (J ⥤ C)) j ⊗ limit.π X j } ≫
          limMap (λ_ X).hom) ≫
      limit.π X j
[PROOFSTEP]
simp
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
⊢ (λ_ (limit X)).hom ≫ limit.π X j =
    (limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' } ⊗
        𝟙 (limit X)) ≫
      (limit.π (𝟙_ (J ⥤ C)) j ⊗ limit.π X j) ≫ (λ_ (X.obj j)).hom
[PROOFSTEP]
conv_rhs => rw [← tensor_id_comp_id_tensor (limit.π X j)]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' } ⊗
      𝟙 (limit X)) ≫
    (limit.π (𝟙_ (J ⥤ C)) j ⊗ limit.π X j) ≫ (λ_ (X.obj j)).hom
[PROOFSTEP]
rw [← tensor_id_comp_id_tensor (limit.π X j)]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' } ⊗
      𝟙 (limit X)) ≫
    (limit.π (𝟙_ (J ⥤ C)) j ⊗ limit.π X j) ≫ (λ_ (X.obj j)).hom
[PROOFSTEP]
rw [← tensor_id_comp_id_tensor (limit.π X j)]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' } ⊗
      𝟙 (limit X)) ≫
    (limit.π (𝟙_ (J ⥤ C)) j ⊗ limit.π X j) ≫ (λ_ (X.obj j)).hom
[PROOFSTEP]
rw [← tensor_id_comp_id_tensor (limit.π X j)]
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
⊢ (λ_ (limit X)).hom ≫ limit.π X j =
    (limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' } ⊗
        𝟙 (limit X)) ≫
      ((limit.π (𝟙_ (J ⥤ C)) j ⊗ 𝟙 (limit X)) ≫ (𝟙 (𝟙_ C) ⊗ limit.π X j)) ≫ (λ_ (X.obj j)).hom
[PROOFSTEP]
slice_rhs 1 2 =>
  rw [← comp_tensor_id]
  erw [limit.lift_π]
  dsimp
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' } ⊗
      𝟙 (limit X)) ≫
    (limit.π (𝟙_ (J ⥤ C)) j ⊗ 𝟙 (limit X))
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| 𝟙 (𝟙_ C) ⊗ limit.π X j
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (λ_ (X.obj j)).hom
[PROOFSTEP]
  rw [← comp_tensor_id]
  erw [limit.lift_π]
  dsimp
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' } ⊗
      𝟙 (limit X)) ≫
    (limit.π (𝟙_ (J ⥤ C)) j ⊗ 𝟙 (limit X))
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| 𝟙 (𝟙_ C) ⊗ limit.π X j
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (λ_ (X.obj j)).hom
[PROOFSTEP]
  rw [← comp_tensor_id]
  erw [limit.lift_π]
  dsimp
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' } ⊗
      𝟙 (limit X)) ≫
    (limit.π (𝟙_ (J ⥤ C)) j ⊗ 𝟙 (limit X))
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| 𝟙 (𝟙_ C) ⊗ limit.π X j
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (λ_ (X.obj j)).hom
[PROOFSTEP]
rw [← comp_tensor_id]
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' } ≫
      limit.π (𝟙_ (J ⥤ C)) j ⊗
    𝟙 (limit X)
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| 𝟙 (𝟙_ C) ⊗ limit.π X j
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (λ_ (X.obj j)).hom
[PROOFSTEP]
erw [limit.lift_π]
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| NatTrans.app { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' }.π j ⊗ 𝟙 (limit X)
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| 𝟙 (𝟙_ C) ⊗ limit.π X j
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (λ_ (X.obj j)).hom
[PROOFSTEP]
dsimp
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
⊢ (λ_ (limit X)).hom ≫ limit.π X j = ((𝟙 tensorUnit' ⊗ 𝟙 (limit X)) ≫ (𝟙 (𝟙_ C) ⊗ limit.π X j)) ≫ (λ_ (X.obj j)).hom
[PROOFSTEP]
slice_rhs 2 3 => rw [leftUnitor_naturality]
[GOAL]
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (𝟙 (𝟙_ C) ⊗ limit.π X j) ≫ (λ_ (X.obj j)).hom
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| 𝟙 tensorUnit' ⊗ 𝟙 (limit X)
[PROOFSTEP]
rw [leftUnitor_naturality]
[GOAL]
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (𝟙 (𝟙_ C) ⊗ limit.π X j) ≫ (λ_ (X.obj j)).hom
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| 𝟙 tensorUnit' ⊗ 𝟙 (limit X)
[PROOFSTEP]
rw [leftUnitor_naturality]
[GOAL]
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (𝟙 (𝟙_ C) ⊗ limit.π X j) ≫ (λ_ (X.obj j)).hom
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| 𝟙 tensorUnit' ⊗ 𝟙 (limit X)
[PROOFSTEP]
rw [leftUnitor_naturality]
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
⊢ (λ_ (limit X)).hom ≫ limit.π X j = (𝟙 tensorUnit' ⊗ 𝟙 (limit X)) ≫ (λ_ (limit X)).hom ≫ limit.π X j
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
⊢ (ρ_ (limit X)).hom =
    (𝟙 (limit X) ⊗
        limit.lift ((Functor.const J).obj tensorUnit')
          { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 (((Functor.const J).obj tensorUnit').obj j) }) ≫
      (fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j }) X
          (𝟙_ (J ⥤ C)) ≫
        map (fun F => limit F) (ρ_ X).hom
[PROOFSTEP]
ext j
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
⊢ (ρ_ (limit X)).hom ≫ limit.π X j =
    ((𝟙 (limit X) ⊗
          limit.lift ((Functor.const J).obj tensorUnit')
            { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 (((Functor.const J).obj tensorUnit').obj j) }) ≫
        (fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := NatTrans.mk fun j => limit.π F j ⊗ limit.π G j })
            X (𝟙_ (J ⥤ C)) ≫
          map (fun F => limit F) (ρ_ X).hom) ≫
      limit.π X j
[PROOFSTEP]
dsimp
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
⊢ (ρ_ (limit X)).hom ≫ limit.π X j =
    ((𝟙 (limit X) ⊗
          limit.lift ((Functor.const J).obj tensorUnit')
            { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' }) ≫
        limit.lift (X ⊗ 𝟙_ (J ⥤ C))
            { pt := limit X ⊗ limit (𝟙_ (J ⥤ C)), π := NatTrans.mk fun j => limit.π X j ⊗ limit.π (𝟙_ (J ⥤ C)) j } ≫
          limMap (ρ_ X).hom) ≫
      limit.π X j
[PROOFSTEP]
simp
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
⊢ (ρ_ (limit X)).hom ≫ limit.π X j =
    (𝟙 (limit X) ⊗
        limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' }) ≫
      (limit.π X j ⊗ limit.π (𝟙_ (J ⥤ C)) j) ≫ (ρ_ (X.obj j)).hom
[PROOFSTEP]
conv_rhs => rw [← id_tensor_comp_tensor_id _ (limit.π X j)]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (𝟙 (limit X) ⊗
      limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' }) ≫
    (limit.π X j ⊗ limit.π (𝟙_ (J ⥤ C)) j) ≫ (ρ_ (X.obj j)).hom
[PROOFSTEP]
rw [← id_tensor_comp_tensor_id _ (limit.π X j)]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (𝟙 (limit X) ⊗
      limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' }) ≫
    (limit.π X j ⊗ limit.π (𝟙_ (J ⥤ C)) j) ≫ (ρ_ (X.obj j)).hom
[PROOFSTEP]
rw [← id_tensor_comp_tensor_id _ (limit.π X j)]
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (𝟙 (limit X) ⊗
      limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' }) ≫
    (limit.π X j ⊗ limit.π (𝟙_ (J ⥤ C)) j) ≫ (ρ_ (X.obj j)).hom
[PROOFSTEP]
rw [← id_tensor_comp_tensor_id _ (limit.π X j)]
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
⊢ (ρ_ (limit X)).hom ≫ limit.π X j =
    (𝟙 (limit X) ⊗
        limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' }) ≫
      ((𝟙 (limit X) ⊗ limit.π (𝟙_ (J ⥤ C)) j) ≫ (limit.π X j ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ (X.obj j)).hom
[PROOFSTEP]
slice_rhs 1 2 =>
  rw [← id_tensor_comp]
  erw [limit.lift_π]
  dsimp
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (𝟙 (limit X) ⊗
      limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' }) ≫
    (𝟙 (limit X) ⊗ limit.π (𝟙_ (J ⥤ C)) j)
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| limit.π X j ⊗ 𝟙 (𝟙_ C)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (ρ_ (X.obj j)).hom
[PROOFSTEP]
  rw [← id_tensor_comp]
  erw [limit.lift_π]
  dsimp
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (𝟙 (limit X) ⊗
      limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' }) ≫
    (𝟙 (limit X) ⊗ limit.π (𝟙_ (J ⥤ C)) j)
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| limit.π X j ⊗ 𝟙 (𝟙_ C)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (ρ_ (X.obj j)).hom
[PROOFSTEP]
  rw [← id_tensor_comp]
  erw [limit.lift_π]
  dsimp
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (𝟙 (limit X) ⊗
      limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' }) ≫
    (𝟙 (limit X) ⊗ limit.π (𝟙_ (J ⥤ C)) j)
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| limit.π X j ⊗ 𝟙 (𝟙_ C)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (ρ_ (X.obj j)).hom
[PROOFSTEP]
rw [← id_tensor_comp]
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| 𝟙 (limit X) ⊗
    limit.lift ((Functor.const J).obj tensorUnit') { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' } ≫
      limit.π (𝟙_ (J ⥤ C)) j
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| limit.π X j ⊗ 𝟙 (𝟙_ C)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (ρ_ (X.obj j)).hom
[PROOFSTEP]
erw [limit.lift_π]
[GOAL]
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| 𝟙 (limit X) ⊗ NatTrans.app { pt := tensorUnit', π := NatTrans.mk fun j => 𝟙 tensorUnit' }.π j
case a.a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| limit.π X j ⊗ 𝟙 (𝟙_ C)
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (ρ_ (X.obj j)).hom
[PROOFSTEP]
dsimp
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
⊢ (ρ_ (limit X)).hom ≫ limit.π X j = ((𝟙 (limit X) ⊗ 𝟙 tensorUnit') ≫ (limit.π X j ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ (X.obj j)).hom
[PROOFSTEP]
slice_rhs 2 3 => rw [rightUnitor_naturality]
[GOAL]
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (limit.π X j ⊗ 𝟙 (𝟙_ C)) ≫ (ρ_ (X.obj j)).hom
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| 𝟙 (limit X) ⊗ 𝟙 tensorUnit'
[PROOFSTEP]
rw [rightUnitor_naturality]
[GOAL]
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (limit.π X j ⊗ 𝟙 (𝟙_ C)) ≫ (ρ_ (X.obj j)).hom
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| 𝟙 (limit X) ⊗ 𝟙 tensorUnit'
[PROOFSTEP]
rw [rightUnitor_naturality]
[GOAL]
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| (limit.π X j ⊗ 𝟙 (𝟙_ C)) ≫ (ρ_ (X.obj j)).hom
case a
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
| 𝟙 (limit X) ⊗ 𝟙 tensorUnit'
[PROOFSTEP]
rw [rightUnitor_naturality]
[GOAL]
case w
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
X : J ⥤ C
j : J
⊢ (ρ_ (limit X)).hom ≫ limit.π X j = (𝟙 (limit X) ⊗ 𝟙 tensorUnit') ≫ (ρ_ (limit X)).hom ≫ limit.π X j
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F G : J ⥤ C
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj (limit F ⊗ limit G)).map f ≫ (fun j => limit.π F j ⊗ limit.π G j) j' =
    (fun j => limit.π F j ⊗ limit.π G j) j ≫ (F ⊗ G).map f
[PROOFSTEP]
dsimp
[GOAL]
J : Type v
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
inst✝ : MonoidalCategory C
F G : J ⥤ C
j j' : J
f : j ⟶ j'
⊢ 𝟙 (limit F ⊗ limit G) ≫ (limit.π F j' ⊗ limit.π G j') = (limit.π F j ⊗ limit.π G j) ≫ (F.map f ⊗ G.map f)
[PROOFSTEP]
simp only [Category.id_comp, ← tensor_comp, limit.w]


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f ↔ IsIso f.fst ∧ IsIso f.snd
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f → IsIso f.fst ∧ IsIso f.snd
[PROOFSTEP]
rintro ⟨g, hfg, hgf⟩
[GOAL]
case mp.mk.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
⊢ IsIso f.fst ∧ IsIso f.snd
[PROOFSTEP]
simp at hfg hgf
[GOAL]
case mp.mk.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f.fst ≫ g.fst = 𝟙 P ∧ f.snd ≫ g.snd = 𝟙 S
hgf : g.fst ≫ f.fst = 𝟙 Q ∧ g.snd ≫ f.snd = 𝟙 T
⊢ IsIso f.fst ∧ IsIso f.snd
[PROOFSTEP]
rcases hfg with ⟨hfg₁, hfg₂⟩
[GOAL]
case mp.mk.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hgf : g.fst ≫ f.fst = 𝟙 Q ∧ g.snd ≫ f.snd = 𝟙 T
hfg₁ : f.fst ≫ g.fst = 𝟙 P
hfg₂ : f.snd ≫ g.snd = 𝟙 S
⊢ IsIso f.fst ∧ IsIso f.snd
[PROOFSTEP]
rcases hgf with ⟨hgf₁, hgf₂⟩
[GOAL]
case mp.mk.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg₁ : f.fst ≫ g.fst = 𝟙 P
hfg₂ : f.snd ≫ g.snd = 𝟙 S
hgf₁ : g.fst ≫ f.fst = 𝟙 Q
hgf₂ : g.snd ≫ f.snd = 𝟙 T
⊢ IsIso f.fst ∧ IsIso f.snd
[PROOFSTEP]
exact ⟨⟨⟨g.1, hfg₁, hgf₁⟩⟩, ⟨⟨g.2, hfg₂, hgf₂⟩⟩⟩
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f.fst ∧ IsIso f.snd → IsIso f
[PROOFSTEP]
rintro ⟨⟨g₁, hfg₁, hgf₁⟩, ⟨g₂, hfg₂, hgf₂⟩⟩
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 (P, S).fst
hgf₁ : g₁ ≫ f.fst = 𝟙 (Q, T).fst
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 (P, S).snd
hgf₂ : g₂ ≫ f.snd = 𝟙 (Q, T).snd
⊢ IsIso f
[PROOFSTEP]
dsimp at hfg₁ hgf₁ hfg₂ hgf₂
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ IsIso f
[PROOFSTEP]
refine' ⟨⟨(g₁, g₂), _, _⟩⟩
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f ≫ (g₁, g₂) = 𝟙 (P, S)
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ (g₁, g₂) ≫ f = 𝟙 (Q, T)
[PROOFSTEP]
repeat {simp; constructor; assumption; assumption
}
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f ≫ (g₁, g₂) = 𝟙 (P, S)
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ (g₁, g₂) ≫ f = 𝟙 (Q, T)
[PROOFSTEP]
{simp; constructor; assumption; assumption
}
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f ≫ (g₁, g₂) = 𝟙 (P, S)
[PROOFSTEP]
simp
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f.fst ≫ g₁ = 𝟙 P ∧ f.snd ≫ g₂ = 𝟙 S
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f.fst ≫ g₁ = 𝟙 P
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f.snd ≫ g₂ = 𝟙 S
[PROOFSTEP]
assumption
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f.snd ≫ g₂ = 𝟙 S
[PROOFSTEP]
assumption
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ (g₁, g₂) ≫ f = 𝟙 (Q, T)
[PROOFSTEP]
{simp; constructor; assumption; assumption
}
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ (g₁, g₂) ≫ f = 𝟙 (Q, T)
[PROOFSTEP]
simp
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ g₁ ≫ f.fst = 𝟙 Q ∧ g₂ ≫ f.snd = 𝟙 T
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ g₁ ≫ f.fst = 𝟙 Q
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ g₂ ≫ f.snd = 𝟙 T
[PROOFSTEP]
assumption
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ g₂ ≫ f.snd = 𝟙 T
[PROOFSTEP]
assumption
[GOAL]

[PROOFSTEP]
{simp; constructor; assumption; assumption
}
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C × D
⊢ (𝟭 (C × D)).obj X = (swap C D ⋙ swap D C).obj X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : D × C
⊢ (swap D C ⋙ swap C D).obj X = (𝟭 (D × C)).obj X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ IsEquivalence (braiding C D).functor
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C × (C ⥤ D)
f : X ⟶ Y
g : Y ⟶ Z
⊢ { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map (f ≫ g) =
    { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map f ≫
      { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map g
[PROOFSTEP]
cases g
[GOAL]
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C × (C ⥤ D)
f : X ⟶ Y
fst✝ : Y.fst ⟶ Z.fst
snd✝ : Y.snd ⟶ Z.snd
⊢ { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
      (f ≫ (fst✝, snd✝)) =
    { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map f ≫
      { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝, snd✝)
[PROOFSTEP]
cases f
[GOAL]
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C × (C ⥤ D)
fst✝¹ : Y.fst ⟶ Z.fst
snd✝¹ : Y.snd ⟶ Z.snd
fst✝ : X.fst ⟶ Y.fst
snd✝ : X.snd ⟶ Y.snd
⊢ { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
      ((fst✝, snd✝) ≫ (fst✝¹, snd✝¹)) =
    { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝, snd✝) ≫
      { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝¹, snd✝¹)
[PROOFSTEP]
cases Z
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C × (C ⥤ D)
fst✝² : X.fst ⟶ Y.fst
snd✝² : X.snd ⟶ Y.snd
fst✝¹ : C
snd✝¹ : C ⥤ D
fst✝ : Y.fst ⟶ (fst✝¹, snd✝¹).fst
snd✝ : Y.snd ⟶ (fst✝¹, snd✝¹).snd
⊢ { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
      ((fst✝², snd✝²) ≫ (fst✝, snd✝)) =
    { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝², snd✝²) ≫
      { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝, snd✝)
[PROOFSTEP]
cases Y
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C × (C ⥤ D)
fst✝³ : C
snd✝³ : C ⥤ D
fst✝² : C
snd✝² : C ⥤ D
fst✝¹ : X.fst ⟶ (fst✝², snd✝²).fst
snd✝¹ : X.snd ⟶ (fst✝², snd✝²).snd
fst✝ : (fst✝², snd✝²).fst ⟶ (fst✝³, snd✝³).fst
snd✝ : (fst✝², snd✝²).snd ⟶ (fst✝³, snd✝³).snd
⊢ { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
      ((fst✝¹, snd✝¹) ≫ (fst✝, snd✝)) =
    { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝¹, snd✝¹) ≫
      { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝, snd✝)
[PROOFSTEP]
cases X
[GOAL]
case mk.mk.mk.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
fst✝⁴ : C
snd✝⁴ : C ⥤ D
fst✝³ : C
snd✝³ : C ⥤ D
fst✝² : (fst✝³, snd✝³).fst ⟶ (fst✝⁴, snd✝⁴).fst
snd✝² : (fst✝³, snd✝³).snd ⟶ (fst✝⁴, snd✝⁴).snd
fst✝¹ : C
snd✝¹ : C ⥤ D
fst✝ : (fst✝¹, snd✝¹).fst ⟶ (fst✝³, snd✝³).fst
snd✝ : (fst✝¹, snd✝¹).snd ⟶ (fst✝³, snd✝³).snd
⊢ { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
      ((fst✝, snd✝) ≫ (fst✝², snd✝²)) =
    { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝, snd✝) ≫
      { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝², snd✝²)
[PROOFSTEP]
simp only [prod_comp, NatTrans.comp_app, Functor.map_comp, Category.assoc]
[GOAL]
case mk.mk.mk.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
fst✝⁴ : C
snd✝⁴ : C ⥤ D
fst✝³ : C
snd✝³ : C ⥤ D
fst✝² : (fst✝³, snd✝³).fst ⟶ (fst✝⁴, snd✝⁴).fst
snd✝² : (fst✝³, snd✝³).snd ⟶ (fst✝⁴, snd✝⁴).snd
fst✝¹ : C
snd✝¹ : C ⥤ D
fst✝ : (fst✝¹, snd✝¹).fst ⟶ (fst✝³, snd✝³).fst
snd✝ : (fst✝¹, snd✝¹).snd ⟶ (fst✝³, snd✝³).snd
⊢ snd✝¹.map fst✝ ≫ snd✝¹.map fst✝² ≫ NatTrans.app snd✝ fst✝⁴ ≫ NatTrans.app snd✝² fst✝⁴ =
    snd✝¹.map fst✝ ≫ NatTrans.app snd✝ fst✝³ ≫ snd✝³.map fst✝² ≫ NatTrans.app snd✝² fst✝⁴
[PROOFSTEP]
rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app, Category.assoc, NatTrans.naturality]
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A × C
f : X ⟶ Y
⊢ (Functor.prod F H).map f ≫ (fun X => (app α X.fst, app β X.snd)) Y =
    (fun X => (app α X.fst, app β X.snd)) X ≫ (Functor.prod G I).map f
[PROOFSTEP]
cases X
[GOAL]
case mk
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
Y : A × C
fst✝ : A
snd✝ : C
f : (fst✝, snd✝) ⟶ Y
⊢ (Functor.prod F H).map f ≫ (fun X => (app α X.fst, app β X.snd)) Y =
    (fun X => (app α X.fst, app β X.snd)) (fst✝, snd✝) ≫ (Functor.prod G I).map f
[PROOFSTEP]
cases Y
[GOAL]
case mk.mk
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ (Functor.prod F H).map f ≫ (fun X => (app α X.fst, app β X.snd)) (fst✝, snd✝) =
    (fun X => (app α X.fst, app β X.snd)) (fst✝¹, snd✝¹) ≫ (Functor.prod G I).map f
[PROOFSTEP]
simp only [Functor.prod_map, prod_comp]
[GOAL]
case mk.mk
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ (F.map f.fst ≫ app α fst✝, H.map f.snd ≫ app β snd✝) = (app α fst✝¹ ≫ G.map f.fst, app β snd✝¹ ≫ I.map f.snd)
[PROOFSTEP]
rw [Prod.mk.inj_iff]
[GOAL]
case mk.mk
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ F.map f.fst ≫ app α fst✝ = app α fst✝¹ ≫ G.map f.fst ∧ H.map f.snd ≫ app β snd✝ = app β snd✝¹ ≫ I.map f.snd
[PROOFSTEP]
constructor
[GOAL]
case mk.mk.left
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ F.map f.fst ≫ app α fst✝ = app α fst✝¹ ≫ G.map f.fst
case mk.mk.right
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ H.map f.snd ≫ app β snd✝ = app β snd✝¹ ≫ I.map f.snd
[PROOFSTEP]
repeat {rw [naturality]
}
[GOAL]
case mk.mk.left
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ F.map f.fst ≫ app α fst✝ = app α fst✝¹ ≫ G.map f.fst
case mk.mk.right
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ H.map f.snd ≫ app β snd✝ = app β snd✝¹ ≫ I.map f.snd
[PROOFSTEP]
{rw [naturality]
}
[GOAL]
case mk.mk.left
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ F.map f.fst ≫ app α fst✝ = app α fst✝¹ ≫ G.map f.fst
[PROOFSTEP]
rw [naturality]
[GOAL]
case mk.mk.right
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ H.map f.snd ≫ app β snd✝ = app β snd✝¹ ≫ I.map f.snd
[PROOFSTEP]
{rw [naturality]
}
[GOAL]
case mk.mk.right
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ H.map f.snd ≫ app β snd✝ = app β snd✝¹ ≫ I.map f.snd
[PROOFSTEP]
rw [naturality]
[GOAL]

[PROOFSTEP]
{rw [naturality]
}
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
X✝ Y✝ : A ⥤ B × C
α : X✝ ⟶ Y✝
X Y : A
f : X ⟶ Y
⊢ ((fun F => (F ⋙ Prod.fst B C, F ⋙ Prod.snd B C)) X✝).fst.map f ≫ (fun X => (NatTrans.app α X).fst) Y =
    (fun X => (NatTrans.app α X).fst) X ≫ ((fun F => (F ⋙ Prod.fst B C, F ⋙ Prod.snd B C)) Y✝).fst.map f
[PROOFSTEP]
simp only [Functor.comp_map, Prod.fst_map, ← prod_comp_fst, α.naturality]
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
X✝ Y✝ : A ⥤ B × C
α : X✝ ⟶ Y✝
X Y : A
f : X ⟶ Y
⊢ ((fun F => (F ⋙ Prod.fst B C, F ⋙ Prod.snd B C)) X✝).snd.map f ≫ (fun X => (NatTrans.app α X).snd) Y =
    (fun X => (NatTrans.app α X).snd) X ≫ ((fun F => (F ⋙ Prod.fst B C, F ⋙ Prod.snd B C)) Y✝).snd.map f
[PROOFSTEP]
simp only [Functor.comp_map, Prod.snd_map, ← prod_comp_snd, α.naturality]