Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X Y : C
f : X ⟶ Y
eq₁ :
  (hom
        ((uliftYonedaMap F Y).app (op X) ≫
          ((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj Y)).descOfIsLeftKanExtension (uliftYonedaMap F Y)
                (F.op.lan.obj (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y))
                (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y))).app
            (F.op.obj (op X))))
      { down := f } =
    (hom ((F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y)).app (op X))) { down := f }
eq₂ :
  (hom
        ((uliftYonedaMap F X).app (op X) ≫
          ((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)).descOfIsLeftKanExtension (uliftYonedaMap F X)
                (F.op.lan.obj (uliftYoneda.{max v₂ w, v₁, u₁}.obj X))
                (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj X))).app
            (F.op.obj (op X))))
      { down := 𝟙 (unop (op X)) } =
    (hom ((F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj X)).app (op X))) { down := 𝟙 (unop (op X)) }
⊢ uliftYonedaEquiv
      ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).map f ≫
        ((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj Y)).leftKanExtensionUnique (uliftYonedaMap F Y)
            (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj Y))
            (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y))).hom) =
    uliftYonedaEquiv
      (((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)).leftKanExtensionUnique (uliftYonedaMap F X)
            (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X))
            (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj X))).hom ≫
        (uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).map f)

Tactic:
have eq₃ := ConcreteCategory.congr_hom (congr_app (F.op.lanUnit.naturality
        (uliftYoneda.{max w v₂}.map f)) _) ⟨𝟙 _⟩

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X Y : C
f : X ⟶ Y
eq₁ :
  (hom
        ((uliftYonedaMap F Y).app (op X) ≫
          ((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj Y)).descOfIsLeftKanExtension (uliftYonedaMap F Y)
                (F.op.lan.obj (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y))
                (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y))).app
            (F.op.obj (op X))))
      { down := f } =
    (hom ((F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y)).app (op X))) { down := f }
eq₂ :
  (hom
        ((uliftYonedaMap F X).app (op X) ≫
          ((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)).descOfIsLeftKanExtension (uliftYonedaMap F X)
                (F.op.lan.obj (uliftYoneda.{max v₂ w, v₁, u₁}.obj X))
                (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj X))).app
            (F.op.obj (op X))))
      { down := 𝟙 (unop (op X)) } =
    (hom ((F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj X)).app (op X))) { down := 𝟙 (unop (op X)) }
eq₃ :
  (hom
        (((𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))).map (uliftYoneda.{max w v₂, v₁, u₁}.map f) ≫
              F.op.lanUnit.app (uliftYoneda.{max w v₂, v₁, u₁}.obj Y)).app
          (op X)))
      { down := 𝟙 (unop (op X)) } =
    (hom
        ((F.op.lanUnit.app (uliftYoneda.{max w v₂, v₁, u₁}.obj X) ≫
              (F.op.lan ⋙ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))).obj F.op).map
                (uliftYoneda.{max w v₂, v₁, u₁}.map f)).app
          (op X)))
      { down := 𝟙 (unop (op X)) }
⊢ uliftYonedaEquiv
      ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).map f ≫
        ((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj Y)).leftKanExtensionUnique (uliftYonedaMap F Y)
            (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj Y))
            (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y))).hom) =
    uliftYonedaEquiv
      (((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)).leftKanExtensionUnique (uliftYonedaMap F X)
            (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X))
            (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj X))).hom ≫
        (uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).map f)