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)) }
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)

Tactic:
dsimp [uliftYoneda, uliftYonedaMap, uliftYonedaEquiv,
        Functor.leftKanExtensionUnique] at eq₁ eq₂ eq₃ ⊢

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
        (((yoneda.obj (F.obj Y) ⋙ uliftFunctor.{max w v₁, v₂}).descOfIsLeftKanExtension
              { app := fun x ↦ ↾fun f ↦ { down := F.map f.down }, naturality := ⋯ }
              (F.op.lan.obj (yoneda.obj Y ⋙ uliftFunctor.{max v₂ w, v₁}))
              (F.op.lanUnit.app (yoneda.obj Y ⋙ uliftFunctor.{max v₂ w, v₁}))).app
          (op (F.obj X))))
      { down := F.map f } =
    (hom ((F.op.lanUnit.app (yoneda.obj Y ⋙ uliftFunctor.{max v₂ w, v₁})).app (op X))) { down := f }
eq₂ :
  (hom
        (((yoneda.obj (F.obj X) ⋙ uliftFunctor.{max w v₁, v₂}).descOfIsLeftKanExtension
              { app := fun x ↦ ↾fun f ↦ { down := F.map f.down }, naturality := ⋯ }
              (F.op.lan.obj (yoneda.obj X ⋙ uliftFunctor.{max v₂ w, v₁}))
              (F.op.lanUnit.app (yoneda.obj X ⋙ uliftFunctor.{max v₂ w, v₁}))).app
          (op (F.obj X))))
      { down := F.map (𝟙 X) } =
    (hom ((F.op.lanUnit.app (yoneda.obj X ⋙ uliftFunctor.{max v₂ w, v₁})).app (op X))) { down := 𝟙 X }
eq₃ :
  (hom ((F.op.lanUnit.app (yoneda.obj Y ⋙ uliftFunctor.{max w v₂, v₁})).app (op X))) { down := 𝟙 X ≫ f } =
    (hom ((F.op.lan.map (Functor.whiskerRight (yoneda.map f) uliftFunctor.{max w v₂, v₁})).app (op (F.obj X))))
      ((hom ((F.op.lanUnit.app (yoneda.obj X ⋙ uliftFunctor.{max w v₂, v₁})).app (op X))) { down := 𝟙 X })
⊢ (hom
        (((yoneda.obj (F.obj Y) ⋙ uliftFunctor.{max w v₁, v₂}).descOfIsLeftKanExtension
              { app := fun x ↦ ↾fun f ↦ { down := F.map f.down }, naturality := ⋯ }
              (F.op.lan.obj (yoneda.obj Y ⋙ uliftFunctor.{max w v₂, v₁}))
              (𝟙 (yoneda.obj Y ⋙ uliftFunctor.{max w v₂, v₁}) ≫
                F.op.lanUnit.app (yoneda.obj Y ⋙ uliftFunctor.{max v₂ w, v₁}))).app
          (op (F.obj X))))
      { down := 𝟙 (F.obj X) ≫ F.map f } =
    (hom ((F.op.lan.map (Functor.whiskerRight (yoneda.map f) uliftFunctor.{max w v₂, v₁})).app (op (F.obj X))))
      ((hom
          (((yoneda.obj (F.obj X) ⋙ uliftFunctor.{max w v₁, v₂}).descOfIsLeftKanExtension
                { app := fun x ↦ ↾fun f ↦ { down := F.map f.down }, naturality := ⋯ }
                (F.op.lan.obj (yoneda.obj X ⋙ uliftFunctor.{max w v₂, v₁}))
                (𝟙 (yoneda.obj X ⋙ uliftFunctor.{max w v₂, v₁}) ≫
                  F.op.lanUnit.app (yoneda.obj X ⋙ uliftFunctor.{max v₂ w, v₁}))).app
            (op (F.obj X))))
        { down := 𝟙 (F.obj X) })