[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : LaxMonoidalFunctor C D
X : C
⊢ (λ_ (F.obj X)).inv ≫ (F.ε ⊗ 𝟙 (F.obj X)) ≫ μ F (𝟙_ C) X = F.map (λ_ X).inv
[PROOFSTEP]
rw [Iso.inv_comp_eq, F.left_unitality, Category.assoc, Category.assoc, ← F.toFunctor.map_comp, Iso.hom_inv_id,
  F.toFunctor.map_id, comp_id]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : LaxMonoidalFunctor C D
X : C
⊢ (ρ_ (F.obj X)).inv ≫ (𝟙 (F.obj X) ⊗ F.ε) ≫ μ F X (𝟙_ C) = F.map (ρ_ X).inv
[PROOFSTEP]
rw [Iso.inv_comp_eq, F.right_unitality, Category.assoc, Category.assoc, ← F.toFunctor.map_comp, Iso.hom_inv_id,
  F.toFunctor.map_id, comp_id]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : LaxMonoidalFunctor C D
X Y Z : C
⊢ (𝟙 (F.obj X) ⊗ μ F Y Z) ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ (μ F X Y ⊗ 𝟙 (F.obj Z)) ≫ μ F (X ⊗ Y) Z
[PROOFSTEP]
rw [Iso.eq_inv_comp, ← F.associativity_assoc, ← F.toFunctor.map_comp, Iso.hom_inv_id, F.toFunctor.map_id, comp_id]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ F.map (f ⊗ g) =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X X') ≫
      (F.map f ⊗ F.map g) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y Y'
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
⊢ F.map (λ_ X).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X) ≫ (inv F.ε ⊗ 𝟙 (F.obj X)) ≫ (λ_ (F.obj X)).hom
[PROOFSTEP]
simp only [LaxMonoidalFunctor.left_unitality]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
⊢ F.map (λ_ X).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X) ≫
      (inv F.ε ⊗ 𝟙 (F.obj X)) ≫
        (F.ε ⊗ 𝟙 (F.obj X)) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X ≫ F.map (λ_ X).hom
[PROOFSTEP]
slice_rhs 2 3 =>
  rw [← comp_tensor_id]
  simp
[GOAL]
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| (inv F.ε ⊗ 𝟙 (F.obj X)) ≫ (F.ε ⊗ 𝟙 (F.obj X))
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| F.map (λ_ X).hom
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X)
[PROOFSTEP]
  rw [← comp_tensor_id]
  simp
[GOAL]
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| (inv F.ε ⊗ 𝟙 (F.obj X)) ≫ (F.ε ⊗ 𝟙 (F.obj X))
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| F.map (λ_ X).hom
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X)
[PROOFSTEP]
  rw [← comp_tensor_id]
  simp
[GOAL]
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| (inv F.ε ⊗ 𝟙 (F.obj X)) ≫ (F.ε ⊗ 𝟙 (F.obj X))
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| F.map (λ_ X).hom
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X)
[PROOFSTEP]
rw [← comp_tensor_id]
[GOAL]
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| inv F.ε ≫ F.ε ⊗ 𝟙 (F.obj X)
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| F.map (λ_ X).hom
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
⊢ F.map (λ_ X).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X) ≫
      (𝟙 (F.obj (𝟙_ C) ⊗ F.obj X) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X) ≫ F.map (λ_ X).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
⊢ F.map (ρ_ X).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (𝟙_ C)) ≫ (𝟙 (F.obj X) ⊗ inv F.ε) ≫ (ρ_ (F.obj X)).hom
[PROOFSTEP]
simp only [LaxMonoidalFunctor.right_unitality]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
⊢ F.map (ρ_ X).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (𝟙_ C)) ≫
      (𝟙 (F.obj X) ⊗ inv F.ε) ≫
        (𝟙 (F.obj X) ⊗ F.ε) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (𝟙_ C) ≫ F.map (ρ_ X).hom
[PROOFSTEP]
slice_rhs 2 3 =>
  rw [← id_tensor_comp]
  simp
[GOAL]
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| (𝟙 (F.obj X) ⊗ inv F.ε) ≫ (𝟙 (F.obj X) ⊗ F.ε)
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (𝟙_ C)
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| F.map (ρ_ X).hom
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (𝟙_ C))
[PROOFSTEP]
  rw [← id_tensor_comp]
  simp
