no goals
C : Type u
inst✝⁴ : Category C
inst✝³ : IsFiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
J : Type v
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
D : Type u₁
inst✝ : Category D
L : D ⥤ C
R : C ⥤ D
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ f ≫
      ↑(Adjunction.homEquiv h Y (coeq (?m.33962 h X Y f g) (?m.33963 h X Y f g)))
        (coeqHom (?m.33962 h X Y f g) (?m.33963 h X Y f g)) =
    g ≫
      ↑(Adjunction.homEquiv h Y (coeq (?m.33962 h X Y f g) (?m.33963 h X Y f g)))
        (coeqHom (?m.33962 h X Y f g) (?m.33963 h X Y f g))
rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, coeq_condition]