awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P_1 : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : ℰ
f : P ⟶ Q
g : Q ⟶ (restrictedULiftYoneda A).obj X
p : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
⊢ Eq (α := A.obj p.left ⟶ X)
    ((StructuredArrow.hom (Functor.LeftExtension.mk L α)).app p.left ≫
      (StructuredArrow.right (Functor.LeftExtension.mk L α)).map p.hom ≫
        (Equiv.symm (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)) :
            (a :
                CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
                  (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj X) →
              ((Functor.LeftExtension.mk L α).coconeAt P).pt ⟶ X)
          (((restrictedULiftYonedaHomEquiv'.{w, v₁, v₂, u₁, u₂} A P X).symm :
              (a : P ⟶ (restrictedULiftYoneda A).obj X) →
                CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
                  (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj X)
            (f ≫ g)))
    (NatTrans.app
      (((restrictedULiftYonedaHomEquiv'.{w, v₁, v₂, u₁, u₂} A P X).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj X) →
            CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
              (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj X)
        (f ≫ g))
      p)

Tactic:
have hfg := (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension
          L α P).comp_homEquiv_symm ((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)) p
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P_1 : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X Y : ℰ
f : L.obj P ⟶ X
g : X ⟶ Y
⊢ ∀ {W W' : ℰ}
    (f :
      Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
        (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
        (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) W))
    (g : W ⟶ W'),
    Eq.{v₂ + 1} (α := ((Functor.LeftExtension.mk L α).coconeAt P).pt ⟶ W')
      ((Equiv.symm (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)) :
            (a :
                CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
                  (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W') →
              ((Functor.LeftExtension.mk L α).coconeAt P).pt ⟶ W')
          (f ≫ Functor.map (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) g) :
        ((Functor.LeftExtension.mk L α).coconeAt P).pt ⟶ W')
      ((Equiv.symm (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)) :
              (a :
                  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
                    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W) →
                ((Functor.LeftExtension.mk L α).coconeAt P).pt ⟶ W)
            f ≫
          g :
        ((Functor.LeftExtension.mk L α).coconeAt P).pt ⟶ W')

Tactic:
have := @IsColimit.homEquiv_symm_naturality (h :=
          Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P_1 : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X Y : ℰ
f : L.obj P ⟶ X
g : X ⟶ Y
this :
  ∀ {W W' : ℰ}
    (f :
      Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
        (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
        (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) W))
    (g : W ⟶ W'),
    Eq.{v₂ + 1} (α := L.obj P ⟶ W')
      ((Equiv.symm (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)) :
            (a :
                CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
                  (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W') →
              L.obj P ⟶ W')
          (f ≫ Functor.map (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) g) :
        L.obj P ⟶ W')
      ((Equiv.symm (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)) :
              (a :
                  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
                    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W) →
                L.obj P ⟶ W)
            f ≫
          g :
        L.obj P ⟶ W')
a :
  Eq.{v₂ + 1} (α := L.obj P ⟶ Y)
    (((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P Y).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj Y) → L.obj P ⟶ Y)
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P Y :
            (a : L.obj P ⟶ Y) → P ⟶ (restrictedULiftYoneda A).obj Y)
          (f ≫ g)) :
      L.obj P ⟶ Y)
    (((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P Y).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj Y) → L.obj P ⟶ Y)
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P X :
              (a : L.obj P ⟶ X) → P ⟶ (restrictedULiftYoneda A).obj X)
            f ≫
          (restrictedULiftYoneda A).map g) :
      L.obj P ⟶ Y)
⊢ Eq (α := P ⟶ (restrictedULiftYoneda A).obj Y)
    ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P Y :
          (a : L.obj P ⟶ Y) → P ⟶ (restrictedULiftYoneda A).obj Y)
        (f ≫ g) :
      P ⟶ (restrictedULiftYoneda A).obj Y)
    ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P X :
            (a : L.obj P ⟶ X) → P ⟶ (restrictedULiftYoneda A).obj X)
          f ≫
        (restrictedULiftYoneda A).map g :
      P ⟶ (restrictedULiftYoneda A).obj Y)

Tactic:
apply (restrictedULiftYonedaHomEquiv L α P Y).symm.injective

Premises used: CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P_1 : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X Y : ℰ
f : L.obj P ⟶ X
g : X ⟶ Y
this :
  ∀ {W W' : ℰ}
    (f :
      Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
        (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
        (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) W))
    (g : W ⟶ W'),
    Eq.{v₂ + 1} (α := L.obj P ⟶ W')
      ((Equiv.symm (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)) :
            (a :
                CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
                  (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W') →
              L.obj P ⟶ W')
          (f ≫ Functor.map (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) g) :
        L.obj P ⟶ W')
      ((Equiv.symm (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)) :
              (a :
                  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
                    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W) →
                L.obj P ⟶ W)
            f ≫
          g :
        L.obj P ⟶ W')
j : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
⊢ Eq (α := Functor.obj (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A) j ⟶ Y)
    (((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫
      ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P Y).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj Y) → L.obj P ⟶ Y)
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P Y :
            (a : L.obj P ⟶ Y) → P ⟶ (restrictedULiftYoneda A).obj Y)
          (f ≫ g)))
    (((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫
      ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P Y).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj Y) → L.obj P ⟶ Y)
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P X :
              (a : L.obj P ⟶ X) → P ⟶ (restrictedULiftYoneda A).obj X)
            f ≫
          (restrictedULiftYoneda A).map g))

Tactic:
simp [restrictedULiftYonedaHomEquiv,
          restrictedULiftYonedaHomEquiv'_symm_naturality_right, this]

Premises used: CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv, CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_naturality_right
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
Y : ℰ
f : L.obj P ⟶ Y
Z : Cᵒᵖ
z : P.obj Z
⊢ Eq (α := (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (((restrictedULiftYoneda A).obj Y).obj Z))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app
              (((uliftYonedaAdjunction.{w, v₁, v₂, u₁, u₂} L α).homEquiv P Y :
                  (a : L.obj P ⟶ Y) → P ⟶ (restrictedULiftYoneda A).obj Y)
                f)
              Z) :
          (a : (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj Z)) →
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (((restrictedULiftYoneda A).obj Y).obj Z))
        z :
      (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (((restrictedULiftYoneda A).obj Y).obj Z))
    ({
        down :=
          α.app (unop Z) ≫
            L.map
                ((Equiv.symm uliftYonedaEquiv :
                    (a : P.obj (op (unop Z))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop Z) ⟶ P)
                  z) ≫
              f } :
      ULift.{max v₁ w, v₂} (A.obj (unop Z) ⟶ Y))

Tactic:
simp [uliftYonedaAdjunction, restrictedULiftYonedaHomEquiv,
    restrictedULiftYonedaHomEquiv', IsColimit.homEquiv]

Premises used: CategoryTheory.Presheaf.uliftYonedaAdjunction, CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv', CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv, CategoryTheory.Limits.IsColimit.homEquiv
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
Z : Cᵒᵖ
z : P.obj Z
⊢ ((uliftYonedaAdjunction.{w, v₁, v₂, u₁, u₂} L α).homEquiv P (L.obj P) :
        (a : L.obj P ⟶ L.obj P) → P ⟶ (restrictedULiftYoneda A).obj (L.obj P))
      (𝟙 (L.obj P)) =
    (uliftYonedaAdjunction.{w, v₁, v₂, u₁, u₂} L α).unit.app P ≫ (restrictedULiftYoneda A).map (𝟙 (L.obj P))

Tactic:
have h₁ := (uliftYonedaAdjunction.{w} L α).homEquiv_unit P _ (𝟙 _)
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
Z : Cᵒᵖ
z : P.obj Z
h₁ :
  ((uliftYonedaAdjunction.{w, v₁, v₂, u₁, u₂} L α).homEquiv P (L.obj P) :
        (a : L.obj P ⟶ L.obj P) → P ⟶ (restrictedULiftYoneda A).obj (L.obj P))
      (𝟙 (L.obj P)) =
    (uliftYonedaAdjunction.{w, v₁, v₂, u₁, u₂} L α).unit.app P ≫ (restrictedULiftYoneda A).map (𝟙 (L.obj P))
⊢ ((uliftYonedaAdjunction.{w, v₁, v₂, u₁, u₂} L α).homEquiv P (L.obj P) :
        (a : L.obj P ⟶ L.obj P) → P ⟶ (restrictedULiftYoneda A).obj (L.obj P))
      (𝟙 (L.obj P)) =
    (uliftYonedaAdjunction.{w, v₁, v₂, u₁, u₂} L α).unit.app P

Tactic:
simp only [Functor.comp_obj, Functor.map_id, comp_id] at h₁

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
Z : Cᵒᵖ
z : P.obj Z
h₁ :
  ((uliftYonedaAdjunction.{w, v₁, v₂, u₁, u₂} L α).homEquiv P (L.obj P) :
        (a : L.obj P ⟶ L.obj P) → P ⟶ (restrictedULiftYoneda A).obj (L.obj P))
      (𝟙 (L.obj P)) =
    (uliftYonedaAdjunction.{w, v₁, v₂, u₁, u₂} L α).unit.app P
⊢ Eq (α := ((restrictedULiftYoneda A).obj (L.obj P)).obj Z)
    ((hom (FC := TypeCat.Fun) (((uliftYonedaAdjunction.{w, v₁, v₂, u₁, u₂} L α).unit.app P).app Z) :
          (a : P.obj Z) → ((restrictedULiftYoneda A).obj (L.obj P)).obj Z)
        z :
      ((restrictedULiftYoneda A).obj (L.obj P)).obj Z)
    ({
        down :=
          α.app (unop Z) ≫
            L.map
              ((Equiv.symm uliftYonedaEquiv : (a : P.obj Z) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop Z) ⟶ P) z) } :
      ULift.{max v₁ w, v₂} (A.obj (unop Z) ⟶ L.obj P))

Tactic:
simp [← h₁]
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
⊢ PreservesColimitsOfSize.{v₃, u₃, max (max (max u₁ v₁) v₂) w, v₂, max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂} L

Tactic:
(uliftYonedaAdjunction L α).leftAdjoint_preservesColimits

Premises used: CategoryTheory.Adjunction.leftAdjoint_preservesColimits, CategoryTheory.Presheaf.uliftYonedaAdjunction
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
⊢ IsIso α

Tactic:
(Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension _ α).isIso_hom

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isIso_hom, CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
⊢ PreservesColimitsOfSize.{v₃, u₃, max (max (max v₂ w) u₁) v₁, v₂, max (max (max (v₂ + 1) (w + 1)) u₁) (v₁ + 1), u₂}
    (Functor.leftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A)

Tactic:
(uliftYonedaAdjunction _ (uliftYoneda.leftKanExtensionUnit A)).leftAdjoint_preservesColimits

Premises used: CategoryTheory.Adjunction.leftAdjoint_preservesColimits, CategoryTheory.Functor.leftKanExtensionUnit, CategoryTheory.Presheaf.uliftYonedaAdjunction, CategoryTheory.uliftYoneda
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
⊢ IsIso (Y := uliftYoneda.{max w v₂, v₁, u₁} ⋙ Functor.leftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A)
    (Functor.leftKanExtensionUnit uliftYoneda.{max w v₂, v₁, u₁} A)

Tactic:
isIso_of_isLeftKanExtension _ (uliftYoneda.leftKanExtensionUnit A)

Premises used: CategoryTheory.Presheaf.isIso_of_isLeftKanExtension, CategoryTheory.Functor.leftKanExtensionUnit, CategoryTheory.uliftYoneda
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
dsimp :
  Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    (Functor.map uliftYoneda.{w, v₁, u₁} (↑f.unop : (unop x₂).fst ⟶ (unop x₁).fst).unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₂).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₂).fst) ⟶ P)
        ((unop x₂).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₁).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
        ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) ≫
      𝟙 P)
⊢ Eq (α := (functorToRepresentables.{w, v₁, u₁} P).obj x₁ ⟶ Functor.obj (Functor.obj (Functor.const P.Elementsᵒᵖ) P) x₂)
    ((functorToRepresentables.{w, v₁, u₁} P).map f ≫
      (Equiv.symm uliftYonedaEquiv :
          (a : (((Functor.const P.Elementsᵒᵖ).obj P).obj x₂).obj (op ((CategoryOfElements.π P).leftOp.obj x₂))) →
            uliftYoneda.{w, v₁, u₁}.obj ((CategoryOfElements.π P).leftOp.obj x₂) ⟶
              ((Functor.const P.Elementsᵒᵖ).obj P).obj x₂)
        ((unop x₂).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
    ((Equiv.symm uliftYonedaEquiv :
          (a : (((Functor.const P.Elementsᵒᵖ).obj P).obj x₁).obj (op ((CategoryOfElements.π P).leftOp.obj x₁))) →
            uliftYoneda.{w, v₁, u₁}.obj ((CategoryOfElements.π P).leftOp.obj x₁) ⟶
              ((Functor.const P.Elementsᵒᵖ).obj P).obj x₁)
        ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) ≫
      Functor.map (Functor.obj (Functor.const P.Elementsᵒᵖ) P) f)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
rw :
  Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    (Functor.map uliftYoneda.{w, v₁, u₁} (↑f.unop : (unop x₂).fst ⟶ (unop x₁).fst).unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₂).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₂).fst) ⟶ P)
        ((unop x₂).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₁).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
      ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