[GOAL]
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| (𝟙 (F.obj X) ⊗ inv F.ε) ≫ (𝟙 (F.obj X) ⊗ F.ε)
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (𝟙_ C)
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| F.map (ρ_ X).hom
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (𝟙_ C))
[PROOFSTEP]
  rw [← id_tensor_comp]
  simp
[GOAL]
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| (𝟙 (F.obj X) ⊗ inv F.ε) ≫ (𝟙 (F.obj X) ⊗ F.ε)
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (𝟙_ C)
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| F.map (ρ_ X).hom
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (𝟙_ C))
[PROOFSTEP]
rw [← id_tensor_comp]
[GOAL]
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| 𝟙 (F.obj X) ⊗ inv F.ε ≫ F.ε
case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (𝟙_ C)
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| F.map (ρ_ X).hom
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
| inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (𝟙_ C))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
⊢ F.map (ρ_ X).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (𝟙_ C)) ≫
      (𝟙 (F.obj X ⊗ F.obj (𝟙_ C)) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X (𝟙_ C)) ≫ F.map (ρ_ X).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
⊢ (X : C × C) → (Functor.prod F.toFunctor F.toFunctor ⋙ tensor D).obj X ≅ (tensor C ⋙ F.toFunctor).obj X
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X✝ : C × C
⊢ (Functor.prod F.toFunctor F.toFunctor ⋙ tensor D).obj X✝ ≅ (tensor C ⋙ F.toFunctor).obj X✝
[PROOFSTEP]
apply F.μIso
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
⊢ ∀ {X Y : C × C} (f : X ⟶ Y),
    (Functor.prod F.toFunctor F.toFunctor ⋙ tensor D).map f ≫ (μIso F Y.fst Y.snd).hom =
      (μIso F X.fst X.snd).hom ≫ (tensor C ⋙ F.toFunctor).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X✝ Y✝ : C × C
f✝ : X✝ ⟶ Y✝
⊢ (Functor.prod F.toFunctor F.toFunctor ⋙ tensor D).map f✝ ≫ (μIso F Y✝.fst Y✝.snd).hom =
    (μIso F X✝.fst X✝.snd).hom ≫ (tensor C ⋙ F.toFunctor).map f✝
[PROOFSTEP]
apply F.toLaxMonoidalFunctor.μ_natural
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X Y Z : C
f : Y ⟶ Z
⊢ (F.toFunctor ⋙ tensorLeft (F.obj X)).map f ≫ ((fun Y => μIso F X Y) Z).hom =
    ((fun Y => μIso F X Y) Y).hom ≫ (tensorLeft X ⋙ F.toFunctor).map f
[PROOFSTEP]
convert F.μ_natural (𝟙 X) f using 2
[GOAL]
case h.e'_2.h.h.e'_6.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X Y Z : C
f : Y ⟶ Z
e_1✝ :
  ((F.toFunctor ⋙ tensorLeft (F.obj X)).obj Y ⟶ (tensorLeft X ⋙ F.toFunctor).obj Z) =
    (F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Z))
e_3✝ : (F.toFunctor ⋙ tensorLeft (F.obj X)).obj Y = F.obj X ⊗ F.obj Y
e_4✝ : (F.toFunctor ⋙ tensorLeft (F.obj X)).obj Z = F.obj X ⊗ F.obj Z
⊢ (F.toFunctor ⋙ tensorLeft (F.obj X)).map f = F.map (𝟙 X) ⊗ F.map f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X Y Z : C
f : Y ⟶ Z
⊢ (F.toFunctor ⋙ tensorRight (F.obj X)).map f ≫ ((fun Y => μIso F Y X) Z).hom =
    ((fun Y => μIso F Y X) Y).hom ≫ (tensorRight X ⋙ F.toFunctor).map f
[PROOFSTEP]
convert F.μ_natural f (𝟙 X) using 2
[GOAL]
case h.e'_2.h.h.e'_6.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X Y Z : C
f : Y ⟶ Z
e_1✝ :
  ((F.toFunctor ⋙ tensorRight (F.obj X)).obj Y ⟶ (tensorRight X ⋙ F.toFunctor).obj Z) =
    (F.obj Y ⊗ F.obj X ⟶ F.obj (Z ⊗ X))
