C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv ((F.obj m₃).map ((MonoidalFunctor.μIso F m₁ m₂).inv.app X)) =
    inv
      ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫
        (F.map (α_ m₁ m₂ m₃).hom).app X ≫
          (MonoidalFunctor.μIso F m₁ (m₂ ⊗ m₃)).inv.app X ≫ (MonoidalFunctor.μIso F m₂ m₃).inv.app ((F.obj m₁).obj X))
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.obj m₃).map ((MonoidalFunctor.μIso F m₁ m₂).inv.app X) =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫
      (F.map (α_ m₁ m₂ m₃).hom).app X ≫
        (MonoidalFunctor.μIso F m₁ (m₂ ⊗ m₃)).inv.app X ≫ (MonoidalFunctor.μIso F m₂ m₃).inv.app ((F.obj m₁).obj X)
rw [← IsIso.inv_eq_inv]
case h.e'_2
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv ((F.obj m₃).map ((MonoidalFunctor.μIso F m₁ m₂).inv.app X)) =
    (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X)

case h.e'_3
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv
      ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫
        (F.map (α_ m₁ m₂ m₃).hom).app X ≫
          (MonoidalFunctor.μIso F m₁ (m₂ ⊗ m₃)).inv.app X ≫ (MonoidalFunctor.μIso F m₂ m₃).inv.app ((F.obj m₁).obj X)) =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X ≫
        (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv.app X
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv ((F.obj m₃).map ((MonoidalFunctor.μIso F m₁ m₂).inv.app X)) =
    inv
      ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫
        (F.map (α_ m₁ m₂ m₃).hom).app X ≫
          (MonoidalFunctor.μIso F m₁ (m₂ ⊗ m₃)).inv.app X ≫ (MonoidalFunctor.μIso F m₂ m₃).inv.app ((F.obj m₁).obj X))
convert obj_μ_app F m₁ m₂ m₃ X using 1
case h.e'_2
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.obj m₃).map ((MonoidalFunctor.μIso F m₁ m₂).inv.app X) ≫
      (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) =
    𝟙 ((F.obj m₃).obj ((F.obj (m₁ ⊗ m₂)).obj X))
case h.e'_2
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv ((F.obj m₃).map ((MonoidalFunctor.μIso F m₁ m₂).inv.app X)) =
    (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X)
refine' IsIso.inv_eq_of_hom_inv_id _
case h.e'_2
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.obj m₃).map
      ((MonoidalFunctor.μIso F m₁ m₂).inv.app X ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) =
    𝟙 ((F.obj m₃).obj ((F.obj (m₁ ⊗ m₂)).obj X))
case h.e'_2
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.obj m₃).map ((MonoidalFunctor.μIso F m₁ m₂).inv.app X) ≫
      (F.obj m₃).map ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) =
    𝟙 ((F.obj m₃).obj ((F.obj (m₁ ⊗ m₂)).obj X))
rw [← Functor.map_comp]
no goals
case h.e'_2
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.obj m₃).map
      ((MonoidalFunctor.μIso F m₁ m₂).inv.app X ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂).app X) =
    𝟙 ((F.obj m₃).obj ((F.obj (m₁ ⊗ m₂)).obj X))
simp
case h.e'_3
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X ≫
        inv ((F.map (α_ m₁ m₂ m₃).hom).app X) ≫ inv ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X) =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X ≫
        (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv.app X
case h.e'_3
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv
      ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫
        (F.map (α_ m₁ m₂ m₃).hom).app X ≫
          (MonoidalFunctor.μIso F m₁ (m₂ ⊗ m₃)).inv.app X ≫ (MonoidalFunctor.μIso F m₂ m₃).inv.app ((F.obj m₁).obj X)) =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X ≫
        (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv.app X
simp only [MonoidalFunctor.μIso_hom, Category.assoc, NatIso.inv_inv_app, IsIso.inv_comp]
case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv ((F.map (α_ m₁ m₂ m₃).hom).app X) = (F.map (α_ m₁ m₂ m₃).inv).app X

case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X) =
    (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv.app X
case h.e'_3
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X ≫
        inv ((F.map (α_ m₁ m₂ m₃).hom).app X) ≫ inv ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X) =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃).app ((F.obj m₁).obj X) ≫
      (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)).app X ≫
        (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv.app X
congr
case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.map (α_ m₁ m₂ m₃).hom).app X ≫ (F.map (α_ m₁ m₂ m₃).inv).app X = 𝟙 ((F.obj ((m₁ ⊗ m₂) ⊗ m₃)).obj X)
case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv ((F.map (α_ m₁ m₂ m₃).hom).app X) = (F.map (α_ m₁ m₂ m₃).inv).app X
refine' IsIso.inv_eq_of_hom_inv_id _
no goals
case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.map (α_ m₁ m₂ m₃).hom).app X ≫ (F.map (α_ m₁ m₂ m₃).inv).app X = 𝟙 ((F.obj ((m₁ ⊗ m₂) ⊗ m₃)).obj X)
simp
case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫ (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv.app X =
    𝟙 ((F.obj m₃).obj ((F.obj (m₁ ⊗ m₂)).obj X))
case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X) =
    (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv.app X
refine' IsIso.inv_eq_of_hom_inv_id _
case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ 𝟙 ((F.obj (m₁ ⊗ m₂) ⊗ F.obj m₃).obj X) = 𝟙 ((F.obj m₃).obj ((F.obj (m₁ ⊗ m₂)).obj X))
case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃).app X ≫ (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv.app X =
    𝟙 ((F.obj m₃).obj ((F.obj (m₁ ⊗ m₂)).obj X))
simp
no goals
case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ 𝟙 ((F.obj (m₁ ⊗ m₂) ⊗ F.obj m₃).obj X) = 𝟙 ((F.obj m₃).obj ((F.obj (m₁ ⊗ m₂)).obj X))
rfl