awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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 Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
X : C
p : Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X ⟶ P
⊢ Eq (α := (F.op ⋙ G.obj Q).obj (op X))
    ((hom (FC := TypeCat.Fun) ((F.op.whiskerLeft (G.map f)).app (op X)) :
          (a : (fun (X : Type (max v₁ v₂ w)) ↦ X) ((F.op ⋙ G.obj P).obj (op X))) →
            (fun (X : Type (max v₁ v₂ w)) ↦ X) ((F.op ⋙ G.obj Q).obj (op X)))
        ((hom (FC := TypeCat.Fun) ((G.map p).app (op (F.obj X))) :
            (a :
                (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                  ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op (F.obj X)))) →
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj P).obj (op (F.obj X))))
          ((hom (FC := TypeCat.Fun) ((φ.app X).app (op (F.obj X))) :
              (a :
                  (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                    (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (op (F.obj X)))) →
                (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                  (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (op (F.obj X))))
            { down := 𝟙 (unop (op (F.obj X))) })) :
      (fun (X : Type (max v₁ v₂ w)) ↦ X) ((F.op ⋙ G.obj Q).obj (op X)))
    ((hom (FC := TypeCat.Fun) ((G.map p ≫ G.map f).app (op (F.obj X))) :
          (a :
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op (F.obj X)))) →
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj Q).obj (op (F.obj X))))
        ((hom (FC := TypeCat.Fun) ((φ.app X).app (op (F.obj X))) :
            (a :
                (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                  (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (op (F.obj X)))) →
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (op (F.obj X))))
          { down := 𝟙 (unop (op (F.obj X))) }) :
      (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj Q).obj (op (F.obj X))))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
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
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
hγ :
  NatTrans.app F.op.lanUnit P ≫
      F.op.whiskerLeft
        (Functor.map F.op.lan f ≫
          (Functor.obj F.op.lan Q).descOfIsLeftKanExtension (NatTrans.app F.op.lanUnit Q) (G.obj Q)
            (presheafHom.{w, v₁, v₂, u₁, u₂} φ Q)) =
    NatTrans.app F.op.lanUnit P ≫
      F.op.whiskerLeft
        ((Functor.obj F.op.lan P).descOfIsLeftKanExtension (NatTrans.app F.op.lanUnit P) (G.obj P)
            (presheafHom.{w, v₁, v₂, u₁, u₂} φ P) ≫
          G.map f)
⊢ Functor.map F.op.lan f ≫
      (Functor.obj F.op.lan Q).descOfIsLeftKanExtension (NatTrans.app F.op.lanUnit Q) (G.obj Q)
        (presheafHom.{w, v₁, v₂, u₁, u₂} φ Q) =
    (Functor.obj F.op.lan P).descOfIsLeftKanExtension (NatTrans.app F.op.lanUnit P) (G.obj P)
        (presheafHom.{w, v₁, v₂, u₁, u₂} φ P) ≫
      G.map f

Tactic:
apply (F.op.lan.obj P).hom_ext_of_isLeftKanExtension (F.op.lanUnit.app P)

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.hom_ext_of_isLeftKanExtension, CategoryTheory.Functor.lan, CategoryTheory.Functor.lanUnit, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
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
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
⊢ Eq (α :=
    Functor.obj (𝟭 (Cᵒᵖ ⥤ Type (max w v₁ v₂))) P ⟶
      Functor.obj (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w v₁ v₂))) F.op) Q)
    (Functor.map (𝟭 (Cᵒᵖ ⥤ Type (max w v₁ v₂))) f ≫ NatTrans.app F.op.lanUnit Q)
    (NatTrans.app F.op.lanUnit P ≫
      Functor.map (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w v₁ v₂))) F.op) f)

Tactic:
have eq := F.op.lanUnit.naturality f
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
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
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
eq :
  Eq (α :=
    Functor.obj (𝟭 (Cᵒᵖ ⥤ Type (max w v₁ v₂))) P ⟶
      Functor.obj (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w v₁ v₂))) F.op) Q)
    (Functor.map (𝟭 (Cᵒᵖ ⥤ Type (max w v₁ v₂))) f ≫ NatTrans.app F.op.lanUnit Q)
    (NatTrans.app F.op.lanUnit P ≫
      Functor.map (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w v₁ v₂))) F.op) f)
hγ :
  NatTrans.app F.op.lanUnit P ≫
      F.op.whiskerLeft (Functor.map F.op.lan f) ≫
        F.op.whiskerLeft
          ((Functor.obj F.op.lan Q).descOfIsLeftKanExtension (NatTrans.app F.op.lanUnit Q) (G.obj Q)
            (presheafHom.{w, v₁, v₂, u₁, u₂} φ Q)) =
    NatTrans.app F.op.lanUnit P ≫
      F.op.whiskerLeft
          ((Functor.obj F.op.lan P).descOfIsLeftKanExtension (NatTrans.app F.op.lanUnit P) (G.obj P)
            (presheafHom.{w, v₁, v₂, u₁, u₂} φ P)) ≫
        F.op.whiskerLeft (G.map f)
