no goals
C : Type u
inst✝ : Category C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ ↑(Adjunction.homEquiv adj A₁.a A₁.a) A₁.str ≫ G.map f.f = f.f ≫ ↑(Adjunction.homEquiv adj A₂.a A₂.a) A₂.str
rw [← Adjunction.homEquiv_naturality_right, ← Adjunction.homEquiv_naturality_left, f.h]