-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
L : Functor.{v₁, v, u₁, u} D C
R : Functor.{v, v₁, u, u₁} C D
h : L ⊣ R
X Y : D
f g : X ⟶ Y
rw :
  Eq.{v₁ + 1} (α := X ⟶ R.obj (coeq (L.map f) (L.map g)))
    (((h.homEquiv X (coeq (L.map f) (L.map g)) :
            Equiv.{v + 1, v₁ + 1} (L.obj X ⟶ coeq (L.map f) (L.map g)) (X ⟶ R.obj (coeq (L.map f) (L.map g)))) :
          (a : L.obj X ⟶ coeq (L.map f) (L.map g)) → X ⟶ R.obj (coeq (L.map f) (L.map g)))
        (L.map f ≫ coeqHom (L.map f) (L.map g)) :
      X ⟶ R.obj (coeq (L.map f) (L.map g)))
    (g ≫
        ((h.homEquiv Y (coeq (L.map f) (L.map g)) :
              Equiv.{v + 1, v₁ + 1} (L.obj Y ⟶ coeq (L.map f) (L.map g)) (Y ⟶ R.obj (coeq (L.map f) (L.map g)))) :
            (a : L.obj Y ⟶ coeq (L.map f) (L.map g)) → Y ⟶ R.obj (coeq (L.map f) (L.map g)))
          (coeqHom (L.map f) (L.map g)) :
      X ⟶ R.obj (coeq (L.map f) (L.map g)))
rw₁ :
  Eq.{v₁ + 1} (α := X ⟶ R.obj (coeq (L.map f) (L.map g)))
    (((h.homEquiv X (coeq (L.map f) (L.map g)) :
            Equiv.{v + 1, v₁ + 1} (L.obj X ⟶ coeq (L.map f) (L.map g)) (X ⟶ R.obj (coeq (L.map f) (L.map g)))) :
          (a : L.obj X ⟶ coeq (L.map f) (L.map g)) → X ⟶ R.obj (coeq (L.map f) (L.map g)))
        (L.map f ≫ coeqHom (L.map f) (L.map g)) :
      X ⟶ R.obj (coeq (L.map f) (L.map g)))
    (((h.homEquiv X (coeq (L.map f) (L.map g)) :
            Equiv.{v + 1, v₁ + 1} (L.obj X ⟶ coeq (L.map f) (L.map g)) (X ⟶ R.obj (coeq (L.map f) (L.map g)))) :
          (a : L.obj X ⟶ coeq (L.map f) (L.map g)) → X ⟶ R.obj (coeq (L.map f) (L.map g)))
        (L.map g ≫ coeqHom (L.map f) (L.map g)) :
      X ⟶ R.obj (coeq (L.map f) (L.map g)))
rw₂ rw₃ :
  Eq.{v₁ + 1} (α := X ⟶ R.obj (coeq (L.map f) (L.map g)))
    (((h.homEquiv X (coeq (L.map f) (L.map g)) :
            Equiv.{v + 1, v₁ + 1} (L.obj X ⟶ coeq (L.map f) (L.map g)) (X ⟶ R.obj (coeq (L.map f) (L.map g)))) :
          (a : L.obj X ⟶ coeq (L.map f) (L.map g)) → X ⟶ R.obj (coeq (L.map f) (L.map g)))
        (L.map g ≫ coeqHom (L.map f) (L.map g)) :
      X ⟶ R.obj (coeq (L.map f) (L.map g)))
    (((h.homEquiv X (coeq (L.map f) (L.map g)) :
            Equiv.{v + 1, v₁ + 1} (L.obj X ⟶ coeq (L.map f) (L.map g)) (X ⟶ R.obj (coeq (L.map f) (L.map g)))) :
          (a : L.obj X ⟶ coeq (L.map f) (L.map g)) → X ⟶ R.obj (coeq (L.map f) (L.map g)))
        (L.map g ≫ coeqHom (L.map f) (L.map g)) :
      X ⟶ R.obj (coeq (L.map f) (L.map g)))
⊢ Eq (α := X ⟶ R.obj (coeq (L.map f) (L.map g)))
    (f ≫
      ((h.homEquiv Y (coeq (L.map f) (L.map g)) :
            Equiv.{v + 1, v₁ + 1} (L.obj Y ⟶ coeq (L.map f) (L.map g)) (Y ⟶ R.obj (coeq (L.map f) (L.map g)))) :
          (a : L.obj Y ⟶ coeq (L.map f) (L.map g)) → Y ⟶ R.obj (coeq (L.map f) (L.map g)))
        (coeqHom (L.map f) (L.map g)))
    (g ≫
      ((h.homEquiv Y (coeq (L.map f) (L.map g)) :
            Equiv.{v + 1, v₁ + 1} (L.obj Y ⟶ coeq (L.map f) (L.map g)) (Y ⟶ R.obj (coeq (L.map f) (L.map g)))) :
          (a : L.obj Y ⟶ coeq (L.map f) (L.map g)) → Y ⟶ R.obj (coeq (L.map f) (L.map g)))
        (coeqHom (L.map f) (L.map g)))

Tactic:
rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, coeq_condition]

Premises used: CategoryTheory.IsFiltered.coeq_condition, CategoryTheory.Adjunction.homEquiv_naturality_left