⊢ NatTrans.app F.op.lanUnit P ≫
      F.op.whiskerLeft
        (Functor.map F.op.lan f ≫
          (Functor.obj F.op.lan Q).descOfIsLeftKanExtension (NatTrans.app F.op.lanUnit Q) (G.obj Q)
            (presheafHom.{w, v₁, v₂, u₁, u₂} φ Q)) =
    NatTrans.app F.op.lanUnit P ≫
      F.op.whiskerLeft
        ((Functor.obj F.op.lan P).descOfIsLeftKanExtension (NatTrans.app F.op.lanUnit P) (G.obj P)
            (presheafHom.{w, v₁, v₂, u₁, u₂} φ P) ≫
          G.map f)

Tactic:
dsimp at eq ⊢
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
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
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
eq :
  Eq (α := P ⟶ F.op ⋙ Functor.obj F.op.lan Q) (f ≫ NatTrans.app F.op.lanUnit Q)
    (NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft (Functor.map F.op.lan f))
hγ :
  NatTrans.app F.op.lanUnit P ≫
      F.op.whiskerLeft (Functor.map F.op.lan f) ≫
        F.op.whiskerLeft
          ((Functor.obj F.op.lan Q).descOfIsLeftKanExtension (NatTrans.app F.op.lanUnit Q) (G.obj Q)
            (presheafHom.{w, v₁, v₂, u₁, u₂} φ Q)) =
    presheafHom.{w, v₁, v₂, u₁, u₂} φ P ≫ F.op.whiskerLeft (G.map f)
hγ₁ :
  f ≫
      NatTrans.app F.op.lanUnit Q ≫
        F.op.whiskerLeft
          ((Functor.obj F.op.lan Q).descOfIsLeftKanExtension (NatTrans.app F.op.lanUnit Q) (G.obj Q)
            (presheafHom.{w, v₁, v₂, u₁, u₂} φ Q)) =
    presheafHom.{w, v₁, v₂, u₁, u₂} φ P ≫ F.op.whiskerLeft (G.map f)
hγ₂ : f ≫ presheafHom.{w, v₁, v₂, u₁, u₂} φ Q = presheafHom.{w, v₁, v₂, u₁, u₂} φ P ≫ F.op.whiskerLeft (G.map f)
hγ₃ hγ₄ : f ≫ presheafHom.{w, v₁, v₂, u₁, u₂} φ Q = f ≫ presheafHom.{w, v₁, v₂, u₁, u₂} φ Q
⊢ NatTrans.app F.op.lanUnit P ≫
      F.op.whiskerLeft (Functor.map F.op.lan f) ≫
        F.op.whiskerLeft
          ((Functor.obj F.op.lan Q).descOfIsLeftKanExtension (NatTrans.app F.op.lanUnit Q) (G.obj Q)
            (presheafHom.{w, v₁, v₂, u₁, u₂} φ Q)) =
    NatTrans.app F.op.lanUnit P ≫
      F.op.whiskerLeft
          ((Functor.obj F.op.lan P).descOfIsLeftKanExtension (NatTrans.app F.op.lanUnit P) (G.obj P)
            (presheafHom.{w, v₁, v₂, u₁, u₂} φ P)) ≫
        F.op.whiskerLeft (G.map f)

Tactic:
rw [Functor.descOfIsLeftKanExtension_fac_assoc, ← reassoc_of% eq,
      Functor.descOfIsLeftKanExtension_fac, presheafHom_naturality]

