-- Mathlib/CategoryTheory/Limits/Presheaf.lean
@[ext]
lemma hom_ext {Φ : yoneda.LeftExtension (F ⋙ yoneda)}
    (f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ) :
    f = g

Proof state:
case h.w.h.hγ.e_a.e_α.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
Φ : yoneda.LeftExtension (F ⋙ yoneda)
f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type v₁
x : P.Elementsᵒᵖ
eq :
  yonedaEquiv.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫
      whiskerLeft F.op (F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd))
eq₁ :
  (f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app
      (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app
        (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) =
    (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))
eq₂ :
  (g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app
      (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app
        (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) =
    (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))
⊢ yonedaEquiv
      ((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst) ≫
        f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫
          Φ.right.map (yonedaEquiv.symm (Opposite.unop x).snd)) =
    yonedaEquiv
      ((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst) ≫
        g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫
          Φ.right.map (yonedaEquiv.symm (Opposite.unop x).snd))

Tactic:
dsimp [yonedaEquiv_apply]

Result:
case h.w.h.hγ.e_a.e_α.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
Φ : yoneda.LeftExtension (F ⋙ yoneda)
f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type v₁
x : P.Elementsᵒᵖ
eq :
  yonedaEquiv.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫
      whiskerLeft F.op (F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd))
eq₁ :
  (f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app
      (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app
        (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) =
    (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))
eq₂ :
  (g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app
      (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app
        (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) =
    (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))
⊢ (Φ.right.map (yonedaEquiv.symm (Opposite.unop x).snd)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      ((f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).1))).app
        (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
        (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app
          (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
          (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst))))) =
    (Φ.right.map (yonedaEquiv.symm (Opposite.unop x).snd)).app
      (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      ((g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).1))).app
        (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
        (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app
          (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
          (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))))

Proof state:
case h.w.h.hγ
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
Φ : yoneda.LeftExtension (F ⋙ yoneda)
f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type v₁
x : P.Elementsᵒᵖ
⊢ (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) =
    (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)

Tactic:
have eq := F.op.lanUnit.naturality (yonedaEquiv.symm x.unop.2)

Result:
case h.w.h.hγ
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
Φ : yoneda.LeftExtension (F ⋙ yoneda)
f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type v₁
x : P.Elementsᵒᵖ
eq :
  (𝟭 (Cᵒᵖ ⥤ Type v₁)).map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫
      (F.op.lan ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op).map (yonedaEquiv.symm (Opposite.unop x).snd)
⊢ (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) =
    (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)