-- 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
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₁
⊢ f.right.app P = g.right.app P

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

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₁
⊢ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) = F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)

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ᵒᵖ
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)))
⊢ 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) ≫ f.right.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) ≫ g.right.app P)

Tactic:
congr 2

Result:
case h.w.h.hγ.e_a.e_α
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)))
⊢ F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ f.right.app P =
    F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ g.right.app P