Premises used: CategoryTheory.Functor.descOfIsLeftKanExtension_fac_assoc, CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.presheafHom_naturality, CategoryTheory.Functor.descOfIsLeftKanExtension_fac
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
dsimp :
  (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).descOfIsLeftKanExtension
      (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
      (G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
      (presheafHom.{w, v₁, v₂, u₁, u₂} φ (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)) =
    NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X
⊢ NatTrans.app (natTrans.{w, v₁, v₂, u₁, u₂} φ) (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X) =
    NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X

Tactic:
dsimp [natTrans]

Premises used: CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.natTrans
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
hγ :
  NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
      F.op.whiskerLeft
        ((Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).descOfIsLeftKanExtension
          (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
          (G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
          (presheafHom.{w, v₁, v₂, u₁, u₂} φ (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))) =
    NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
      F.op.whiskerLeft (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X)
⊢ (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).descOfIsLeftKanExtension
      (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
      (G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
      (presheafHom.{w, v₁, v₂, u₁, u₂} φ (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)) =
    NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X

Tactic:
apply (F.op.lan.obj (uliftYoneda.obj X)).hom_ext_of_isLeftKanExtension (F.op.lanUnit.app _)

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.hom_ext_of_isLeftKanExtension, CategoryTheory.Functor.lan, CategoryTheory.Functor.lanUnit, CategoryTheory.uliftYoneda, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
hγ :
  presheafHom.{w, v₁, v₂, u₁, u₂} φ (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X) =
    NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
      F.op.whiskerLeft (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X)
⊢ NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
      F.op.whiskerLeft
        ((Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).descOfIsLeftKanExtension
          (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
          (G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
          (presheafHom.{w, v₁, v₂, u₁, u₂} φ (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))) =
    NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
      F.op.whiskerLeft (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X)

Tactic:
rw [Functor.descOfIsLeftKanExtension_fac]

Premises used: CategoryTheory.Functor.descOfIsLeftKanExtension_fac
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
hγ :
  Eq (α := (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
            (F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X))
        (presheafHom.{w, v₁, v₂, u₁, u₂} φ (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)) :
      (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
            (F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X))
        (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
          F.op.whiskerLeft
            (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X)) :
      (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
⊢ presheafHom.{w, v₁, v₂, u₁, u₂} φ (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X) =
    NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
      F.op.whiskerLeft (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X)

Tactic:
apply uliftYonedaEquiv.injective

Premises used: Equiv.injective, CategoryTheory.uliftYonedaEquiv
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
hγ :
  Eq (α := (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
    ((hom (FC := TypeCat.Fun) ((φ.app X).app (F.op.obj (op X))) :
          (a :
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (F.op.obj (op X)))) →
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
              (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (F.op.obj (op X))))
        { down := 𝟙 (unop (F.op.obj (op X))) } :
      (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (F.op.obj (op X))))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
            (F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X))
        (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
          F.op.whiskerLeft
            (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X)) :
      (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
⊢ Eq (α := (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
            (F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X))
        (presheafHom.{w, v₁, v₂, u₁, u₂} φ (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)) :
      (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
            (F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X))
        (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
          F.op.whiskerLeft
            (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X)) :
      (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))

Tactic:
rw [uliftYonedaEquiv_presheafHom_uliftYoneda_obj]

Premises used: CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_presheafHom_uliftYoneda_obj
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
⊢ Eq (α := (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
    ((hom (FC := TypeCat.Fun) ((φ.app X).app (F.op.obj (op X))) :
          (a :
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (F.op.obj (op X)))) →
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
              (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (F.op.obj (op X))))
        { down := 𝟙 (unop (F.op.obj (op X))) } :
      (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (F.op.obj (op X))))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
            (F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X))
        (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
          F.op.whiskerLeft
            (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X)) :
      (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))

Tactic:
_root_.congr_arg _ (compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id F X).symm

Premises used: CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id, congr_arg, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
⊢ Eq (α := (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
    ((hom (FC := TypeCat.Fun) ((φ.app X).app (F.op.obj (op X))) :
          (a :
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (F.op.obj (op X)))) →
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
              (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (F.op.obj (op X))))
        { down := 𝟙 (unop (F.op.obj (op X))) } :
      (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (F.op.obj (op X))))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
            (F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X))
        (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
          F.op.whiskerLeft
            (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X)) :
      (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))

Tactic:
exact _root_.congr_arg _ (compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id F X).symm

Premises used: CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id, congr_arg, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
w :
  ∀ (X : C),
    (StructuredArrow.hom
              (Functor.LeftExtension.mk F.op.lan
                (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F))) ≫
            Functor.map
              (Functor.obj (Functor.whiskeringLeft C (Cᵒᵖ ⥤ Type (max (max w v₁) v₂)) (Dᵒᵖ ⥤ Type (max (max w v₁) v₂)))
                uliftYoneda.{max w v₂, v₁, u₁})
              (natTrans.{w, v₁, v₂, u₁, u₂} (StructuredArrow.hom Φ))).app
        X =
      (StructuredArrow.hom Φ).app X
⊢ StructuredArrow.hom
        (Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F))) ≫
      Functor.map
        (Functor.obj (Functor.whiskeringLeft C (Cᵒᵖ ⥤ Type (max (max w v₁) v₂)) (Dᵒᵖ ⥤ Type (max (max w v₁) v₂)))
          uliftYoneda.{max w v₂, v₁, u₁})
        (natTrans.{w, v₁, v₂, u₁, u₂} (StructuredArrow.hom Φ)) =
    StructuredArrow.hom Φ

Tactic:
ext X : 2
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
X : C
w :
  NatTrans.app (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫
      NatTrans.app (natTrans.{w, v₁, v₂, u₁, u₂} (StructuredArrow.hom Φ))
        (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X) =
    (StructuredArrow.hom Φ).app X
⊢ (StructuredArrow.hom
            (Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F))) ≫
          Functor.map
            (Functor.obj (Functor.whiskeringLeft C (Cᵒᵖ ⥤ Type (max (max w v₁) v₂)) (Dᵒᵖ ⥤ Type (max (max w v₁) v₂)))
              uliftYoneda.{max w v₂, v₁, u₁})
            (natTrans.{w, v₁, v₂, u₁, u₂} (StructuredArrow.hom Φ))).app
      X =
    (StructuredArrow.hom Φ).app X

Tactic:
dsimp