e_3✝ : (F.toFunctor ⋙ tensorRight (F.obj X)).obj Y = F.obj Y ⊗ F.obj X
e_4✝ : (F.toFunctor ⋙ tensorRight (F.obj X)).obj Z = F.obj Z ⊗ F.obj X
⊢ (F.toFunctor ⋙ tensorRight (F.obj X)).map f = F.map f ⊗ F.map (𝟙 X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
x✝³ x✝² x✝¹ x✝ : C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
⊢ ((Functor.mk src✝.toPrefunctor).map f ⊗ (Functor.mk src✝.toPrefunctor).map g) ≫
      (fun X Y => μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) x✝² x✝ =
    (fun X Y => μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) x✝³ x✝¹ ≫ (Functor.mk src✝.toPrefunctor).map (f ⊗ g)
[PROOFSTEP]
simp only [Functor.comp_map, assoc]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
x✝³ x✝² x✝¹ x✝ : C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
⊢ (G.map (F.map f) ⊗ G.map (F.map g)) ≫ μ G (F.obj x✝²) (F.obj x✝) ≫ G.map (μ F x✝² x✝) =
    μ G (F.obj x✝³) (F.obj x✝¹) ≫ G.map (μ F x✝³ x✝¹) ≫ G.map (F.map (f ⊗ g))
[PROOFSTEP]
rw [← Category.assoc, LaxMonoidalFunctor.μ_natural, Category.assoc, ← map_comp, ← map_comp, ←
  LaxMonoidalFunctor.μ_natural]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
⊢ ((fun X Y => μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) X Y ⊗ 𝟙 ((Functor.mk src✝.toPrefunctor).obj Z)) ≫
      (fun X Y => μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) (X ⊗ Y) Z ≫
        (Functor.mk src✝.toPrefunctor).map (α_ X Y Z).hom =
    (α_ ((Functor.mk src✝.toPrefunctor).obj X) ((Functor.mk src✝.toPrefunctor).obj Y)
          ((Functor.mk src✝.toPrefunctor).obj Z)).hom ≫
      (𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ (fun X Y => μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) Y Z) ≫
        (fun X Y => μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) X (Y ⊗ Z)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
⊢ (μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y) ⊗ 𝟙 (G.obj (F.obj Z))) ≫
      (μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫ G.map (μ F (X ⊗ Y) Z)) ≫ G.map (F.map (α_ X Y Z).hom) =
    (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom ≫
      (𝟙 (G.obj (F.obj X)) ⊗ μ G (F.obj Y) (F.obj Z) ≫ G.map (μ F Y Z)) ≫
        μ G (F.obj X) (F.obj (Y ⊗ Z)) ≫ G.map (μ F X (Y ⊗ Z))
[PROOFSTEP]
rw [id_tensor_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
⊢ (μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y) ⊗ 𝟙 (G.obj (F.obj Z))) ≫
      (μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫ G.map (μ F (X ⊗ Y) Z)) ≫ G.map (F.map (α_ X Y Z).hom) =
    (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom ≫
      ((𝟙 (G.obj (F.obj X)) ⊗ μ G (F.obj Y) (F.obj Z)) ≫ (𝟙 (G.obj (F.obj X)) ⊗ G.map (μ F Y Z))) ≫
        μ G (F.obj X) (F.obj (Y ⊗ Z)) ≫ G.map (μ F X (Y ⊗ Z))
[PROOFSTEP]
slice_rhs 3 4 => rw [← G.toFunctor.map_id, G.μ_natural]
[GOAL]
case a.a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| (𝟙 (G.obj (F.obj X)) ⊗ G.map (μ F Y Z)) ≫ μ G (F.obj X) (F.obj (Y ⊗ Z))
case a.a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (μ F X (Y ⊗ Z))
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom
case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| 𝟙 (G.obj (F.obj X)) ⊗ μ G (F.obj Y) (F.obj Z)
[PROOFSTEP]
rw [← G.toFunctor.map_id, G.μ_natural]
[GOAL]
case a.a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| (𝟙 (G.obj (F.obj X)) ⊗ G.map (μ F Y Z)) ≫ μ G (F.obj X) (F.obj (Y ⊗ Z))
case a.a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (μ F X (Y ⊗ Z))
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom
case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| 𝟙 (G.obj (F.obj X)) ⊗ μ G (F.obj Y) (F.obj Z)
[PROOFSTEP]
rw [← G.toFunctor.map_id, G.μ_natural]
[GOAL]
case a.a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| (𝟙 (G.obj (F.obj X)) ⊗ G.map (μ F Y Z)) ≫ μ G (F.obj X) (F.obj (Y ⊗ Z))
case a.a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (μ F X (Y ⊗ Z))
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom
case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| 𝟙 (G.obj (F.obj X)) ⊗ μ G (F.obj Y) (F.obj Z)
[PROOFSTEP]
rw [← G.toFunctor.map_id, G.μ_natural]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
⊢ (μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y) ⊗ 𝟙 (G.obj (F.obj Z))) ≫
      (μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫ G.map (μ F (X ⊗ Y) Z)) ≫ G.map (F.map (α_ X Y Z).hom) =
    (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom ≫
      (𝟙 (G.obj (F.obj X)) ⊗ μ G (F.obj Y) (F.obj Z)) ≫
        (μ G (F.obj X) (F.obj Y ⊗ F.obj Z) ≫ G.map (𝟙 (F.obj X) ⊗ μ F Y Z)) ≫ G.map (μ F X (Y ⊗ Z))
[PROOFSTEP]
slice_rhs 1 3 => rw [← G.associativity]
[GOAL]
case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom ≫
    (𝟙 (G.obj (F.obj X)) ⊗ μ G (F.obj Y) (F.obj Z)) ≫ μ G (F.obj X) (F.obj Y ⊗ F.obj Z)
case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (𝟙 (F.obj X) ⊗ μ F Y Z)
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (μ F X (Y ⊗ Z))
[PROOFSTEP]
rw [← G.associativity]
[GOAL]
case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom ≫
    (𝟙 (G.obj (F.obj X)) ⊗ μ G (F.obj Y) (F.obj Z)) ≫ μ G (F.obj X) (F.obj Y ⊗ F.obj Z)
case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (𝟙 (F.obj X) ⊗ μ F Y Z)
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (μ F X (Y ⊗ Z))
[PROOFSTEP]
rw [← G.associativity]
[GOAL]
case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom ≫
    (𝟙 (G.obj (F.obj X)) ⊗ μ G (F.obj Y) (F.obj Z)) ≫ μ G (F.obj X) (F.obj Y ⊗ F.obj Z)
case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (𝟙 (F.obj X) ⊗ μ F Y Z)
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (μ F X (Y ⊗ Z))
[PROOFSTEP]
rw [← G.associativity]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
⊢ (μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y) ⊗ 𝟙 (G.obj (F.obj Z))) ≫
      (μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫ G.map (μ F (X ⊗ Y) Z)) ≫ G.map (F.map (α_ X Y Z).hom) =
    (((μ G (F.obj X) (F.obj Y) ⊗ 𝟙 (G.obj (F.obj Z))) ≫
          μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) ≫
        G.map (𝟙 (F.obj X) ⊗ μ F Y Z)) ≫
      G.map (μ F X (Y ⊗ Z))
[PROOFSTEP]
rw [comp_tensor_id]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
⊢ ((μ G (F.obj X) (F.obj Y) ⊗ 𝟙 (G.obj (F.obj Z))) ≫ (G.map (μ F X Y) ⊗ 𝟙 (G.obj (F.obj Z)))) ≫
      (μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫ G.map (μ F (X ⊗ Y) Z)) ≫ G.map (F.map (α_ X Y Z).hom) =
    (((μ G (F.obj X) (F.obj Y) ⊗ 𝟙 (G.obj (F.obj Z))) ≫
          μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) ≫
        G.map (𝟙 (F.obj X) ⊗ μ F Y Z)) ≫
      G.map (μ F X (Y ⊗ Z))
[PROOFSTEP]
slice_lhs 2 3 => rw [← G.toFunctor.map_id, G.μ_natural]
[GOAL]
case a.a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| (G.map (μ F X Y) ⊗ 𝟙 (G.obj (F.obj Z))) ≫ μ G (F.obj (X ⊗ Y)) (F.obj Z)
case a.a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (μ F (X ⊗ Y) Z)
case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (F.map (α_ X Y Z).hom)
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| μ G (F.obj X) (F.obj Y) ⊗ 𝟙 (G.obj (F.obj Z))
[PROOFSTEP]
rw [← G.toFunctor.map_id, G.μ_natural]
[GOAL]
case a.a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| (G.map (μ F X Y) ⊗ 𝟙 (G.obj (F.obj Z))) ≫ μ G (F.obj (X ⊗ Y)) (F.obj Z)
case a.a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (μ F (X ⊗ Y) Z)
case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (F.map (α_ X Y Z).hom)
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| μ G (F.obj X) (F.obj Y) ⊗ 𝟙 (G.obj (F.obj Z))
[PROOFSTEP]
rw [← G.toFunctor.map_id, G.μ_natural]
[GOAL]
case a.a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| (G.map (μ F X Y) ⊗ 𝟙 (G.obj (F.obj Z))) ≫ μ G (F.obj (X ⊗ Y)) (F.obj Z)
case a.a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (μ F (X ⊗ Y) Z)
case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| G.map (F.map (α_ X Y Z).hom)
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
| μ G (F.obj X) (F.obj Y) ⊗ 𝟙 (G.obj (F.obj Z))
[PROOFSTEP]
rw [← G.toFunctor.map_id, G.μ_natural]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X Y Z : C
⊢ (μ G (F.obj X) (F.obj Y) ⊗ 𝟙 (G.obj (F.obj Z))) ≫
      ((μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (μ F X Y ⊗ 𝟙 (F.obj Z))) ≫ G.map (μ F (X ⊗ Y) Z)) ≫
        G.map (F.map (α_ X Y Z).hom) =
    (((μ G (F.obj X) (F.obj Y) ⊗ 𝟙 (G.obj (F.obj Z))) ≫
          μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) ≫
        G.map (𝟙 (F.obj X) ⊗ μ F Y Z)) ≫
      G.map (μ F X (Y ⊗ Z))
[PROOFSTEP]
rw [Category.assoc, Category.assoc, Category.assoc, Category.assoc, Category.assoc, ← G.toFunctor.map_comp, ←
  G.toFunctor.map_comp, ← G.toFunctor.map_comp, ← G.toFunctor.map_comp, F.associativity]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X : C
⊢ (λ_ ((Functor.mk src✝.toPrefunctor).obj X)).hom =
    (G.ε ≫ G.map F.ε ⊗ 𝟙 ((Functor.mk src✝.toPrefunctor).obj X)) ≫
      (fun X Y => μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) (𝟙_ C) X ≫ (Functor.mk src✝.toPrefunctor).map (λ_ X).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X : C
⊢ (λ_ (G.obj (F.obj X))).hom =
    (G.ε ≫ G.map F.ε ⊗ 𝟙 (G.obj (F.obj X))) ≫
      (μ G (F.obj (𝟙_ C)) (F.obj X) ≫ G.map (μ F (𝟙_ C) X)) ≫ G.map (F.map (λ_ X).hom)
[PROOFSTEP]
rw [G.left_unitality, comp_tensor_id, Category.assoc, Category.assoc]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X : C
⊢ (G.ε ⊗ 𝟙 (G.obj (F.obj X))) ≫ μ G (𝟙_ D) (F.obj X) ≫ G.map (λ_ (F.obj X)).hom =
    (G.ε ⊗ 𝟙 (G.obj (F.obj X))) ≫
      (G.map F.ε ⊗ 𝟙 (G.obj (F.obj X))) ≫ μ G (F.obj (𝟙_ C)) (F.obj X) ≫ G.map (μ F (𝟙_ C) X) ≫ G.map (F.map (λ_ X).hom)
[PROOFSTEP]
apply congr_arg
[GOAL]
case h
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X : C
⊢ μ G (𝟙_ D) (F.obj X) ≫ G.map (λ_ (F.obj X)).hom =
    (G.map F.ε ⊗ 𝟙 (G.obj (F.obj X))) ≫ μ G (F.obj (𝟙_ C)) (F.obj X) ≫ G.map (μ F (𝟙_ C) X) ≫ G.map (F.map (λ_ X).hom)
[PROOFSTEP]
rw [F.left_unitality, map_comp, ← NatTrans.id_app, ← Category.assoc, ← LaxMonoidalFunctor.μ_natural, NatTrans.id_app,
  map_id, ← Category.assoc, map_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X : C
⊢ (ρ_ ((Functor.mk src✝.toPrefunctor).obj X)).hom =
    (𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ G.ε ≫ G.map F.ε) ≫
      (fun X Y => μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) X (𝟙_ C) ≫ (Functor.mk src✝.toPrefunctor).map (ρ_ X).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X : C
⊢ (ρ_ (G.obj (F.obj X))).hom =
    (𝟙 (G.obj (F.obj X)) ⊗ G.ε ≫ G.map F.ε) ≫
      (μ G (F.obj X) (F.obj (𝟙_ C)) ≫ G.map (μ F X (𝟙_ C))) ≫ G.map (F.map (ρ_ X).hom)
[PROOFSTEP]
rw [G.right_unitality, id_tensor_comp, Category.assoc, Category.assoc]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X : C
⊢ (𝟙 (G.obj (F.obj X)) ⊗ G.ε) ≫ μ G (F.obj X) (𝟙_ D) ≫ G.map (ρ_ (F.obj X)).hom =
    (𝟙 (G.obj (F.obj X)) ⊗ G.ε) ≫
      (𝟙 (G.obj (F.obj X)) ⊗ G.map F.ε) ≫ μ G (F.obj X) (F.obj (𝟙_ C)) ≫ G.map (μ F X (𝟙_ C)) ≫ G.map (F.map (ρ_ X).hom)
[PROOFSTEP]
apply congr_arg
[GOAL]
case h
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor D E
src✝ : C ⥤ E := F.toFunctor ⋙ G.toFunctor
X : C
⊢ μ G (F.obj X) (𝟙_ D) ≫ G.map (ρ_ (F.obj X)).hom =
    (𝟙 (G.obj (F.obj X)) ⊗ G.map F.ε) ≫ μ G (F.obj X) (F.obj (𝟙_ C)) ≫ G.map (μ F X (𝟙_ C)) ≫ G.map (F.map (ρ_ X).hom)
[PROOFSTEP]
rw [F.right_unitality, map_comp, ← NatTrans.id_app, ← Category.assoc, ← LaxMonoidalFunctor.μ_natural, NatTrans.id_app,
  map_id, ← Category.assoc, map_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor C E
⊢ (prod' F G).ε = (F.ε, G.ε)
[PROOFSTEP]
dsimp [prod']
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor C E
⊢ (F.ε ≫ F.map (𝟙 (𝟙_ C)), G.ε ≫ G.map (𝟙 (𝟙_ C))) = (F.ε, G.ε)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor C E
X Y : C
⊢ μ (prod' F G) X Y = (μ F X Y, μ G X Y)
[PROOFSTEP]
dsimp [prod']
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor C E
X Y : C
⊢ (μ F X Y ≫ F.map (𝟙 (X ⊗ Y)), μ G X Y ≫ G.map (𝟙 (X ⊗ Y))) = (μ F X Y, μ G X Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : MonoidalFunctor C D
G : MonoidalFunctor D E
src✝ : LaxMonoidalFunctor C E := F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor
⊢ IsIso (LaxMonoidalFunctor.mk src✝.toFunctor src✝.ε src✝.μ).ε
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : MonoidalFunctor C D
G : MonoidalFunctor D E
src✝ : LaxMonoidalFunctor C E := F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor
⊢ IsIso (G.ε ≫ G.map F.ε)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : MonoidalFunctor C D
G : MonoidalFunctor D E
src✝ : LaxMonoidalFunctor C E := F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor
⊢ ∀ (X Y : C), IsIso (LaxMonoidalFunctor.μ (LaxMonoidalFunctor.mk src✝.toFunctor src✝.ε src✝.μ) X Y)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : MonoidalFunctor C D
G : MonoidalFunctor D E
src✝ : LaxMonoidalFunctor C E := F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor
⊢ ∀ (X Y : C),
    IsIso
      (LaxMonoidalFunctor.μ G.toLaxMonoidalFunctor (F.obj X) (F.obj Y) ≫
        G.map (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : MonoidalFunctor C D
G : D ⥤ C
h : F.toFunctor ⊣ G
X Y X' Y' : D
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (G.map f ⊗ G.map g) ≫
      (fun X Y =>
          ↑(Adjunction.homEquiv h (G.obj X ⊗ G.obj Y) (X ⊗ Y))
            (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (G.obj Y)) ≫
              (NatTrans.app h.counit X ⊗ NatTrans.app h.counit Y)))
        Y Y' =
    (fun X Y =>
          ↑(Adjunction.homEquiv h (G.obj X ⊗ G.obj Y) (X ⊗ Y))
            (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (G.obj Y)) ≫
              (NatTrans.app h.counit X ⊗ NatTrans.app h.counit Y)))
        X X' ≫
      G.map (f ⊗ g)
[PROOFSTEP]
rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_right, Equiv.apply_eq_iff_eq, assoc, IsIso.eq_inv_comp, ←
  F.toLaxMonoidalFunctor.μ_natural_assoc, IsIso.hom_inv_id_assoc, ← tensor_comp, Adjunction.counit_naturality,
  Adjunction.counit_naturality, tensor_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : MonoidalFunctor C D
G : D ⥤ C
h : F.toFunctor ⊣ G
X Y Z : D
⊢ ((fun X Y =>
            ↑(Adjunction.homEquiv h (G.obj X ⊗ G.obj Y) (X ⊗ Y))
              (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (G.obj Y)) ≫
                (NatTrans.app h.counit X ⊗ NatTrans.app h.counit Y)))
          X Y ⊗
        𝟙 (G.obj Z)) ≫
      (fun X Y =>
            ↑(Adjunction.homEquiv h (G.obj X ⊗ G.obj Y) (X ⊗ Y))
              (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (G.obj Y)) ≫
                (NatTrans.app h.counit X ⊗ NatTrans.app h.counit Y)))
          (X ⊗ Y) Z ≫
        G.map (α_ X Y Z).hom =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      (𝟙 (G.obj X) ⊗
          (fun X Y =>
              ↑(Adjunction.homEquiv h (G.obj X ⊗ G.obj Y) (X ⊗ Y))
                (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (G.obj Y)) ≫
                  (NatTrans.app h.counit X ⊗ NatTrans.app h.counit Y)))
            Y Z) ≫
        (fun X Y =>
            ↑(Adjunction.homEquiv h (G.obj X ⊗ G.obj Y) (X ⊗ Y))
              (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (G.obj Y)) ≫
                (NatTrans.app h.counit X ⊗ NatTrans.app h.counit Y)))
          X (Y ⊗ Z)
[PROOFSTEP]
dsimp only
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : MonoidalFunctor C D
G : D ⥤ C
h : F.toFunctor ⊣ G
X Y Z : D
⊢ (↑(Adjunction.homEquiv h (G.obj X ⊗ G.obj Y) (X ⊗ Y))
          (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (G.obj Y)) ≫
            (NatTrans.app h.counit X ⊗ NatTrans.app h.counit Y)) ⊗
        𝟙 (G.obj Z)) ≫
      ↑(Adjunction.homEquiv h (G.obj (X ⊗ Y) ⊗ G.obj Z) ((X ⊗ Y) ⊗ Z))
          (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj (X ⊗ Y)) (G.obj Z)) ≫
            (NatTrans.app h.counit (X ⊗ Y) ⊗ NatTrans.app h.counit Z)) ≫
        G.map (α_ X Y Z).hom =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      (𝟙 (G.obj X) ⊗
          ↑(Adjunction.homEquiv h (G.obj Y ⊗ G.obj Z) (Y ⊗ Z))
            (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj Y) (G.obj Z)) ≫
              (NatTrans.app h.counit Y ⊗ NatTrans.app h.counit Z))) ≫
        ↑(Adjunction.homEquiv h (G.obj X ⊗ G.obj (Y ⊗ Z)) (X ⊗ Y ⊗ Z))
          (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (G.obj (Y ⊗ Z))) ≫
            (NatTrans.app h.counit X ⊗ NatTrans.app h.counit (Y ⊗ Z)))
