[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
