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
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 : C
f : Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X ⟶ P
⊢ Eq (α := (F.op ⋙ G.obj P).obj (op X))
    ((uliftYonedaEquiv : (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj P) → (F.op ⋙ G.obj P).obj (op X))
        (f ≫ presheafHom.{w, v₁, v₂, u₁, u₂} φ P) :
      (F.op ⋙ G.obj P).obj (op X))
    ((hom (FC := TypeCat.Fun) ((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 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 (max v₁ v₂) w)) ↦ X) ((G.obj P).obj (op (F.obj X))))
have obtain : ∀ (x : P.obj (op X)),
  Eq (α := (F.op ⋙ G.obj P).obj (op X))
    ((uliftYonedaEquiv : (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj P) → (F.op ⋙ G.obj P).obj (op X))
        ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X)) → uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ P) x ≫
          presheafHom.{w, v₁, v₂, u₁, u₂} φ P) :
      (F.op ⋙ G.obj P).obj (op X))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app
              (G.map ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X)) → uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ P) x))
              (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 (max v₁ v₂) w)) ↦ X) ((G.obj P).obj (op (F.obj X))))
Tactic: obtain ⟨x, rfl⟩ := uliftYonedaEquiv.symm.surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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))
    ((uliftYonedaEquiv : (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj Q) → (F.op ⋙ G.obj Q).obj (op X))
        (p ≫ presheafHom.{w, v₁, v₂, u₁, u₂} φ P ≫ F.op.whiskerLeft (G.map f)) :
      (F.op ⋙ G.obj Q).obj (op X))
    ((uliftYonedaEquiv : (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj Q) → (F.op ⋙ G.obj Q).obj (op X))
        (p ≫ f ≫ presheafHom.{w, v₁, v₂, u₁, u₂} φ Q) :
      (F.op ⋙ G.obj Q).obj (op X))
have rw : 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: rw [← assoc p f, uliftYonedaEquiv_ι_presheafHom, ← assoc,
      uliftYonedaEquiv_comp, uliftYonedaEquiv_ι_presheafHom,
      Functor.map_comp]
-- 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
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
⊢ 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
have 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)
Tactic: apply (F.op.lan.obj P).hom_ext_of_isLeftKanExtension (F.op.lanUnit.app 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_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
⊢ 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)
have 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)
Tactic: have eq := F.op.lanUnit.naturality 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
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)
⊢ 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)
have 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)
Tactic: dsimp at eq ⊢
-- 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
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))
⊢ 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)
have 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)
Tactic: rw [Functor.descOfIsLeftKanExtension_fac_assoc, ← reassoc_of% eq,
      Functor.descOfIsLeftKanExtension_fac, presheafHom_naturality]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [Functor.descOfIsLeftKanExtension_fac_assoc, ← reassoc_of% eq,
      Functor.descOfIsLeftKanExtension_fac, presheafHom_naturality]
-- 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
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)
⊢ 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)
have hγ₂ : f ≫ presheafHom.{w, v₁, v₂, u₁, u₂} φ Q = 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]
-- 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
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)
⊢ 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)
have hγ₃ : f ≫ presheafHom.{w, v₁, v₂, u₁, u₂} φ Q = f ≫ presheafHom.{w, v₁, v₂, u₁, u₂} φ Q
Tactic: rw [Functor.descOfIsLeftKanExtension_fac_assoc, ← reassoc_of% eq,
      Functor.descOfIsLeftKanExtension_fac, presheafHom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
⊢ 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
have 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
Tactic: dsimp [natTrans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
⊢ (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
have 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)
Tactic: apply (F.op.lan.obj (uliftYoneda.obj X)).hom_ext_of_isLeftKanExtension (F.op.lanUnit.app _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
⊢ 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)
have 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)
Tactic: rw [Functor.descOfIsLeftKanExtension_fac]