[PROOFSTEP]
rw [← h.homEquiv_naturality_right, ← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, ←
  h.homEquiv_naturality_left, Equiv.apply_eq_iff_eq, ←
  cancel_epi (F.toLaxMonoidalFunctor.μ (G.obj X ⊗ G.obj Y) (G.obj Z)), ←
  cancel_epi (F.toLaxMonoidalFunctor.μ (G.obj X) (G.obj Y) ⊗ 𝟙 (F.obj (G.obj Z))),
  F.toLaxMonoidalFunctor.associativity_assoc (G.obj X) (G.obj Y) (G.obj Z), ← F.toLaxMonoidalFunctor.μ_natural_assoc,
  assoc, IsIso.hom_inv_id_assoc, ← F.toLaxMonoidalFunctor.μ_natural_assoc, IsIso.hom_inv_id_assoc, ← tensor_comp, ←
  tensor_comp, id_comp, Functor.map_id, Functor.map_id, id_comp, ← tensor_comp_assoc, ← tensor_comp_assoc, id_comp,
  id_comp, h.homEquiv_unit, h.homEquiv_unit, Functor.map_comp, assoc, assoc, h.counit_naturality,
  h.left_triangle_components_assoc, Functor.map_comp, assoc, h.counit_naturality, h.left_triangle_components_assoc]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : MonoidalFunctor C D