rw₁ :
  Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    ((Equiv.symm uliftYonedaEquiv :
          (a : P.obj (op (unop (unop x₁).fst))) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
        ((hom (FC := TypeCat.Fun) (P.map (↑f.unop : (unop x₂).fst ⟶ (unop x₁).fst)) :
            (a : (fun (X : Type (max v₁ w)) ↦ X) (P.obj (unop x₂).fst)) →
              (fun (X : Type (max v₁ w)) ↦ X) (P.obj (unop x₁).fst))
          ((unop x₂).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))) :
      Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₁).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
        ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) :
      Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
rw₂ rw₃ :
  Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    ((Equiv.symm uliftYonedaEquiv :
          (a : P.obj (op (unop (unop x₁).fst))) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
        ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) :
      Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₁).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
        ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) :
      Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
⊢ Eq (α := Functor.obj uliftYoneda.{w, v₁, u₁} (unop ((unop x₁).fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    (Functor.map uliftYoneda.{w, v₁, u₁} (↑f.unop : (unop x₂).fst ⟶ (unop x₁).fst).unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₂).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₂).fst) ⟶ P)
        ((unop x₂).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (unop x₁).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop x₁).fst) ⟶ P)
        ((unop x₁).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) ≫
      𝟙 P)

Tactic:
rw [comp_id, ← uliftYonedaEquiv_symm_map, f.unop.2]

