no goals
C : Type u
inst✝ : Category C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ F.map f.f ≫ ↑(Adjunction.homEquiv adj V₂.V V₂.V).symm V₂.str = ↑(Adjunction.homEquiv adj V₁.V V₁.V).symm V₁.str ≫ f.f
rw [← Adjunction.homEquiv_naturality_left_symm, ← Adjunction.homEquiv_naturality_right_symm,
  f.h]