G : D ⥤ C
h : F.toFunctor ⊣ G
X Y Z : D
⊢ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (G.obj Y) ≫
          inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (G.obj Y)) ≫
            (NatTrans.app h.counit X ⊗ NatTrans.app h.counit Y) ⊗
        NatTrans.app h.counit Z) ≫
      (α_ X Y Z).hom =
    (α_ (F.obj (G.obj X)) (F.obj (G.obj Y)) (F.obj (G.obj Z))).hom ≫
      (NatTrans.app h.counit X ⊗
        LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj Y) (G.obj Z) ≫
          inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj Y) (G.obj Z)) ≫
            (NatTrans.app h.counit Y ⊗ NatTrans.app h.counit Z))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : MonoidalFunctor C D
G : D ⥤ C
h : F.toFunctor ⊣ G
X : D
⊢ (λ_ (G.obj X)).hom =
    (↑(Adjunction.homEquiv h (𝟙_ C) (𝟙_ D)) (inv F.ε) ⊗ 𝟙 (G.obj X)) ≫
      (fun X Y =>
            ↑(Adjunction.homEquiv h (G.obj X ⊗ G.obj Y) (X ⊗ Y))
              (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (G.obj Y)) ≫
                (NatTrans.app h.counit X ⊗ NatTrans.app h.counit Y)))
          (𝟙_ D) X ≫
        G.map (λ_ X).hom
