-- Mathlib/CategoryTheory/Limits/Presheaf.lean
lemma isLeftKanExtension_along_yoneda_iff :
    L.IsLeftKanExtension α ↔
      (IsIso α ∧ PreservesColimitsOfSize.{v₁, max u₁ v₁} L)

Proof state:
case mpr.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : yoneda.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ
α : A ⟶ yoneda ⋙ L
left✝ : IsIso α
right✝ : PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L
P : Cᵒᵖ ⥤ Type v₁
⊢ (Functor.LeftExtension.mk L α).IsPointwiseLeftKanExtensionAt P

Tactic:
dsimp [Functor.LeftExtension.IsPointwiseLeftKanExtensionAt]

Result:
case mpr.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : yoneda.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ
α : A ⟶ yoneda ⋙ L
left✝ : IsIso α
right✝ : PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L
P : Cᵒᵖ ⥤ Type v₁
⊢ IsColimit ((Functor.LeftExtension.mk L α).coconeAt P)

Proof state:
case mpr.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : yoneda.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ
α : A ⟶ yoneda ⋙ L
left✝ : IsIso α
right✝ : PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L
P : Cᵒᵖ ⥤ Type v₁
⊢ IsColimit
    (Cocone.whisker (CategoryOfElements.costructuredArrowYonedaEquivalence P).functor
      ((Functor.LeftExtension.mk L α).coconeAt P))

Tactic:
let e : CategoryOfElements.toCostructuredArrow P ⋙ CostructuredArrow.proj yoneda P ⋙ A ≅
    functorToRepresentables P ⋙ L :=
  isoWhiskerLeft _ (isoWhiskerLeft _ (asIso α)) ≪≫
    isoWhiskerLeft _ (Functor.associator _ _ _).symm ≪≫
    (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight (Iso.refl _) L

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

Proof state:
case mpr.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : yoneda.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ
α : A ⟶ yoneda ⋙ L
left✝ : IsIso α
right✝ : PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L
P : Cᵒᵖ ⥤ Type v₁
⊢ IsColimit ((Functor.LeftExtension.mk L α).coconeAt P)

Tactic:
apply IsColimit.ofWhiskerEquivalence (CategoryOfElements.costructuredArrowYonedaEquivalence _)

Result:
case mpr.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : yoneda.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ
α : A ⟶ yoneda ⋙ L
left✝ : IsIso α
right✝ : PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L
P : Cᵒᵖ ⥤ Type v₁
⊢ IsColimit
    (Cocone.whisker (CategoryOfElements.costructuredArrowYonedaEquivalence P).functor
      ((Functor.LeftExtension.mk L α).coconeAt P))

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

Tactic:
exact IsColimit.ofIsoColimit (isColimitOfPreserves L (colimitOfRepresentable P))
  (Cocones.ext (Iso.refl _))

Result:
no goals

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

Tactic:
apply (IsColimit.precomposeHomEquiv e.symm _).1

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

Proof state:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₁, u₂} ℰ
A : C ⥤ ℰ
inst✝ : yoneda.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ
α : A ⟶ yoneda ⋙ L
a✝ : L.IsLeftKanExtension α
⊢ IsIso α ∧ PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L

Tactic:
exact ⟨inferInstance, preservesColimits_of_natIso
  (Functor.leftKanExtensionUnique _ (yoneda.leftKanExtensionUnit A) _ α)⟩

Result:
no goals