-- Mathlib/CategoryTheory/Limits/Presheaf.lean
lemma natTrans_app_yoneda_obj (X : C) : (natTrans φ).app (yoneda.obj X) =
    (compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
X : C
⊢ (F.op.lan.obj (yoneda.obj X)).descOfIsLeftKanExtension (F.op.lanUnit.app (yoneda.obj X)) (G.obj (yoneda.obj X))
      (presheafHom φ (yoneda.obj X)) =
    (compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X

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

Result:
case hγ
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
X : C
⊢ F.op.lanUnit.app (yoneda.obj X) ≫
      whiskerLeft F.op
        ((F.op.lan.obj (yoneda.obj X)).descOfIsLeftKanExtension (F.op.lanUnit.app (yoneda.obj X)) (G.obj (yoneda.obj X))
          (presheafHom φ (yoneda.obj X))) =
    F.op.lanUnit.app (yoneda.obj X) ≫ whiskerLeft F.op ((compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
X : C
⊢ (natTrans φ).app (yoneda.obj X) = (compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X

Tactic:
dsimp [natTrans]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
X : C
⊢ (F.op.lan.obj (yoneda.obj X)).descOfIsLeftKanExtension (F.op.lanUnit.app (yoneda.obj X)) (G.obj (yoneda.obj X))
      (presheafHom φ (yoneda.obj X)) =
    (compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X

Proof state:
case hγ.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
X : C
⊢ (φ.app X).app (F.op.obj (Opposite.op X)) (𝟙 (Opposite.unop (F.op.obj (Opposite.op X)))) =
    yonedaEquiv
      (F.op.lanUnit.app (yoneda.obj X) ≫ whiskerLeft F.op ((compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X))

Tactic:
exact congr_arg _ (compYonedaIsoYonedaCompLan_inv_app_app_apply_eq_id F X).symm

Result:
no goals

Proof state:
case hγ
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
X : C
⊢ F.op.lanUnit.app (yoneda.obj X) ≫
      whiskerLeft F.op
        ((F.op.lan.obj (yoneda.obj X)).descOfIsLeftKanExtension (F.op.lanUnit.app (yoneda.obj X)) (G.obj (yoneda.obj X))
          (presheafHom φ (yoneda.obj X))) =
    F.op.lanUnit.app (yoneda.obj X) ≫ whiskerLeft F.op ((compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X)

Tactic:
rw [Functor.descOfIsLeftKanExtension_fac]

Result:
case hγ
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
X : C
⊢ presheafHom φ (yoneda.obj X) =
    F.op.lanUnit.app (yoneda.obj X) ≫ whiskerLeft F.op ((compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X)

Proof state:
case hγ
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
X : C
⊢ presheafHom φ (yoneda.obj X) =
    F.op.lanUnit.app (yoneda.obj X) ≫ whiskerLeft F.op ((compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X)

Tactic:
apply yonedaEquiv.injective

Result:
case hγ.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
X : C
⊢ yonedaEquiv (presheafHom φ (yoneda.obj X)) =
    yonedaEquiv
      (F.op.lanUnit.app (yoneda.obj X) ≫ whiskerLeft F.op ((compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X))

Proof state:
case hγ.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
X : C
⊢ yonedaEquiv (presheafHom φ (yoneda.obj X)) =
    yonedaEquiv
      (F.op.lanUnit.app (yoneda.obj X) ≫ whiskerLeft F.op ((compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X))

Tactic:
rw [yonedaEquiv_presheafHom_yoneda_obj]

Result:
case hγ.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
X : C
⊢ (φ.app X).app (F.op.obj (Opposite.op X)) (𝟙 (Opposite.unop (F.op.obj (Opposite.op X)))) =
    yonedaEquiv
      (F.op.lanUnit.app (yoneda.obj X) ≫ whiskerLeft F.op ((compYonedaIsoYonedaCompLan F).inv.app X ≫ φ.app X))