Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
x : P.Elementsᵒᵖ
eq :
  (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))).map (uliftYonedaEquiv.symm (unop x).snd) ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1)) ≫
      (F.op.lan ⋙ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))).obj F.op).map
        (uliftYonedaEquiv.symm (unop x).snd)
eq₁ :
  (hom
        (((StructuredArrow.hom (Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom) ≫
                  ((Functor.whiskeringLeft C (Cᵒᵖ ⥤ Type (max (max w v₁) v₂)) (Dᵒᵖ ⥤ Type (max (max w v₁) v₂))).obj
                        uliftYoneda.{max w v₂, v₁, u₁}).map
                    (StructuredArrow.Hom.right f)).app
              (unop (unop x).fst)).app
          (F.op.obj (unop x).fst)))
      { down := 𝟙 (unop (F.op.obj (unop x).fst)) } =
    (hom (((StructuredArrow.hom Φ).app (unop (unop x).fst)).app (F.op.obj (unop x).fst)))
      { down := 𝟙 (unop (F.op.obj (unop x).fst)) }
⊢ (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
    (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)

Tactic:
have eq₂ := congr_hom (CC := fun X ↦ X) (congr_app (congr_app (StructuredArrow.w g) x.unop.1.unop)
    (F.op.obj x.unop.1)) (ULift.up (𝟙 _))

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
x : P.Elementsᵒᵖ
eq :
  (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))).map (uliftYonedaEquiv.symm (unop x).snd) ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1)) ≫
      (F.op.lan ⋙ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))).obj F.op).map
        (uliftYonedaEquiv.symm (unop x).snd)
eq₁ :
  (hom
        (((StructuredArrow.hom (Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom) ≫
                  ((Functor.whiskeringLeft C (Cᵒᵖ ⥤ Type (max (max w v₁) v₂)) (Dᵒᵖ ⥤ Type (max (max w v₁) v₂))).obj
                        uliftYoneda.{max w v₂, v₁, u₁}).map
                    (StructuredArrow.Hom.right f)).app
              (unop (unop x).fst)).app
          (F.op.obj (unop x).fst)))
      { down := 𝟙 (unop (F.op.obj (unop x).fst)) } =
    (hom (((StructuredArrow.hom Φ).app (unop (unop x).fst)).app (F.op.obj (unop x).fst)))
      { down := 𝟙 (unop (F.op.obj (unop x).fst)) }
eq₂ :
  (hom
        (((StructuredArrow.hom (Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom) ≫
                  ((Functor.whiskeringLeft C (Cᵒᵖ ⥤ Type (max (max w v₁) v₂)) (Dᵒᵖ ⥤ Type (max (max w v₁) v₂))).obj
                        uliftYoneda.{max w v₂, v₁, u₁}).map
                    (StructuredArrow.Hom.right g)).app
              (unop (unop x).fst)).app
          (F.op.obj (unop x).fst)))
      { down := 𝟙 (unop (F.op.obj (unop x).fst)) } =
    (hom (((StructuredArrow.hom Φ).app (unop (unop x).fst)).app (F.op.obj (unop x).fst)))
      { down := 𝟙 (unop (F.op.obj (unop x).fst)) }
⊢ (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
    (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)