Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
left✝ : IsIso α
right✝ :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
P : Cᵒᵖ ⥤ Type (max (max w v₂) v₁)
e : (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor ⋙
    CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ≅
  functorToRepresentables P ⋙ L :=
  (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.isoWhiskerLeft
      ((CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P).isoWhiskerLeft (asIso α)) ≪≫
    (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.isoWhiskerLeft
        ((CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P).associator uliftYoneda.{max w v₂, v₁, u₁} L).symm ≪≫
      ((CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.associator
            (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ uliftYoneda.{max w v₂, v₁, u₁}) L).symm ≪≫
        Functor.isoWhiskerRight
          (Iso.refl
            ((CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor ⋙
              CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ uliftYoneda.{max w v₂, v₁, u₁}))
          L
⊢ IsColimit
    (Cocone.whisker (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor
      ((Functor.LeftExtension.mk L α).coconeAt P))

Tactic:
refine (IsColimit.precomposeHomEquiv e.symm _).1 ?_

Goal state after:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
left✝ : IsIso α
right✝ :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
P : Cᵒᵖ ⥤ Type (max (max w v₂) v₁)
e : (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor ⋙
    CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ≅
  functorToRepresentables P ⋙ L :=
  (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.isoWhiskerLeft
      ((CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P).isoWhiskerLeft (asIso α)) ≪≫
    (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.isoWhiskerLeft
        ((CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P).associator uliftYoneda.{max w v₂, v₁, u₁} L).symm ≪≫
      ((CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.associator
            (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ uliftYoneda.{max w v₂, v₁, u₁}) L).symm ≪≫
        Functor.isoWhiskerRight
          (Iso.refl
            ((CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor ⋙
              CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ uliftYoneda.{max w v₂, v₁, u₁}))
          L
⊢ IsColimit
    ((Cocone.precompose e.symm.hom).obj
      (Cocone.whisker (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor
        ((Functor.LeftExtension.mk L α).coconeAt P)))