-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X Y : C
f : X ⟶ Y
⊢ (F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).map f ≫
      Iso.hom
        ((fun (X : C) ↦
            (Functor.leftKanExtensionUnique (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
                (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X)
                (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
                (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X)) :
              Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X) ≅
                Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)))
          Y) =
    Iso.hom
        ((fun (X : C) ↦
            (Functor.leftKanExtensionUnique (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
                (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X)
                (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
                (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X)) :
              Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X) ≅
                Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)))
          X) ≫
      (uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).map f
have a : Eq (α := ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y).obj (op (F.obj X)))
  ((uliftYonedaEquiv :
        (a : uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ (uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y) →
          ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y).obj (op (F.obj X)))
      ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).map f ≫
        Iso.hom
          ((fun (X : C) ↦
              (Functor.leftKanExtensionUnique (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
                  (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X)
                  (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
                  (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X)) :
                Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X) ≅
                  Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)))
            Y)) :
    ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y).obj (op (F.obj X)))
  ((uliftYonedaEquiv :
        (a : uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ (uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y) →
          ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y).obj (op (F.obj X)))
      (Iso.hom
          ((fun (X : C) ↦
              (Functor.leftKanExtensionUnique (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
                  (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X)
                  (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
                  (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X)) :
                Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X) ≅
                  Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)))
            X) ≫
        (uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).map f) :
    ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y).obj (op (F.obj X)))
Tactic: apply uliftYonedaEquiv.injective