awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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₁)
s : Cocone (functorToRepresentables.{w, v₁, u₁} P)
m : (coconeOfRepresentable P).pt ⟶ s.pt
hm :
  ∀ (j : P.Elementsᵒᵖ),
    (Equiv.symm uliftYonedaEquiv : (a : P.obj (unop j).fst) → uliftYoneda.{w, v₁, u₁}.obj (unop (unop j).fst) ⟶ P)
          ((unop j).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) ≫
        m =
      s.ι.app j
X : Cᵒᵖ
x : (coconeOfRepresentable P).pt.obj X
w :
  Eq (α := s.pt.obj X) ((hom (FC := TypeCat.Fun) (m.app X) : (a : P.obj X) → s.pt.obj X) x : s.pt.obj X)
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj X)
        ((Equiv.symm uliftYonedaEquiv :
              (a : P.obj (unop (op (P.elementsMk X x))).fst) →
                uliftYoneda.{w, v₁, u₁}.obj (unop (unop (op (P.elementsMk X x))).fst) ⟶ P)
            ((unop (op (P.elementsMk X x))).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) ≫
          m) :
      s.pt.obj X)
w₁ :
  Eq (α := s.pt.obj X) ((hom (FC := TypeCat.Fun) (m.app X) : (a : P.obj X) → s.pt.obj X) x : s.pt.obj X)
    ((hom (FC := TypeCat.Fun) (m.app (op (unop X))) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (P.obj (op (unop X)))) →
            (fun (X : Type (max v₁ w)) ↦ X) (s.pt.obj (op (unop X))))
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ P) → P.obj (op (unop X)))
          ((Equiv.symm uliftYonedaEquiv :
              (a : P.obj (unop (op (P.elementsMk X x))).fst) →
                uliftYoneda.{w, v₁, u₁}.obj (unop (unop (op (P.elementsMk X x))).fst) ⟶ P)
            ((unop (op (P.elementsMk X x))).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))) :
      (fun (X : Type (max v₁ w)) ↦ X) (s.pt.obj (op (unop X))))
⊢ Eq (α := s.pt.obj X) ((hom (FC := TypeCat.Fun) (m.app X) : (a : P.obj X) → s.pt.obj X) x : s.pt.obj X)
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ s.pt) → s.pt.obj X)
        (s.ι.app (op (P.elementsMk X x))) :
      s.pt.obj X)
have w₂ : Eq (α := s.pt.obj X) ((hom (FC := TypeCat.Fun) (m.app X) : (a : P.obj X) → s.pt.obj X) x : s.pt.obj X)
  ((hom (FC := TypeCat.Fun) (m.app (op (unop X))) :
        (a : (fun (X : Type (max v₁ w)) ↦ X) (P.obj (op (unop X)))) →
          (fun (X : Type (max v₁ w)) ↦ X) (s.pt.obj (op (unop X))))
      ((unop (op (P.elementsMk X x))).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)) :
    (fun (X : Type (max v₁ w)) ↦ X) (s.pt.obj (op (unop X))))
