no goals
C : Type u
inst✝⁴ : Category C
inst✝³ : IsCofiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
J : Type w
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
D : Type u₁
inst✝ : Category D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ ↑(Adjunction.homEquiv h (eq (R.map f) (R.map g)) X).symm (eqHom (R.map f) (R.map g)) ≫ f =
    ↑(Adjunction.homEquiv h (eq (R.map f) (R.map g)) X).symm (eqHom (R.map f) (R.map g)) ≫ g
rw [← h.homEquiv_naturality_right_symm, ← h.homEquiv_naturality_right_symm, eq_condition]