[PROOFSTEP]
rw [← h.homEquiv_naturality_right, ← h.homEquiv_naturality_left, ← Equiv.symm_apply_eq, h.homEquiv_counit,
  F.map_leftUnitor, h.homEquiv_unit, assoc, assoc, assoc, F.map_tensor, assoc, assoc, IsIso.hom_inv_id_assoc, ←
  tensor_comp_assoc, Functor.map_id, id_comp, Functor.map_comp, assoc, h.counit_naturality,
  h.left_triangle_components_assoc, ← leftUnitor_naturality, ← tensor_comp_assoc, id_comp, comp_id]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : MonoidalFunctor C D
G : D ⥤ C
h : F.toFunctor ⊣ G
X : D
⊢ inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) (G.obj X)) ≫
      (inv F.ε ⊗ NatTrans.app h.counit X) ≫ (λ_ ((𝟭 D).obj X)).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) (G.obj X)) ≫
      (inv F.ε ⊗ NatTrans.app h.counit X) ≫ (λ_ X).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : MonoidalFunctor C D
G : D ⥤ C
h : F.toFunctor ⊣ G
X : D
⊢ (ρ_ (G.obj X)).hom =
    (𝟙 (G.obj X) ⊗ ↑(Adjunction.homEquiv h (𝟙_ C) (𝟙_ D)) (inv F.ε)) ≫
      (fun X Y =>
            ↑(Adjunction.homEquiv h (G.obj X ⊗ G.obj Y) (X ⊗ Y))
              (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (G.obj Y)) ≫
                (NatTrans.app h.counit X ⊗ NatTrans.app h.counit Y)))
          X (𝟙_ D) ≫
        G.map (ρ_ X).hom