Tactic: rw [← hm, uliftYonedaEquiv_comp, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
⊢ L.IsLeftKanExtension α ↔
    IsIso α ∧
      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
have mp : L.IsLeftKanExtension α →
  IsIso α ∧
    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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
mp :
  L.IsLeftKanExtension α →
    IsIso α ∧
      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
⊢ L.IsLeftKanExtension α ↔
    IsIso α ∧
      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
have mpr : IsIso α ∧
    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 →
  L.IsLeftKanExtension α
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
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
⊢ L.IsLeftKanExtension α
have mpr : (Functor.LeftExtension.mk L α).IsPointwiseLeftKanExtension
Tactic: apply Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
      (E := Functor.LeftExtension.mk _ α)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
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₁)
⊢ IsColimit ((Functor.LeftExtension.mk L α).coconeAt P)
have mpr : IsColimit
  (Cocone.whisker (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor
    ((Functor.LeftExtension.mk L α).coconeAt P))
Tactic: apply IsColimit.ofWhiskerEquivalence
      (CategoryOfElements.costructuredArrowULiftYonedaEquivalence _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
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
      (Functor.isoWhiskerLeft (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P) (asIso α)) ≪≫
    (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.isoWhiskerLeft
        (Iso.symm
          (Functor.associator (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P) uliftYoneda.{max w v₂, v₁, u₁}
            L)) ≪≫
      ((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))
have mpr : IsColimit
  ((Cocone.precompose e.symm.hom).obj
    (Cocone.whisker (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor
      ((Functor.LeftExtension.mk L α).coconeAt P)))
Tactic: refine (IsColimit.precomposeHomEquiv e.symm _).1 ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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₂)) ⥤ ℰ
e : A ≅ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 :
  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
⊢ L.IsLeftKanExtension e.hom
have rw : IsIso e.hom ∧
  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
Tactic: rw [isLeftKanExtension_along_uliftYoneda_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
X : C
Y : F.op.LeftExtension (Functor.obj yoneda X)
⊢ StructuredArrow.hom (Functor.LeftExtension.mk (Functor.obj yoneda (F.obj X)) (yonedaMap F X)) ≫
      Functor.map (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)) F.op)
        ((Equiv.symm yonedaEquiv :
            (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
          ((yonedaEquiv :
              (a : yoneda.obj X ⟶ F.op ⋙ StructuredArrow.right Y) → (F.op ⋙ StructuredArrow.right Y).obj (op X))
            (StructuredArrow.hom Y))) =
    StructuredArrow.hom Y
have w : ∀ (Z : Cᵒᵖ) (f : Functor.obj (Functor.obj yoneda X) Z),
  TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (NatTrans.app
          (StructuredArrow.hom (Functor.LeftExtension.mk (Functor.obj yoneda (F.obj X)) (yonedaMap F X)) ≫
            Functor.map (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)) F.op)
              ((Equiv.symm yonedaEquiv :
                  (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
                ((yonedaEquiv :
                    (a : yoneda.obj X ⟶ F.op ⋙ StructuredArrow.right Y) → (F.op ⋙ StructuredArrow.right Y).obj (op X))
                  (StructuredArrow.hom Y))))
          Z))
      f =
    (hom (FC := TypeCat.Fun) ((StructuredArrow.hom Y).app Z)).toFun f
Tactic: ext Z f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
X : C
Y : F.op.LeftExtension (Functor.obj yoneda X)
Z : Cᵒᵖ
f : Functor.obj (Functor.obj yoneda X) Z
⊢ TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (NatTrans.app
          (StructuredArrow.hom (Functor.LeftExtension.mk (Functor.obj yoneda (F.obj X)) (yonedaMap F X)) ≫
            Functor.map (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)) F.op)
              ((Equiv.symm yonedaEquiv :
                  (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
                ((yonedaEquiv :
                    (a : yoneda.obj X ⟶ F.op ⋙ StructuredArrow.right Y) → (F.op ⋙ StructuredArrow.right Y).obj (op X))
                  (StructuredArrow.hom Y))))
          Z))
      f =
    (hom (FC := TypeCat.Fun) ((StructuredArrow.hom Y).app Z)).toFun f
have h : f =
  (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda X) (Quiver.Hom.op f)) :
      (a : (yoneda.obj X).obj (op X)) → (yoneda.obj X).obj (op (unop Z)))
    (𝟙 X)
