[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : ((cocones J D).obj (op (K ⋙ F))).obj Y
j j' : J
f : j ⟶ j'
⊢ (op (op K).unop).unop.map f ≫ (fun j => ↑(homEquiv adj (K.obj j) Y) (NatTrans.app t j)) j' =
    (fun j => ↑(homEquiv adj (K.obj j) Y) (NatTrans.app t j)) j ≫ ((const J).obj (G.obj Y)).map f
[PROOFSTEP]
erw [← adj.homEquiv_naturality_left, t.naturality]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : ((cocones J D).obj (op (K ⋙ F))).obj Y
j j' : J
f : j ⟶ j'
⊢ ↑(homEquiv adj ((op (op K).unop).unop.obj j) Y) (NatTrans.app t j ≫ ((const J).obj Y).map f) =
    (fun j => ↑(homEquiv adj (K.obj j) Y) (NatTrans.app t j)) j ≫ ((const J).obj (G.obj Y)).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : ((cocones J D).obj (op (K ⋙ F))).obj Y
j j' : J
f : j ⟶ j'
⊢ ↑(homEquiv adj (K.obj j) Y) (NatTrans.app t j ≫ 𝟙 Y) = ↑(homEquiv adj (K.obj j) Y) (NatTrans.app t j) ≫ 𝟙 (G.obj Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : (G ⋙ (cocones J C).obj (op K)).obj Y
j j' : J
f : j ⟶ j'
⊢ (op (op (K ⋙ F)).unop).unop.map f ≫ (fun j => ↑(homEquiv adj (K.obj j) Y).symm (NatTrans.app t j)) j' =
    (fun j => ↑(homEquiv adj (K.obj j) Y).symm (NatTrans.app t j)) j ≫ ((const J).obj Y).map f
[PROOFSTEP]
erw [← adj.homEquiv_naturality_left_symm, ← adj.homEquiv_naturality_right_symm, t.naturality]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : (G ⋙ (cocones J C).obj (op K)).obj Y
j j' : J
f : j ⟶ j'
⊢ ↑(homEquiv adj (K.obj j) (((const J).obj Y).obj j')).symm (NatTrans.app t j ≫ ((const J).obj (G.obj Y)).map f) =
    ↑(homEquiv adj (K.obj j) (((const J).obj Y).obj j')).symm (NatTrans.app t j ≫ G.map (((const J).obj Y).map f))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : (G ⋙ (cocones J C).obj (op K)).obj Y
j j' : J
f : j ⟶ j'
⊢ ↑(homEquiv adj (K.obj j) Y).symm (NatTrans.app t j ≫ 𝟙 (G.obj Y)) =
    ↑(homEquiv adj (K.obj j) Y).symm (NatTrans.app t j ≫ G.map (𝟙 Y))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : (F.op ⋙ (cones J D).obj K).obj X
j j' : J
f : j ⟶ j'
⊢ ((const J).op.obj X).unop.map f ≫ (fun j => ↑(homEquiv adj X.unop (K.obj j)) (NatTrans.app t j)) j' =
    (fun j => ↑(homEquiv adj X.unop (K.obj j)) (NatTrans.app t j)) j ≫ (K ⋙ G).map f
[PROOFSTEP]
erw [← adj.homEquiv_naturality_right, ← t.naturality, Category.id_comp, Category.id_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : (F.op ⋙ (cones J D).obj K).obj X
j j' : J
f : j ⟶ j'
⊢ (fun j => ↑(homEquiv adj X.unop (K.obj j)) (NatTrans.app t j)) j' =
    ↑(homEquiv adj (((const J).op.obj X).unop.obj j) (K.obj j')) (NatTrans.app t j')
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : ((cones J C).obj (K ⋙ G)).obj X
j j' : J
f : j ⟶ j'
⊢ ((const J).op.obj (F.op.obj X)).unop.map f ≫ (fun j => ↑(homEquiv adj X.unop (K.obj j)).symm (NatTrans.app t j)) j' =
    (fun j => ↑(homEquiv adj X.unop (K.obj j)).symm (NatTrans.app t j)) j ≫ K.map f
[PROOFSTEP]
erw [← adj.homEquiv_naturality_right_symm, ← t.naturality, Category.id_comp, Category.id_comp]
