-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
X : Cᵒᵖ
t : (obj (cones J C) (K ⋙ G)).obj X
j j' : J
f : j ⟶ j'
erw :
  Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
    (map (unop (obj (Functor.op (const J)) (F.op.obj X))) f ≫
      ((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
          (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
        (t.app j'))
    (((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
          Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
        (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
      (t.app j ≫ G.map (K.map f)))
erw₁ :
  Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
    (map (unop (obj (Functor.op (const J)) (F.op.obj X))) f ≫
      ((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
          (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
        (t.app j'))
    (((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
          Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
        (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
      (map (unop (obj (Functor.op (const J)) X)) f ≫ t.app j'))
erw₂ :
  Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
    (((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
          (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
        (t.app j') :
      F.obj (unop X) ⟶ K.obj j')
    (((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
          (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
        (map (unop (obj (Functor.op (const J)) X)) f ≫ t.app j') :
      F.obj (unop X) ⟶ K.obj j')
⊢ Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
    (map (unop (obj (Functor.op (const J)) (F.op.obj X))) f ≫
      ((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
          (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
        (t.app j'))
    (((Equiv.symm (adj.homEquiv (unop X) (K.obj j)) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j)) (F.obj (unop X) ⟶ K.obj j)) :
          (a : unop X ⟶ G.obj (K.obj j)) → F.obj (unop X) ⟶ K.obj j)
        (t.app j) ≫
      K.map f)
have erw₃ : Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
  (((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
          Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
        (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
      (t.app j') :
    F.obj (unop X) ⟶ K.obj j')
  (((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
          Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
        (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
      (t.app j') :
    F.obj (unop X) ⟶ K.obj j')
Tactic: erw [← adj.homEquiv_naturality_right_symm, ← t.naturality, Category.id_comp, Category.id_comp]