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₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
rw :
  Eq (α := A.obj y.left ⟶ E)
    (A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)))
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op y.left))
        (y.hom ≫ g)))
⊢ A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)) =
    ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y.left))
          (y.hom ≫ g)) ≫
      𝟙 E
have rw₁ : Eq (α := A.obj y.left ⟶ E)
  (A.map f.left ≫
    ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op y'.left))
        (y'.hom ≫ g)))
  (ULift.down
    ((uliftYonedaEquiv :
        (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
          ((restrictedULiftYoneda A).obj E).obj (op y.left))
      ((Functor.map uliftYoneda.{max w v₂, v₁, u₁} f.left ≫ y'.hom) ≫ g)))
Tactic: rw [comp_id, ← CostructuredArrow.w f, assoc, map_comp_uliftYonedaEquiv_down]
-- 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₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
rw :
  Eq (α := A.obj y.left ⟶ E)
    (A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)))
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op y.left))
        (y.hom ≫ g)))
rw₁ :
  Eq (α := A.obj y.left ⟶ E)
    (A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)))
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op y.left))
        ((Functor.map uliftYoneda.{max w v₂, v₁, u₁} f.left ≫ y'.hom) ≫ g)))
⊢ A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)) =
    ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y.left))
          (y.hom ≫ g)) ≫
      𝟙 E
have rw₂ : Eq (α := A.obj y.left ⟶ E)
  (A.map f.left ≫
    ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op y'.left))
        (y'.hom ≫ g)))
  (ULift.down
    ((uliftYonedaEquiv :
        (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
          ((restrictedULiftYoneda A).obj E).obj (op y.left))
      (Functor.map uliftYoneda.{max w v₂, v₁, u₁} f.left ≫ y'.hom ≫ g)))
Tactic: rw [comp_id, ← CostructuredArrow.w f, assoc, map_comp_uliftYonedaEquiv_down]
-- 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₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
rw :
  Eq (α := A.obj y.left ⟶ E)
    (A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)))
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op y.left))
        (y.hom ≫ g)))
rw₁ :
  Eq (α := A.obj y.left ⟶ E)
    (A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)))
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op y.left))
        ((Functor.map uliftYoneda.{max w v₂, v₁, u₁} f.left ≫ y'.hom) ≫ g)))
rw₂ :
  Eq (α := A.obj y.left ⟶ E)
    (A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)))
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op y.left))
        (Functor.map uliftYoneda.{max w v₂, v₁, u₁} f.left ≫ y'.hom ≫ g)))
⊢ A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)) =
    ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y.left))
          (y.hom ≫ g)) ≫
      𝟙 E
have rw₃ : Eq.{v₂ + 1} (α := A.obj y.left ⟶ E)
  (ULift.down
    ((uliftYonedaEquiv :
        (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
          ((restrictedULiftYoneda A).obj E).obj (op y.left))
      (Functor.map uliftYoneda.{max v₂ w, v₁, u₁} f.left ≫ y'.hom ≫ g)))
  (ULift.down
    ((uliftYonedaEquiv :
        (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
          ((restrictedULiftYoneda A).obj E).obj (op y.left))
      (Functor.map uliftYoneda.{max w v₂, v₁, u₁} f.left ≫ y'.hom ≫ g)))
Tactic: rw [comp_id, ← CostructuredArrow.w f, assoc, map_comp_uliftYonedaEquiv_down]
-- 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_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
⊢ Eq.{v₂ + 1} (α := L.obj P ⟶ X)
    (((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P X).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj X) → L.obj P ⟶ X)
        (f ≫ g) :
      L.obj P ⟶ X)
    (L.map f ≫
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α Q X).symm :
            (a : Q ⟶ (restrictedULiftYoneda A).obj X) → L.obj Q ⟶ X)
          g :
      L.obj P ⟶ X)
have apply : ∀ (j : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P),
  Eq (α := Functor.obj (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A) j ⟶ X)
    (((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫
      ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P X).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj X) → L.obj P ⟶ X)
        (f ≫ g))
    (((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫
      L.map f ≫
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α Q X).symm :
            (a : Q ⟶ (restrictedULiftYoneda A).obj X) → L.obj Q ⟶ X)
          g)
Tactic: apply (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (hypothesis)
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 (α := Functor.obj (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A) p ⟶ X)
    (((Functor.LeftExtension.mk L α).coconeAt P).ι.app p ≫
      ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P X).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj X) → L.obj P ⟶ X)
        (f ≫ g))
    (((Functor.LeftExtension.mk L α).coconeAt P).ι.app p ≫
      L.map f ≫
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α Q X).symm :
            (a : Q ⟶ (restrictedULiftYoneda A).obj X) → L.obj Q ⟶ X)
          g)
have hfg : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (hypothesis)
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
⊢ 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)
have 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} (α := ((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)
-- 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_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')
⊢ 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)
have 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)
Tactic: apply (restrictedULiftYonedaHomEquiv L α P Y).symm.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (hypothesis)
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
⊢ 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))
have 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))
Tactic: have h₁ := (uliftYonedaAdjunction.{w} L α).homEquiv_unit P _ (𝟙 _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (hypothesis)
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))
⊢ 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))
have 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
Tactic: simp only [Functor.comp_obj, Functor.map_id, comp_id] at h₁
Cleared hypotheses: h₁
-- 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₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
⊢ 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)
have 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)
Tactic: dsimp
-- 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₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
⊢ 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)
have 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)))
Tactic: rw [comp_id, ← uliftYonedaEquiv_symm_map, f.unop.2]