[PROOFSTEP]
rw [← h.homEquiv_naturality_right, ← h.homEquiv_naturality_left, ← Equiv.symm_apply_eq, h.homEquiv_counit,
  F.map_rightUnitor, assoc, assoc, ← rightUnitor_naturality, ← tensor_comp_assoc, comp_id, id_comp, h.homEquiv_unit,
  F.map_tensor, assoc, assoc, assoc, IsIso.hom_inv_id_assoc, Functor.map_comp, Functor.map_id, ← tensor_comp_assoc,
  assoc, h.counit_naturality, h.left_triangle_components_assoc, id_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F : MonoidalFunctor C D
G : D ⥤ C
h : F.toFunctor ⊣ G
X : D
⊢ inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (𝟙_ C)) ≫
      (NatTrans.app h.counit X ⊗ inv F.ε) ≫ (ρ_ ((𝟭 D).obj X)).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (G.obj X) (𝟙_ C)) ≫
      (NatTrans.app h.counit X ⊗ inv F.ε) ≫ (ρ_ X).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
⊢ IsIso (monoidalAdjoint F (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1))).ε
[PROOFSTEP]
dsimp [Equivalence.toAdjunction]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
⊢ IsIso
    (NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) (𝟙_ C) ≫
      (Functor.inv F.toLaxMonoidalFunctor.1).map (inv F.ε))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
X Y : D
⊢ IsIso
    (LaxMonoidalFunctor.μ (monoidalAdjoint F (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1))) X Y)
[PROOFSTEP]
dsimp [Equivalence.toAdjunction]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
X Y : D
⊢ IsIso
    (NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1))
        ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y) ≫
      (Functor.inv F.toLaxMonoidalFunctor.1).map
        (inv
            (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
              ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
          (NatTrans.app (Equivalence.counit (asEquivalence F.toLaxMonoidalFunctor.1)) X ⊗
            NatTrans.app (Equivalence.counit (asEquivalence F.toLaxMonoidalFunctor.1)) Y)))
[PROOFSTEP]
infer_instance
