-- 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
⊢ L.IsLeftKanExtension α

Tactic:
apply Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
  (E := Functor.LeftExtension.mk _ α)

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
⊢ (Functor.LeftExtension.mk L α).IsPointwiseLeftKanExtension

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
⊢ (Functor.LeftExtension.mk L α).IsPointwiseLeftKanExtension

Tactic:
intro P

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₁
⊢ (Functor.LeftExtension.mk L α).IsPointwiseLeftKanExtensionAt 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
⊢ L.IsLeftKanExtension α → IsIso α ∧ PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L

Tactic:
intro

Result:
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

Proof state:
case mpr
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
⊢ IsIso α ∧ PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L → L.IsLeftKanExtension α

Tactic:
rintro ⟨_, _⟩

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
⊢ L.IsLeftKanExtension α

Proof state:
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
⊢ L.IsLeftKanExtension α ↔ IsIso α ∧ PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L

Tactic:
constructor

Result:
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
⊢ L.IsLeftKanExtension α → IsIso α ∧ PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L

case mpr
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
⊢ IsIso α ∧ PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L → L.IsLeftKanExtension α