[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]
