-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, coeq_condition]