Premises used: CategoryTheory.uliftYonedaEquiv_symm_map, Quiver.Hom.unop, CategoryTheory.Category.comp_id, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P₁ P₂ : Cᵒᵖ ⥤ Type (max w v₁)
α : P₁ ⟶ P₂
j : P₁.Elementsᵒᵖ
w :
  ∀ (T : Cᵒᵖ) (f : ((functorToRepresentables.{w, v₁, u₁} P₁).obj j).obj T),
    (hom (FC := TypeCat.Fun) (((coconeOfRepresentable P₁).ι.app j ≫ α).app T)).toFun f =
      TypeCat.Fun.toFun
        (@hom _ types TypeCat.Fun _ _ _ _ _
          (NatTrans.app ((coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j)) T))
        f
⊢ (coconeOfRepresentable P₁).ι.app j ≫ α = (coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j)

Tactic:
ext T f
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P₁ P₂ : Cᵒᵖ ⥤ Type (max w v₁)
α : P₁ ⟶ P₂
j : P₁.Elementsᵒᵖ
T : Cᵒᵖ
f : ((functorToRepresentables.{w, v₁, u₁} P₁).obj j).obj T
⊢ (hom (FC := TypeCat.Fun) (((coconeOfRepresentable P₁).ι.app j ≫ α).app T)).toFun f =
    TypeCat.Fun.toFun
      (@hom _ types TypeCat.Fun _ _ _ _ _
        (NatTrans.app ((coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j)) T))
      f

Tactic:
simp [uliftYonedaEquiv]

Premises used: CategoryTheory.uliftYonedaEquiv