-- 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γ
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)

Tactic:
apply (colimitOfRepresentable P).hom_ext

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₁
⊢ ∀ (j : P.Elementsᵒᵖ),
    (coconeOfRepresentable P).ι.app j ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) =
      (coconeOfRepresentable P).ι.app j ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)

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)))
⊢ (Φ.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)))))

Tactic:
rw [eq₁, eq₂]

Result:
no goals

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 :
  (𝟭 (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)
eq₁ :
  (((Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom).hom ≫
              ((whiskeringLeft C (Cᵒᵖ ⥤ Type v₁) (Dᵒᵖ ⥤ Type v₁)).obj yoneda).map f.right).app
          (Opposite.unop (Opposite.unop x).fst)).app
      (F.op.obj (Opposite.unop x).fst) (𝟙 (Opposite.unop (F.op.obj (Opposite.unop x).fst))) =
    (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (F.op.obj (Opposite.unop x).fst)
      (𝟙 (Opposite.unop (F.op.obj (Opposite.unop x).fst)))
eq₂ :
  (((Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom).hom ≫
              ((whiskeringLeft C (Cᵒᵖ ⥤ Type v₁) (Dᵒᵖ ⥤ Type v₁)).obj yoneda).map g.right).app
          (Opposite.unop (Opposite.unop x).fst)).app
      (F.op.obj (Opposite.unop x).fst) (𝟙 (Opposite.unop (F.op.obj (Opposite.unop x).fst))) =
    (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (F.op.obj (Opposite.unop x).fst)
      (𝟙 (Opposite.unop (F.op.obj (Opposite.unop x).fst)))
⊢ (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:
dsimp at eq₁ eq₂ eq ⊢

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 :
  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.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) =
    yonedaEquiv.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)