Tactic: convert! (Y.hom.naturality_apply f.op _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
X : C
Y : F.op.LeftExtension (Functor.obj yoneda X)
φ : Functor.LeftExtension.mk (Functor.obj yoneda (F.obj X)) (yonedaMap F X) ⟶ Y
⊢ φ =
    StructuredArrow.homMk
      ((Equiv.symm yonedaEquiv :
          (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
        ((yonedaEquiv :
            (a : yoneda.obj X ⟶ F.op ⋙ StructuredArrow.right Y) → (F.op ⋙ StructuredArrow.right Y).obj (op X))
          (StructuredArrow.hom Y)))
      ⋯
have h : StructuredArrow.Hom.right φ =
  StructuredArrow.Hom.right
    (StructuredArrow.homMk
      ((Equiv.symm yonedaEquiv :
          (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
        ((yonedaEquiv :
            (a : yoneda.obj X ⟶ F.op ⋙ StructuredArrow.right Y) → (F.op ⋙ StructuredArrow.right Y).obj (op X))
          (StructuredArrow.hom Y)))
      sorry)
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
X : C
Y : F.op.LeftExtension (Functor.obj yoneda X)
φ : Functor.LeftExtension.mk (Functor.obj yoneda (F.obj X)) (yonedaMap F X) ⟶ Y
⊢ StructuredArrow.Hom.right φ =
    StructuredArrow.Hom.right
      (StructuredArrow.homMk
        ((Equiv.symm yonedaEquiv :
            (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
          ((yonedaEquiv :
              (a : yoneda.obj X ⟶ F.op ⋙ StructuredArrow.right Y) → (F.op ⋙ StructuredArrow.right Y).obj (op X))
            (StructuredArrow.hom Y)))
        ⋯)
have h : Eq.{v₁ + 1} (α := (StructuredArrow.right Y).obj (op (F.obj X)))
  ((yonedaEquiv : (a : yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y) → (StructuredArrow.right Y).obj (op (F.obj X)))
      (StructuredArrow.Hom.right φ) :
    (StructuredArrow.right Y).obj (op (F.obj X)))
  ((yonedaEquiv : (a : yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y) → (StructuredArrow.right Y).obj (op (F.obj X)))
      (StructuredArrow.Hom.right
        (StructuredArrow.homMk
          ((Equiv.symm yonedaEquiv :
              (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
            ((yonedaEquiv :
                (a : yoneda.obj X ⟶ F.op ⋙ StructuredArrow.right Y) → (F.op ⋙ StructuredArrow.right Y).obj (op X))
              (StructuredArrow.hom Y)))
          sorry)) :
    (StructuredArrow.right Y).obj (op (F.obj X)))
Tactic: apply yonedaEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
Y : F.op.LeftExtension (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)
⊢ StructuredArrow.hom
        (Functor.LeftExtension.mk (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
          (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X)) ≫
      Functor.map (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op)
        ((Equiv.symm uliftYonedaEquiv :
            (a : (StructuredArrow.right Y).obj (op (F.obj X))) →
              uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y)
          ((uliftYonedaEquiv :
              (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ StructuredArrow.right Y) →
                (F.op ⋙ StructuredArrow.right Y).obj (op X))
            (StructuredArrow.hom Y))) =
    StructuredArrow.hom Y
have w : ∀ (Z : Cᵒᵖ) (f : Functor.obj (Functor.obj yoneda X) Z),
  TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (NatTrans.app
          (StructuredArrow.hom
              (Functor.LeftExtension.mk (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
                (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X)) ≫
            Functor.map (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op)
              ((Equiv.symm uliftYonedaEquiv :
                  (a : (StructuredArrow.right Y).obj (op (F.obj X))) →
                    uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y)
                ((uliftYonedaEquiv :
                    (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ StructuredArrow.right Y) →
                      (F.op ⋙ StructuredArrow.right Y).obj (op X))
                  (StructuredArrow.hom Y))))
          Z))
      { down := f : ULift.{max w v₂, v₁} (Functor.obj (Functor.obj yoneda X) Z) } =
    (hom (FC := TypeCat.Fun) ((StructuredArrow.hom Y).app Z)).toFun
      { down := f : ULift.{max w v₂, v₁} (Functor.obj (Functor.obj yoneda X) Z) }
Tactic: ext Z ⟨f⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
Y : F.op.LeftExtension (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)
φ :
  Functor.LeftExtension.mk (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
      (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X) ⟶
    Y
⊢ φ =
    StructuredArrow.homMk
      ((Equiv.symm uliftYonedaEquiv :
          (a : (StructuredArrow.right Y).obj (op (F.obj X))) →
            uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y)
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ StructuredArrow.right Y) →
              (F.op ⋙ StructuredArrow.right Y).obj (op X))
          (StructuredArrow.hom Y)))
      ⋯
have h : StructuredArrow.Hom.right φ =
  StructuredArrow.Hom.right
    (StructuredArrow.homMk
      ((Equiv.symm uliftYonedaEquiv :
          (a : (StructuredArrow.right Y).obj (op (F.obj X))) →
            uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y)
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ StructuredArrow.right Y) →
              (F.op ⋙ StructuredArrow.right Y).obj (op X))
          (StructuredArrow.hom Y)))
      sorry)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
Y : F.op.LeftExtension (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)
φ :
  Functor.LeftExtension.mk (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
      (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X) ⟶
    Y
⊢ StructuredArrow.Hom.right φ =
    StructuredArrow.Hom.right
      (StructuredArrow.homMk
        ((Equiv.symm uliftYonedaEquiv :
            (a : (StructuredArrow.right Y).obj (op (F.obj X))) →
              uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y)
          ((uliftYonedaEquiv :
              (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ StructuredArrow.right Y) →
                (F.op ⋙ StructuredArrow.right Y).obj (op X))
            (StructuredArrow.hom Y)))
        ⋯)
have h : Eq (α := (StructuredArrow.right Y).obj (op (F.obj X)))
  ((uliftYonedaEquiv :
        (a : uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y) →
          (StructuredArrow.right Y).obj (op (F.obj X)))
      (StructuredArrow.Hom.right φ) :
    (StructuredArrow.right Y).obj (op (F.obj X)))
  ((uliftYonedaEquiv :
        (a : uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y) →
          (StructuredArrow.right Y).obj (op (F.obj X)))
      (StructuredArrow.Hom.right
        (StructuredArrow.homMk
          ((Equiv.symm uliftYonedaEquiv :
              (a : (StructuredArrow.right Y).obj (op (F.obj X))) →
                uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y)
            ((uliftYonedaEquiv :
                (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ StructuredArrow.right Y) →
                  (F.op ⋙ StructuredArrow.right Y).obj (op X))
              (StructuredArrow.hom Y)))
          sorry)) :
    (StructuredArrow.right Y).obj (op (F.obj X)))
Tactic: apply uliftYonedaEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (hypothesis)
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
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
x y : P.Elements
f : x ⟶ y
⊢ Functor.map uliftYoneda.{max v₂ w, v₁, u₁} (↑f : x.fst ⟶ y.fst).unop ≫ coconeApp.{w, v₁, v₂, u₁, u₂} φ x =
    coconeApp.{w, v₁, v₂, u₁, u₂} φ y
have eq₁ : Eq (α := Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
  (Functor.map uliftYoneda.{max v₂ w, v₁, u₁} (↑f : x.fst ⟶ y.fst).unop ≫
    (Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop x.fst))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x.fst) ⟶ P)
      (x.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
  ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop y.1))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop y.1) ⟶ P)
    (y.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
Tactic: have eq₁ : uliftYoneda.map f.1.unop ≫ uliftYonedaEquiv.symm x.2 =
      uliftYonedaEquiv.{max w v₂}.symm y.2 :=
    uliftYonedaEquiv.injective
      (by simpa only [Equiv.apply_symm_apply, ← uliftYonedaEquiv_naturality] using f.2)