-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
x : P.Elementsᵒᵖ
eq :
  Eq (α := Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1) ⟶ F.op ⋙ Functor.obj F.op.lan P)
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x).1) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1) ⟶ P)
          ((unop x).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) ≫
        NatTrans.app F.op.lanUnit P :
      Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1) ⟶ F.op ⋙ Functor.obj F.op.lan P)
    (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1)) ≫
        F.op.whiskerLeft
          (Functor.map F.op.lan
            ((Equiv.symm uliftYonedaEquiv :
                (a : P.obj (unop x).1) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1) ⟶ P)
              ((unop x).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))) :
      Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1) ⟶ F.op ⋙ Functor.obj F.op.lan P)
eq₁ :
  Eq (α :=
    ((StructuredArrow.right Φ).obj
          (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))).obj
      (op (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app
              ((StructuredArrow.Hom.right f).app
                (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))
              (op (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
          (a :
              (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).fst))).obj
                (op (F.obj (unop (unop x).fst)))) →
            ((StructuredArrow.right Φ).obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).fst))).obj
              (op (F.obj (unop (unop x).fst))))
        ((hom (FC := TypeCat.Fun)
              (NatTrans.app
                (NatTrans.app (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F))
                  (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                (op (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
            (a : ULift.{max v₁ w, v₂} (F.obj (unop (unop x).fst) ⟶ F.obj (unop (unop x).fst))) →
              (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).fst))).obj
                (op (F.obj (unop (unop x).fst))))
          { down := 𝟙 (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))) }) :
      ((StructuredArrow.right Φ).obj
            (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))).obj
        (op (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app ((StructuredArrow.hom Φ).app (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
              (op (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
          (a : ULift.{max v₁ w, v₂} (F.obj (unop (unop x).fst) ⟶ F.obj (unop (unop x).fst))) →
            ((StructuredArrow.right Φ).obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).fst))).obj
              (op (F.obj (unop (unop x).fst))))
        { down := 𝟙 (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))) } :
      ((StructuredArrow.right Φ).obj
            (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))).obj
        (op (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
eq₂ :
  Eq (α :=
    ((StructuredArrow.right Φ).obj
          (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))).obj
      (op (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app
              ((StructuredArrow.Hom.right g).app
                (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))
              (op (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
          (a :
              (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).fst))).obj
                (op (F.obj (unop (unop x).fst)))) →
            ((StructuredArrow.right Φ).obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).fst))).obj
              (op (F.obj (unop (unop x).fst))))
        ((hom (FC := TypeCat.Fun)
              (NatTrans.app
                (NatTrans.app (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F))
                  (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
                (op (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
            (a : ULift.{max v₁ w, v₂} (F.obj (unop (unop x).fst) ⟶ F.obj (unop (unop x).fst))) →
              (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).fst))).obj
                (op (F.obj (unop (unop x).fst))))
          { down := 𝟙 (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))) }) :
      ((StructuredArrow.right Φ).obj
            (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))).obj
        (op (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app ((StructuredArrow.hom Φ).app (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
              (op (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
          (a : ULift.{max v₁ w, v₂} (F.obj (unop (unop x).fst) ⟶ F.obj (unop (unop x).fst))) →
            ((StructuredArrow.right Φ).obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).fst))).obj
              (op (F.obj (unop (unop x).fst))))
        { down := 𝟙 (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))) } :
      ((StructuredArrow.right Φ).obj
            (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))).obj
        (op (F.obj (unop ((unop x).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
h :
  Eq (α :=
    Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1)) ⟶
      (StructuredArrow.right Φ).obj P)
    (Functor.map F.op.lan
        ((Equiv.symm uliftYonedaEquiv :
            (a : P.obj (unop x).1) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1) ⟶ P)
          ((unop x).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ≫
      (StructuredArrow.Hom.right f).app P)
    (Functor.map F.op.lan
        ((Equiv.symm uliftYonedaEquiv :
            (a : P.obj (unop x).1) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1) ⟶ P)
          ((unop x).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ≫
      (StructuredArrow.Hom.right g).app P)
⊢ NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1)) ≫
      F.op.whiskerLeft
        (Functor.map F.op.lan
            ((Equiv.symm uliftYonedaEquiv :
                (a : P.obj (unop x).1) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1) ⟶ P)
              ((unop x).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ≫
          (StructuredArrow.Hom.right f).app P) =
    NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1)) ≫
      F.op.whiskerLeft
        (Functor.map F.op.lan
            ((Equiv.symm uliftYonedaEquiv :
                (a : P.obj (unop x).1) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1) ⟶ P)
              ((unop x).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ≫
          (StructuredArrow.Hom.right g).app P)

Tactic:
congr 2