[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.4486, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
⊢ ∀ ⦃X Y : D⦄ (f : X ⟶ Y),
    ((𝟭 (D ⥤ C)).obj G).map f ≫ (fun X => NatTrans.app (ihom.coev (F.obj X)) (G.obj X)) Y =
      (fun X => NatTrans.app (ihom.coev (F.obj X)) (G.obj X)) X ≫ ((tensorLeft F ⋙ closedIhom F).obj G).map f
[PROOFSTEP]
intro X Y f
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.4486, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ ((𝟭 (D ⥤ C)).obj G).map f ≫ (fun X => NatTrans.app (ihom.coev (F.obj X)) (G.obj X)) Y =
    (fun X => NatTrans.app (ihom.coev (F.obj X)) (G.obj X)) X ≫ ((tensorLeft F ⋙ closedIhom F).obj G).map f
[PROOFSTEP]
dsimp
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.4486, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ NatTrans.app (ihom.coev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.coev (F.obj X)) (G.obj X) ≫ ((closedIhom F).obj (F ⊗ G)).map f
[PROOFSTEP]
simp only [ihom.coev_naturality, closedIhom_obj_map, Monoidal.tensorObj_map]
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.4486, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ (ihom (F.obj Y)).map (𝟙 (F.obj Y) ⊗ G.map f) =
    NatTrans.app (ihom.coev (F.obj X)) (G.obj X) ≫
      NatTrans.app (pre (CategoryTheory.inv (F.map f))) ((F ⊗ G).obj X) ≫ (ihom (F.obj Y)).map (F.map f ⊗ G.map f)
[PROOFSTEP]
dsimp
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.4486, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ (ihom (F.obj Y)).map (𝟙 (F.obj Y) ⊗ G.map f) =
    NatTrans.app (ihom.coev (F.obj X)) (G.obj X) ≫
      NatTrans.app (pre (CategoryTheory.inv (F.map f))) (F.obj X ⊗ G.obj X) ≫ (ihom (F.obj Y)).map (F.map f ⊗ G.map f)
[PROOFSTEP]
rw [coev_app_comp_pre_app_assoc, ← Functor.map_comp]
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.4486, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ (ihom (F.obj Y)).map (𝟙 (F.obj Y) ⊗ G.map f) =
    NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫
      (ihom (F.obj Y)).map ((CategoryTheory.inv (F.map f) ⊗ 𝟙 (G.obj X)) ≫ (F.map f ⊗ G.map f))
[PROOFSTEP]
simp
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.13597, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
⊢ ∀ ⦃X Y : D⦄ (f : X ⟶ Y),
    ((closedIhom F ⋙ tensorLeft F).obj G).map f ≫ (fun X => NatTrans.app (ihom.ev (F.obj X)) (G.obj X)) Y =
      (fun X => NatTrans.app (ihom.ev (F.obj X)) (G.obj X)) X ≫ ((𝟭 (D ⥤ C)).obj G).map f
[PROOFSTEP]
intro X Y f
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.13597, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ ((closedIhom F ⋙ tensorLeft F).obj G).map f ≫ (fun X => NatTrans.app (ihom.ev (F.obj X)) (G.obj X)) Y =
    (fun X => NatTrans.app (ihom.ev (F.obj X)) (G.obj X)) X ≫ ((𝟭 (D ⥤ C)).obj G).map f
[PROOFSTEP]
dsimp
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.13597, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (F.map f ⊗ ((closedIhom F).obj G).map f) ≫ NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f
[PROOFSTEP]
simp only [closedIhom_obj_map, pre_comm_ihom_map]
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.13597, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (F.map f ⊗ (ihom (F.obj X)).map (G.map f) ≫ NatTrans.app (pre (CategoryTheory.inv (F.map f))) (G.obj Y)) ≫
      NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f
[PROOFSTEP]
rw [← tensor_id_comp_id_tensor, id_tensor_comp]
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.13597, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ ((F.map f ⊗ 𝟙 ((ihom (F.obj X)).obj (G.obj X))) ≫
        (𝟙 (F.obj Y) ⊗ (ihom (F.obj X)).map (G.map f)) ≫
          (𝟙 (F.obj Y) ⊗ NatTrans.app (pre (CategoryTheory.inv (F.map f))) (G.obj Y))) ≫
      NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f
[PROOFSTEP]
simp
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.29801, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
⊢ (X : D ⥤ C) → Closed X
[PROOFSTEP]
infer_instance
