-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
L : Functor.{v, v₁, u, u₁} C D
R : Functor.{v₁, v, u₁, u} D C
h : L ⊣ R
X Y : D
f g : X ⟶ Y
rw :
  Eq.{v₁ + 1} (α := L.obj (eq (R.map f) (R.map g)) ⟶ Y)
    (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) Y) :
            Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj Y) (L.obj (eq (R.map f) (R.map g)) ⟶ Y)) :
          (a : eq (R.map f) (R.map g) ⟶ R.obj Y) → L.obj (eq (R.map f) (R.map g)) ⟶ Y)
        (eqHom (R.map f) (R.map g) ≫ R.map f) :
      L.obj (eq (R.map f) (R.map g)) ⟶ Y)
    (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) X) :
              Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj X) (L.obj (eq (R.map f) (R.map g)) ⟶ X)) :
            (a : eq (R.map f) (R.map g) ⟶ R.obj X) → L.obj (eq (R.map f) (R.map g)) ⟶ X)
          (eqHom (R.map f) (R.map g)) ≫
        g :
      L.obj (eq (R.map f) (R.map g)) ⟶ Y)
rw₁ :
  Eq.{v₁ + 1} (α := L.obj (eq (R.map f) (R.map g)) ⟶ Y)
    (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) Y) :
            Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj Y) (L.obj (eq (R.map f) (R.map g)) ⟶ Y)) :
          (a : eq (R.map f) (R.map g) ⟶ R.obj Y) → L.obj (eq (R.map f) (R.map g)) ⟶ Y)
        (eqHom (R.map f) (R.map g) ≫ R.map f) :
      L.obj (eq (R.map f) (R.map g)) ⟶ Y)
    (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) Y) :
            Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj Y) (L.obj (eq (R.map f) (R.map g)) ⟶ Y)) :
          (a : eq (R.map f) (R.map g) ⟶ R.obj Y) → L.obj (eq (R.map f) (R.map g)) ⟶ Y)
        (eqHom (R.map f) (R.map g) ≫ R.map g) :
      L.obj (eq (R.map f) (R.map g)) ⟶ Y)
⊢ Eq.{v₁ + 1} (α := L.obj (eq (R.map f) (R.map g)) ⟶ Y)
    (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) X) :
              Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj X) (L.obj (eq (R.map f) (R.map g)) ⟶ X)) :
            (a : eq (R.map f) (R.map g) ⟶ R.obj X) → L.obj (eq (R.map f) (R.map g)) ⟶ X)
          (eqHom (R.map f) (R.map g)) ≫
        f :
      L.obj (eq (R.map f) (R.map g)) ⟶ Y)
    (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) X) :
              Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj X) (L.obj (eq (R.map f) (R.map g)) ⟶ X)) :
            (a : eq (R.map f) (R.map g) ⟶ R.obj X) → L.obj (eq (R.map f) (R.map g)) ⟶ X)
          (eqHom (R.map f) (R.map g)) ≫
        g :
      L.obj (eq (R.map f) (R.map g)) ⟶ Y)
have rw₂ : Eq.{v₁ + 1} (α := L.obj (eq (R.map f) (R.map g)) ⟶ Y)
  (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) Y) :
          Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj Y) (L.obj (eq (R.map f) (R.map g)) ⟶ Y)) :
        (a : eq (R.map f) (R.map g) ⟶ R.obj Y) → L.obj (eq (R.map f) (R.map g)) ⟶ Y)
      (eqHom (R.map f) (R.map g) ≫ R.map g) :
    L.obj (eq (R.map f) (R.map g)) ⟶ Y)
  (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) Y) :
          Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj Y) (L.obj (eq (R.map f) (R.map g)) ⟶ Y)) :
        (a : eq (R.map f) (R.map g) ⟶ R.obj Y) → L.obj (eq (R.map f) (R.map g)) ⟶ Y)
      (eqHom (R.map f) (R.map g) ≫ R.map g) :
    L.obj (eq (R.map f) (R.map g)) ⟶ Y)
Tactic: rw [← h.homEquiv_naturality_right_symm, ← h.homEquiv_naturality_right_symm, eq_condition]